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

Theorem 1259lem2 17129
Description: Lemma for 1259prm 17133. 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 12535 . . . . . 6 1 ∈ ℕ0
3 2nn0 12536 . . . . . 6 2 ∈ ℕ0
42, 3deccl 12739 . . . . 5 12 ∈ ℕ0
5 5nn0 12539 . . . . 5 5 ∈ ℕ0
64, 5deccl 12739 . . . 4 125 ∈ ℕ0
7 9nn 12357 . . . 4 9 ∈ ℕ
86, 7decnncl 12744 . . 3 1259 ∈ ℕ
91, 8eqeltri 2821 . 2 𝑁 ∈ ℕ
10 2nn 12332 . 2 2 ∈ ℕ
11 7nn0 12541 . . 3 7 ∈ ℕ0
122, 11deccl 12739 . 2 17 ∈ ℕ0
13 4nn0 12538 . . . 4 4 ∈ ℕ0
142, 13deccl 12739 . . 3 14 ∈ ℕ0
1514nn0zi 12634 . 2 14 ∈ ℤ
16 3nn0 12537 . . . 4 3 ∈ ℕ0
172, 16deccl 12739 . . 3 13 ∈ ℕ0
18 6nn0 12540 . . 3 6 ∈ ℕ0
1917, 18deccl 12739 . 2 136 ∈ ℕ0
20 8nn0 12542 . . . 4 8 ∈ ℕ0
2120, 11deccl 12739 . . 3 87 ∈ ℕ0
22 0nn0 12534 . . 3 0 ∈ ℕ0
2321, 22deccl 12739 . 2 870 ∈ ℕ0
2411259lem1 17128 . 2 ((2↑17) mod 𝑁) = (136 mod 𝑁)
25 eqid 2725 . . 3 17 = 17
26 2cn 12334 . . . . . 6 2 ∈ ℂ
2726mulridi 11264 . . . . 5 (2 · 1) = 2
2827oveq1i 7433 . . . 4 ((2 · 1) + 1) = (2 + 1)
29 2p1e3 12401 . . . 4 (2 + 1) = 3
3028, 29eqtri 2753 . . 3 ((2 · 1) + 1) = 3
31 7cn 12353 . . . 4 7 ∈ ℂ
32 7t2e14 12833 . . . 4 (7 · 2) = 14
3331, 26, 32mulcomli 11269 . . 3 (2 · 7) = 14
343, 2, 11, 25, 13, 2, 30, 33decmul2c 12790 . 2 (2 · 17) = 34
35 9nn0 12543 . . . 4 9 ∈ ℕ0
36 eqid 2725 . . . 4 870 = 870
37 eqid 2725 . . . . 5 125 = 125
38 eqid 2725 . . . . . 6 87 = 87
39 eqid 2725 . . . . . 6 12 = 12
40 8p1e9 12409 . . . . . 6 (8 + 1) = 9
41 7p2e9 12420 . . . . . 6 (7 + 2) = 9
4220, 11, 2, 3, 38, 39, 40, 41decadd 12778 . . . . 5 (87 + 12) = 99
43 9p7e16 12816 . . . . . 6 (9 + 7) = 16
44 eqid 2725 . . . . . . 7 14 = 14
45 3cn 12340 . . . . . . . . 9 3 ∈ ℂ
46 ax-1cn 11212 . . . . . . . . 9 1 ∈ ℂ
47 3p1e4 12404 . . . . . . . . 9 (3 + 1) = 4
4845, 46, 47addcomli 11452 . . . . . . . 8 (1 + 3) = 4
4913dec0h 12746 . . . . . . . 8 4 = 04
5048, 49eqtri 2753 . . . . . . 7 (1 + 3) = 04
5146mulridi 11264 . . . . . . . . 9 (1 · 1) = 1
52 00id 11435 . . . . . . . . 9 (0 + 0) = 0
5351, 52oveq12i 7435 . . . . . . . 8 ((1 · 1) + (0 + 0)) = (1 + 0)
5446addridi 11447 . . . . . . . 8 (1 + 0) = 1
5553, 54eqtri 2753 . . . . . . 7 ((1 · 1) + (0 + 0)) = 1
56 4cn 12344 . . . . . . . . . 10 4 ∈ ℂ
5756mulridi 11264 . . . . . . . . 9 (4 · 1) = 4
5857oveq1i 7433 . . . . . . . 8 ((4 · 1) + 4) = (4 + 4)
59 4p4e8 12414 . . . . . . . 8 (4 + 4) = 8
6020dec0h 12746 . . . . . . . 8 8 = 08
6158, 59, 603eqtri 2757 . . . . . . 7 ((4 · 1) + 4) = 08
622, 13, 22, 13, 44, 50, 2, 20, 22, 55, 61decmac 12776 . . . . . 6 ((14 · 1) + (1 + 3)) = 18
6318dec0h 12746 . . . . . . 7 6 = 06
6426mullidi 11265 . . . . . . . . 9 (1 · 2) = 2
6546addlidi 11448 . . . . . . . . 9 (0 + 1) = 1
6664, 65oveq12i 7435 . . . . . . . 8 ((1 · 2) + (0 + 1)) = (2 + 1)
6766, 29eqtri 2753 . . . . . . 7 ((1 · 2) + (0 + 1)) = 3
68 4t2e8 12427 . . . . . . . . 9 (4 · 2) = 8
6968oveq1i 7433 . . . . . . . 8 ((4 · 2) + 6) = (8 + 6)
70 8p6e14 12808 . . . . . . . 8 (8 + 6) = 14
7169, 70eqtri 2753 . . . . . . 7 ((4 · 2) + 6) = 14
722, 13, 22, 18, 44, 63, 3, 13, 2, 67, 71decmac 12776 . . . . . 6 ((14 · 2) + 6) = 34
732, 3, 2, 18, 39, 43, 14, 13, 16, 62, 72decma2c 12777 . . . . 5 ((14 · 12) + (9 + 7)) = 184
7435dec0h 12746 . . . . . 6 9 = 09
75 5cn 12347 . . . . . . . . 9 5 ∈ ℂ
7675mullidi 11265 . . . . . . . 8 (1 · 5) = 5
7726addlidi 11448 . . . . . . . 8 (0 + 2) = 2
7876, 77oveq12i 7435 . . . . . . 7 ((1 · 5) + (0 + 2)) = (5 + 2)
79 5p2e7 12415 . . . . . . 7 (5 + 2) = 7
8078, 79eqtri 2753 . . . . . 6 ((1 · 5) + (0 + 2)) = 7
81 5t4e20 12826 . . . . . . . 8 (5 · 4) = 20
8275, 56, 81mulcomli 11269 . . . . . . 7 (4 · 5) = 20
83 9cn 12359 . . . . . . . 8 9 ∈ ℂ
8483addlidi 11448 . . . . . . 7 (0 + 9) = 9
853, 22, 35, 82, 84decaddi 12784 . . . . . 6 ((4 · 5) + 9) = 29
862, 13, 22, 35, 44, 74, 5, 35, 3, 80, 85decmac 12776 . . . . 5 ((14 · 5) + 9) = 79
874, 5, 35, 35, 37, 42, 14, 35, 11, 73, 86decma2c 12777 . . . 4 ((14 · 125) + (87 + 12)) = 1849
8883mullidi 11265 . . . . . . . . 9 (1 · 9) = 9
8988oveq1i 7433 . . . . . . . 8 ((1 · 9) + 3) = (9 + 3)
90 9p3e12 12812 . . . . . . . 8 (9 + 3) = 12
9189, 90eqtri 2753 . . . . . . 7 ((1 · 9) + 3) = 12
92 9t4e36 12848 . . . . . . . 8 (9 · 4) = 36
9383, 56, 92mulcomli 11269 . . . . . . 7 (4 · 9) = 36
9435, 2, 13, 44, 18, 16, 91, 93decmul1c 12789 . . . . . 6 (14 · 9) = 126
9594oveq1i 7433 . . . . 5 ((14 · 9) + 0) = (126 + 0)
964, 18deccl 12739 . . . . . . 7 126 ∈ ℕ0
9796nn0cni 12531 . . . . . 6 126 ∈ ℂ
9897addridi 11447 . . . . 5 (126 + 0) = 126
9995, 98eqtri 2753 . . . 4 ((14 · 9) + 0) = 126
1006, 35, 21, 22, 1, 36, 14, 18, 4, 87, 99decma2c 12777 . . 3 ((14 · 𝑁) + 870) = 18496
101 eqid 2725 . . . 4 136 = 136
10220, 2deccl 12739 . . . 4 81 ∈ ℕ0
103 eqid 2725 . . . . 5 13 = 13
104 eqid 2725 . . . . 5 81 = 81
10513, 22deccl 12739 . . . . 5 40 ∈ ℕ0
106 eqid 2725 . . . . . . 7 40 = 40
10756addlidi 11448 . . . . . . 7 (0 + 4) = 4
108 8cn 12356 . . . . . . . 8 8 ∈ ℂ
109108addridi 11447 . . . . . . 7 (8 + 0) = 8
11022, 20, 13, 22, 60, 106, 107, 109decadd 12778 . . . . . 6 (8 + 40) = 48
111 4p1e5 12405 . . . . . . . 8 (4 + 1) = 5
1125dec0h 12746 . . . . . . . 8 5 = 05
113111, 112eqtri 2753 . . . . . . 7 (4 + 1) = 05
11445mulridi 11264 . . . . . . . . 9 (3 · 1) = 3
115114oveq1i 7433 . . . . . . . 8 ((3 · 1) + 5) = (3 + 5)
116 5p3e8 12416 . . . . . . . . 9 (5 + 3) = 8
11775, 45, 116addcomli 11452 . . . . . . . 8 (3 + 5) = 8
118115, 117, 603eqtri 2757 . . . . . . 7 ((3 · 1) + 5) = 08
1192, 16, 22, 5, 103, 113, 2, 20, 22, 55, 118decmac 12776 . . . . . 6 ((13 · 1) + (4 + 1)) = 18
120 6cn 12350 . . . . . . . . 9 6 ∈ ℂ
121120mulridi 11264 . . . . . . . 8 (6 · 1) = 6
122121oveq1i 7433 . . . . . . 7 ((6 · 1) + 8) = (6 + 8)
123108, 120, 70addcomli 11452 . . . . . . 7 (6 + 8) = 14
124122, 123eqtri 2753 . . . . . 6 ((6 · 1) + 8) = 14
12517, 18, 13, 20, 101, 110, 2, 13, 2, 119, 124decmac 12776 . . . . 5 ((136 · 1) + (8 + 40)) = 184
1262dec0h 12746 . . . . . 6 1 = 01
12765, 126eqtri 2753 . . . . . . 7 (0 + 1) = 01
12845mullidi 11265 . . . . . . . . 9 (1 · 3) = 3
129128, 65oveq12i 7435 . . . . . . . 8 ((1 · 3) + (0 + 1)) = (3 + 1)
130129, 47eqtri 2753 . . . . . . 7 ((1 · 3) + (0 + 1)) = 4
131 3t3e9 12426 . . . . . . . . 9 (3 · 3) = 9
132131oveq1i 7433 . . . . . . . 8 ((3 · 3) + 1) = (9 + 1)
133 9p1e10 12726 . . . . . . . 8 (9 + 1) = 10
134132, 133eqtri 2753 . . . . . . 7 ((3 · 3) + 1) = 10
1352, 16, 22, 2, 103, 127, 16, 22, 2, 130, 134decmac 12776 . . . . . 6 ((13 · 3) + (0 + 1)) = 40
136 6t3e18 12829 . . . . . . 7 (6 · 3) = 18
1372, 20, 2, 136, 40decaddi 12784 . . . . . 6 ((6 · 3) + 1) = 19
13817, 18, 22, 2, 101, 126, 16, 35, 2, 135, 137decmac 12776 . . . . 5 ((136 · 3) + 1) = 409
1392, 16, 20, 2, 103, 104, 19, 35, 105, 125, 138decma2c 12777 . . . 4 ((136 · 13) + 81) = 1849
14016dec0h 12746 . . . . . 6 3 = 03
141120mullidi 11265 . . . . . . . 8 (1 · 6) = 6
142141, 77oveq12i 7435 . . . . . . 7 ((1 · 6) + (0 + 2)) = (6 + 2)
143 6p2e8 12418 . . . . . . 7 (6 + 2) = 8
144142, 143eqtri 2753 . . . . . 6 ((1 · 6) + (0 + 2)) = 8
145120, 45, 136mulcomli 11269 . . . . . . 7 (3 · 6) = 18
146 1p1e2 12384 . . . . . . 7 (1 + 1) = 2
147 8p3e11 12805 . . . . . . 7 (8 + 3) = 11
1482, 20, 16, 145, 146, 2, 147decaddci 12785 . . . . . 6 ((3 · 6) + 3) = 21
1492, 16, 22, 16, 103, 140, 18, 2, 3, 144, 148decmac 12776 . . . . 5 ((13 · 6) + 3) = 81
150 6t6e36 12832 . . . . 5 (6 · 6) = 36
15118, 17, 18, 101, 18, 16, 149, 150decmul1c 12789 . . . 4 (136 · 6) = 816
15219, 17, 18, 101, 18, 102, 139, 151decmul2c 12790 . . 3 (136 · 136) = 18496
153100, 152eqtr4i 2756 . 2 ((14 · 𝑁) + 870) = (136 · 136)
1549, 10, 12, 15, 19, 23, 24, 34, 153mod2xi 17066 1 ((2↑34) mod 𝑁) = (870 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  (class class class)co 7423  0cc0 11154  1c1 11155   + caddc 11157   · cmul 11159  cn 12259  2c2 12314  3c3 12315  4c4 12316  5c5 12317  6c6 12318  7c7 12319  8c8 12320  9c9 12321  cdc 12724   mod cmo 13884  cexp 14076
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-en 8974  df-dom 8975  df-sdom 8976  df-sup 9481  df-inf 9482  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328  df-9 12329  df-n0 12520  df-z 12606  df-dec 12725  df-uz 12870  df-rp 13024  df-fl 13807  df-mod 13885  df-seq 14017  df-exp 14077
This theorem is referenced by:  1259lem3  17130  1259lem5  17132
  Copyright terms: Public domain W3C validator