MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1259lem2 Structured version   Visualization version   GIF version

Theorem 1259lem2 16041
Description: Lemma for 1259prm 16045. Calculate a power mod. In decimal, we calculate 2↑34 = (2↑17)↑2≡136↑2≡14𝑁 + 870. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
Hypothesis
Ref Expression
1259prm.1 𝑁 = 1259
Assertion
Ref Expression
1259lem2 ((2↑34) mod 𝑁) = (870 mod 𝑁)

Proof of Theorem 1259lem2
StepHypRef Expression
1 1259prm.1 . . 3 𝑁 = 1259
2 1nn0 11500 . . . . . 6 1 ∈ ℕ0
3 2nn0 11501 . . . . . 6 2 ∈ ℕ0
42, 3deccl 11704 . . . . 5 12 ∈ ℕ0
5 5nn0 11504 . . . . 5 5 ∈ ℕ0
64, 5deccl 11704 . . . 4 125 ∈ ℕ0
7 9nn 11384 . . . 4 9 ∈ ℕ
86, 7decnncl 11710 . . 3 1259 ∈ ℕ
91, 8eqeltri 2835 . 2 𝑁 ∈ ℕ
10 2nn 11377 . 2 2 ∈ ℕ
11 7nn0 11506 . . 3 7 ∈ ℕ0
122, 11deccl 11704 . 2 17 ∈ ℕ0
13 4nn0 11503 . . . 4 4 ∈ ℕ0
142, 13deccl 11704 . . 3 14 ∈ ℕ0
1514nn0zi 11594 . 2 14 ∈ ℤ
16 3nn0 11502 . . . 4 3 ∈ ℕ0
172, 16deccl 11704 . . 3 13 ∈ ℕ0
18 6nn0 11505 . . 3 6 ∈ ℕ0
1917, 18deccl 11704 . 2 136 ∈ ℕ0
20 8nn0 11507 . . . 4 8 ∈ ℕ0
2120, 11deccl 11704 . . 3 87 ∈ ℕ0
22 0nn0 11499 . . 3 0 ∈ ℕ0
2321, 22deccl 11704 . 2 870 ∈ ℕ0
2411259lem1 16040 . 2 ((2↑17) mod 𝑁) = (136 mod 𝑁)
25 eqid 2760 . . 3 17 = 17
26 2cn 11283 . . . . . 6 2 ∈ ℂ
2726mulid1i 10234 . . . . 5 (2 · 1) = 2
2827oveq1i 6823 . . . 4 ((2 · 1) + 1) = (2 + 1)
29 2p1e3 11343 . . . 4 (2 + 1) = 3
3028, 29eqtri 2782 . . 3 ((2 · 1) + 1) = 3
31 7cn 11296 . . . 4 7 ∈ ℂ
32 7t2e14 11840 . . . 4 (7 · 2) = 14
3331, 26, 32mulcomli 10239 . . 3 (2 · 7) = 14
343, 2, 11, 25, 13, 2, 30, 33decmul2c 11781 . 2 (2 · 17) = 34
35 9nn0 11508 . . . 4 9 ∈ ℕ0
36 eqid 2760 . . . 4 870 = 870
37 eqid 2760 . . . . 5 125 = 125
38 eqid 2760 . . . . . 6 87 = 87
39 eqid 2760 . . . . . 6 12 = 12
40 8p1e9 11350 . . . . . 6 (8 + 1) = 9
41 7p2e9 11364 . . . . . 6 (7 + 2) = 9
4220, 11, 2, 3, 38, 39, 40, 41decadd 11762 . . . . 5 (87 + 12) = 99
43 9p7e16 11817 . . . . . 6 (9 + 7) = 16
44 eqid 2760 . . . . . . 7 14 = 14
45 3cn 11287 . . . . . . . . 9 3 ∈ ℂ
46 ax-1cn 10186 . . . . . . . . 9 1 ∈ ℂ
47 3p1e4 11345 . . . . . . . . 9 (3 + 1) = 4
4845, 46, 47addcomli 10420 . . . . . . . 8 (1 + 3) = 4
4913dec0h 11714 . . . . . . . 8 4 = 04
5048, 49eqtri 2782 . . . . . . 7 (1 + 3) = 04
5146mulid1i 10234 . . . . . . . . 9 (1 · 1) = 1
52 00id 10403 . . . . . . . . 9 (0 + 0) = 0
5351, 52oveq12i 6825 . . . . . . . 8 ((1 · 1) + (0 + 0)) = (1 + 0)
5446addid1i 10415 . . . . . . . 8 (1 + 0) = 1
5553, 54eqtri 2782 . . . . . . 7 ((1 · 1) + (0 + 0)) = 1
56 4cn 11290 . . . . . . . . . 10 4 ∈ ℂ
5756mulid1i 10234 . . . . . . . . 9 (4 · 1) = 4
5857oveq1i 6823 . . . . . . . 8 ((4 · 1) + 4) = (4 + 4)
59 4p4e8 11356 . . . . . . . 8 (4 + 4) = 8
6020dec0h 11714 . . . . . . . 8 8 = 08
6158, 59, 603eqtri 2786 . . . . . . 7 ((4 · 1) + 4) = 08
622, 13, 22, 13, 44, 50, 2, 20, 22, 55, 61decmac 11758 . . . . . 6 ((14 · 1) + (1 + 3)) = 18
6318dec0h 11714 . . . . . . 7 6 = 06
6426mulid2i 10235 . . . . . . . . 9 (1 · 2) = 2
6546addid2i 10416 . . . . . . . . 9 (0 + 1) = 1
6664, 65oveq12i 6825 . . . . . . . 8 ((1 · 2) + (0 + 1)) = (2 + 1)
6766, 29eqtri 2782 . . . . . . 7 ((1 · 2) + (0 + 1)) = 3
68 4t2e8 11373 . . . . . . . . 9 (4 · 2) = 8
6968oveq1i 6823 . . . . . . . 8 ((4 · 2) + 6) = (8 + 6)
70 8p6e14 11808 . . . . . . . 8 (8 + 6) = 14
7169, 70eqtri 2782 . . . . . . 7 ((4 · 2) + 6) = 14
722, 13, 22, 18, 44, 63, 3, 13, 2, 67, 71decmac 11758 . . . . . 6 ((14 · 2) + 6) = 34
732, 3, 2, 18, 39, 43, 14, 13, 16, 62, 72decma2c 11760 . . . . 5 ((14 · 12) + (9 + 7)) = 184
7435dec0h 11714 . . . . . 6 9 = 09
75 5cn 11292 . . . . . . . . 9 5 ∈ ℂ
7675mulid2i 10235 . . . . . . . 8 (1 · 5) = 5
7726addid2i 10416 . . . . . . . 8 (0 + 2) = 2
7876, 77oveq12i 6825 . . . . . . 7 ((1 · 5) + (0 + 2)) = (5 + 2)
79 5p2e7 11357 . . . . . . 7 (5 + 2) = 7
8078, 79eqtri 2782 . . . . . 6 ((1 · 5) + (0 + 2)) = 7
81 5t4e20 11829 . . . . . . . 8 (5 · 4) = 20
8275, 56, 81mulcomli 10239 . . . . . . 7 (4 · 5) = 20
83 9cn 11300 . . . . . . . 8 9 ∈ ℂ
8483addid2i 10416 . . . . . . 7 (0 + 9) = 9
853, 22, 35, 82, 84decaddi 11771 . . . . . 6 ((4 · 5) + 9) = 29
862, 13, 22, 35, 44, 74, 5, 35, 3, 80, 85decmac 11758 . . . . 5 ((14 · 5) + 9) = 79
874, 5, 35, 35, 37, 42, 14, 35, 11, 73, 86decma2c 11760 . . . 4 ((14 · 125) + (87 + 12)) = 1849
8883mulid2i 10235 . . . . . . . . 9 (1 · 9) = 9
8988oveq1i 6823 . . . . . . . 8 ((1 · 9) + 3) = (9 + 3)
90 9p3e12 11813 . . . . . . . 8 (9 + 3) = 12
9189, 90eqtri 2782 . . . . . . 7 ((1 · 9) + 3) = 12
92 9t4e36 11857 . . . . . . . 8 (9 · 4) = 36
9383, 56, 92mulcomli 10239 . . . . . . 7 (4 · 9) = 36
9435, 2, 13, 44, 18, 16, 91, 93decmul1c 11779 . . . . . 6 (14 · 9) = 126
9594oveq1i 6823 . . . . 5 ((14 · 9) + 0) = (126 + 0)
964, 18deccl 11704 . . . . . . 7 126 ∈ ℕ0
9796nn0cni 11496 . . . . . 6 126 ∈ ℂ
9897addid1i 10415 . . . . 5 (126 + 0) = 126
9995, 98eqtri 2782 . . . 4 ((14 · 9) + 0) = 126
1006, 35, 21, 22, 1, 36, 14, 18, 4, 87, 99decma2c 11760 . . 3 ((14 · 𝑁) + 870) = 18496
101 eqid 2760 . . . 4 136 = 136
10220, 2deccl 11704 . . . 4 81 ∈ ℕ0
103 eqid 2760 . . . . 5 13 = 13
104 eqid 2760 . . . . 5 81 = 81
10513, 22deccl 11704 . . . . 5 40 ∈ ℕ0
106 eqid 2760 . . . . . . 7 40 = 40
10756addid2i 10416 . . . . . . 7 (0 + 4) = 4
108 8cn 11298 . . . . . . . 8 8 ∈ ℂ
109108addid1i 10415 . . . . . . 7 (8 + 0) = 8
11022, 20, 13, 22, 60, 106, 107, 109decadd 11762 . . . . . 6 (8 + 40) = 48
111 4p1e5 11346 . . . . . . . 8 (4 + 1) = 5
1125dec0h 11714 . . . . . . . 8 5 = 05
113111, 112eqtri 2782 . . . . . . 7 (4 + 1) = 05
11445mulid1i 10234 . . . . . . . . 9 (3 · 1) = 3
115114oveq1i 6823 . . . . . . . 8 ((3 · 1) + 5) = (3 + 5)
116 5p3e8 11358 . . . . . . . . 9 (5 + 3) = 8
11775, 45, 116addcomli 10420 . . . . . . . 8 (3 + 5) = 8
118115, 117, 603eqtri 2786 . . . . . . 7 ((3 · 1) + 5) = 08
1192, 16, 22, 5, 103, 113, 2, 20, 22, 55, 118decmac 11758 . . . . . 6 ((13 · 1) + (4 + 1)) = 18
120 6cn 11294 . . . . . . . . 9 6 ∈ ℂ
121120mulid1i 10234 . . . . . . . 8 (6 · 1) = 6
122121oveq1i 6823 . . . . . . 7 ((6 · 1) + 8) = (6 + 8)
123108, 120, 70addcomli 10420 . . . . . . 7 (6 + 8) = 14
124122, 123eqtri 2782 . . . . . 6 ((6 · 1) + 8) = 14
12517, 18, 13, 20, 101, 110, 2, 13, 2, 119, 124decmac 11758 . . . . 5 ((136 · 1) + (8 + 40)) = 184
1262dec0h 11714 . . . . . 6 1 = 01
12765, 126eqtri 2782 . . . . . . 7 (0 + 1) = 01
12845mulid2i 10235 . . . . . . . . 9 (1 · 3) = 3
129128, 65oveq12i 6825 . . . . . . . 8 ((1 · 3) + (0 + 1)) = (3 + 1)
130129, 47eqtri 2782 . . . . . . 7 ((1 · 3) + (0 + 1)) = 4
131 3t3e9 11372 . . . . . . . . 9 (3 · 3) = 9
132131oveq1i 6823 . . . . . . . 8 ((3 · 3) + 1) = (9 + 1)
133 9p1e10 11688 . . . . . . . 8 (9 + 1) = 10
134132, 133eqtri 2782 . . . . . . 7 ((3 · 3) + 1) = 10
1352, 16, 22, 2, 103, 127, 16, 22, 2, 130, 134decmac 11758 . . . . . 6 ((13 · 3) + (0 + 1)) = 40
136 6t3e18 11834 . . . . . . 7 (6 · 3) = 18
1372, 20, 2, 136, 40decaddi 11771 . . . . . 6 ((6 · 3) + 1) = 19
13817, 18, 22, 2, 101, 126, 16, 35, 2, 135, 137decmac 11758 . . . . 5 ((136 · 3) + 1) = 409
1392, 16, 20, 2, 103, 104, 19, 35, 105, 125, 138decma2c 11760 . . . 4 ((136 · 13) + 81) = 1849
14016dec0h 11714 . . . . . 6 3 = 03
141120mulid2i 10235 . . . . . . . 8 (1 · 6) = 6
142141, 77oveq12i 6825 . . . . . . 7 ((1 · 6) + (0 + 2)) = (6 + 2)
143 6p2e8 11361 . . . . . . 7 (6 + 2) = 8
144142, 143eqtri 2782 . . . . . 6 ((1 · 6) + (0 + 2)) = 8
145120, 45, 136mulcomli 10239 . . . . . . 7 (3 · 6) = 18
146 1p1e2 11326 . . . . . . 7 (1 + 1) = 2
147 8p3e11 11804 . . . . . . 7 (8 + 3) = 11
1482, 20, 16, 145, 146, 2, 147decaddci 11772 . . . . . 6 ((3 · 6) + 3) = 21
1492, 16, 22, 16, 103, 140, 18, 2, 3, 144, 148decmac 11758 . . . . 5 ((13 · 6) + 3) = 81
150 6t6e36 11838 . . . . 5 (6 · 6) = 36
15118, 17, 18, 101, 18, 16, 149, 150decmul1c 11779 . . . 4 (136 · 6) = 816
15219, 17, 18, 101, 18, 102, 139, 151decmul2c 11781 . . 3 (136 · 136) = 18496
153100, 152eqtr4i 2785 . 2 ((14 · 𝑁) + 870) = (136 · 136)
1549, 10, 12, 15, 19, 23, 24, 34, 153mod2xi 15975 1 ((2↑34) mod 𝑁) = (870 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6813  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133  cn 11212  2c2 11262  3c3 11263  4c4 11264  5c5 11265  6c6 11266  7c7 11267  8c8 11268  9c9 11269  cdc 11685   mod cmo 12862  cexp 13054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-sup 8513  df-inf 8514  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-rp 12026  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055
This theorem is referenced by:  1259lem3  16042  1259lem5  16044
  Copyright terms: Public domain W3C validator