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

Theorem 1259lem2 16037
Description: Lemma for 1259prm 16041. 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 11496 . . . . . 6 1 ∈ ℕ0
3 2nn0 11497 . . . . . 6 2 ∈ ℕ0
42, 3deccl 11700 . . . . 5 12 ∈ ℕ0
5 5nn0 11500 . . . . 5 5 ∈ ℕ0
64, 5deccl 11700 . . . 4 125 ∈ ℕ0
7 9nn 11380 . . . 4 9 ∈ ℕ
86, 7decnncl 11706 . . 3 1259 ∈ ℕ
91, 8eqeltri 2831 . 2 𝑁 ∈ ℕ
10 2nn 11373 . 2 2 ∈ ℕ
11 7nn0 11502 . . 3 7 ∈ ℕ0
122, 11deccl 11700 . 2 17 ∈ ℕ0
13 4nn0 11499 . . . 4 4 ∈ ℕ0
142, 13deccl 11700 . . 3 14 ∈ ℕ0
1514nn0zi 11590 . 2 14 ∈ ℤ
16 3nn0 11498 . . . 4 3 ∈ ℕ0
172, 16deccl 11700 . . 3 13 ∈ ℕ0
18 6nn0 11501 . . 3 6 ∈ ℕ0
1917, 18deccl 11700 . 2 136 ∈ ℕ0
20 8nn0 11503 . . . 4 8 ∈ ℕ0
2120, 11deccl 11700 . . 3 87 ∈ ℕ0
22 0nn0 11495 . . 3 0 ∈ ℕ0
2321, 22deccl 11700 . 2 870 ∈ ℕ0
2411259lem1 16036 . 2 ((2↑17) mod 𝑁) = (136 mod 𝑁)
25 eqid 2756 . . 3 17 = 17
26 2cn 11279 . . . . . 6 2 ∈ ℂ
2726mulid1i 10230 . . . . 5 (2 · 1) = 2
2827oveq1i 6819 . . . 4 ((2 · 1) + 1) = (2 + 1)
29 2p1e3 11339 . . . 4 (2 + 1) = 3
3028, 29eqtri 2778 . . 3 ((2 · 1) + 1) = 3
31 7cn 11292 . . . 4 7 ∈ ℂ
32 7t2e14 11836 . . . 4 (7 · 2) = 14
3331, 26, 32mulcomli 10235 . . 3 (2 · 7) = 14
343, 2, 11, 25, 13, 2, 30, 33decmul2c 11777 . 2 (2 · 17) = 34
35 9nn0 11504 . . . 4 9 ∈ ℕ0
36 eqid 2756 . . . 4 870 = 870
37 eqid 2756 . . . . 5 125 = 125
38 eqid 2756 . . . . . 6 87 = 87
39 eqid 2756 . . . . . 6 12 = 12
40 8p1e9 11346 . . . . . 6 (8 + 1) = 9
41 7p2e9 11360 . . . . . 6 (7 + 2) = 9
4220, 11, 2, 3, 38, 39, 40, 41decadd 11758 . . . . 5 (87 + 12) = 99
43 9p7e16 11813 . . . . . 6 (9 + 7) = 16
44 eqid 2756 . . . . . . 7 14 = 14
45 3cn 11283 . . . . . . . . 9 3 ∈ ℂ
46 ax-1cn 10182 . . . . . . . . 9 1 ∈ ℂ
47 3p1e4 11341 . . . . . . . . 9 (3 + 1) = 4
4845, 46, 47addcomli 10416 . . . . . . . 8 (1 + 3) = 4
4913dec0h 11710 . . . . . . . 8 4 = 04
5048, 49eqtri 2778 . . . . . . 7 (1 + 3) = 04
5146mulid1i 10230 . . . . . . . . 9 (1 · 1) = 1
52 00id 10399 . . . . . . . . 9 (0 + 0) = 0
5351, 52oveq12i 6821 . . . . . . . 8 ((1 · 1) + (0 + 0)) = (1 + 0)
5446addid1i 10411 . . . . . . . 8 (1 + 0) = 1
5553, 54eqtri 2778 . . . . . . 7 ((1 · 1) + (0 + 0)) = 1
56 4cn 11286 . . . . . . . . . 10 4 ∈ ℂ
5756mulid1i 10230 . . . . . . . . 9 (4 · 1) = 4
5857oveq1i 6819 . . . . . . . 8 ((4 · 1) + 4) = (4 + 4)
59 4p4e8 11352 . . . . . . . 8 (4 + 4) = 8
6020dec0h 11710 . . . . . . . 8 8 = 08
6158, 59, 603eqtri 2782 . . . . . . 7 ((4 · 1) + 4) = 08
622, 13, 22, 13, 44, 50, 2, 20, 22, 55, 61decmac 11754 . . . . . 6 ((14 · 1) + (1 + 3)) = 18
6318dec0h 11710 . . . . . . 7 6 = 06
6426mulid2i 10231 . . . . . . . . 9 (1 · 2) = 2
6546addid2i 10412 . . . . . . . . 9 (0 + 1) = 1
6664, 65oveq12i 6821 . . . . . . . 8 ((1 · 2) + (0 + 1)) = (2 + 1)
6766, 29eqtri 2778 . . . . . . 7 ((1 · 2) + (0 + 1)) = 3
68 4t2e8 11369 . . . . . . . . 9 (4 · 2) = 8
6968oveq1i 6819 . . . . . . . 8 ((4 · 2) + 6) = (8 + 6)
70 8p6e14 11804 . . . . . . . 8 (8 + 6) = 14
7169, 70eqtri 2778 . . . . . . 7 ((4 · 2) + 6) = 14
722, 13, 22, 18, 44, 63, 3, 13, 2, 67, 71decmac 11754 . . . . . 6 ((14 · 2) + 6) = 34
732, 3, 2, 18, 39, 43, 14, 13, 16, 62, 72decma2c 11756 . . . . 5 ((14 · 12) + (9 + 7)) = 184
7435dec0h 11710 . . . . . 6 9 = 09
75 5cn 11288 . . . . . . . . 9 5 ∈ ℂ
7675mulid2i 10231 . . . . . . . 8 (1 · 5) = 5
7726addid2i 10412 . . . . . . . 8 (0 + 2) = 2
7876, 77oveq12i 6821 . . . . . . 7 ((1 · 5) + (0 + 2)) = (5 + 2)
79 5p2e7 11353 . . . . . . 7 (5 + 2) = 7
8078, 79eqtri 2778 . . . . . 6 ((1 · 5) + (0 + 2)) = 7
81 5t4e20 11825 . . . . . . . 8 (5 · 4) = 20
8275, 56, 81mulcomli 10235 . . . . . . 7 (4 · 5) = 20
83 9cn 11296 . . . . . . . 8 9 ∈ ℂ
8483addid2i 10412 . . . . . . 7 (0 + 9) = 9
853, 22, 35, 82, 84decaddi 11767 . . . . . 6 ((4 · 5) + 9) = 29
862, 13, 22, 35, 44, 74, 5, 35, 3, 80, 85decmac 11754 . . . . 5 ((14 · 5) + 9) = 79
874, 5, 35, 35, 37, 42, 14, 35, 11, 73, 86decma2c 11756 . . . 4 ((14 · 125) + (87 + 12)) = 1849
8883mulid2i 10231 . . . . . . . . 9 (1 · 9) = 9
8988oveq1i 6819 . . . . . . . 8 ((1 · 9) + 3) = (9 + 3)
90 9p3e12 11809 . . . . . . . 8 (9 + 3) = 12
9189, 90eqtri 2778 . . . . . . 7 ((1 · 9) + 3) = 12
92 9t4e36 11853 . . . . . . . 8 (9 · 4) = 36
9383, 56, 92mulcomli 10235 . . . . . . 7 (4 · 9) = 36
9435, 2, 13, 44, 18, 16, 91, 93decmul1c 11775 . . . . . 6 (14 · 9) = 126
9594oveq1i 6819 . . . . 5 ((14 · 9) + 0) = (126 + 0)
964, 18deccl 11700 . . . . . . 7 126 ∈ ℕ0
9796nn0cni 11492 . . . . . 6 126 ∈ ℂ
9897addid1i 10411 . . . . 5 (126 + 0) = 126
9995, 98eqtri 2778 . . . 4 ((14 · 9) + 0) = 126
1006, 35, 21, 22, 1, 36, 14, 18, 4, 87, 99decma2c 11756 . . 3 ((14 · 𝑁) + 870) = 18496
101 eqid 2756 . . . 4 136 = 136
10220, 2deccl 11700 . . . 4 81 ∈ ℕ0
103 eqid 2756 . . . . 5 13 = 13
104 eqid 2756 . . . . 5 81 = 81
10513, 22deccl 11700 . . . . 5 40 ∈ ℕ0
106 eqid 2756 . . . . . . 7 40 = 40
10756addid2i 10412 . . . . . . 7 (0 + 4) = 4
108 8cn 11294 . . . . . . . 8 8 ∈ ℂ
109108addid1i 10411 . . . . . . 7 (8 + 0) = 8
11022, 20, 13, 22, 60, 106, 107, 109decadd 11758 . . . . . 6 (8 + 40) = 48
111 4p1e5 11342 . . . . . . . 8 (4 + 1) = 5
1125dec0h 11710 . . . . . . . 8 5 = 05
113111, 112eqtri 2778 . . . . . . 7 (4 + 1) = 05
11445mulid1i 10230 . . . . . . . . 9 (3 · 1) = 3
115114oveq1i 6819 . . . . . . . 8 ((3 · 1) + 5) = (3 + 5)
116 5p3e8 11354 . . . . . . . . 9 (5 + 3) = 8
11775, 45, 116addcomli 10416 . . . . . . . 8 (3 + 5) = 8
118115, 117, 603eqtri 2782 . . . . . . 7 ((3 · 1) + 5) = 08
1192, 16, 22, 5, 103, 113, 2, 20, 22, 55, 118decmac 11754 . . . . . 6 ((13 · 1) + (4 + 1)) = 18
120 6cn 11290 . . . . . . . . 9 6 ∈ ℂ
121120mulid1i 10230 . . . . . . . 8 (6 · 1) = 6
122121oveq1i 6819 . . . . . . 7 ((6 · 1) + 8) = (6 + 8)
123108, 120, 70addcomli 10416 . . . . . . 7 (6 + 8) = 14
124122, 123eqtri 2778 . . . . . 6 ((6 · 1) + 8) = 14
12517, 18, 13, 20, 101, 110, 2, 13, 2, 119, 124decmac 11754 . . . . 5 ((136 · 1) + (8 + 40)) = 184
1262dec0h 11710 . . . . . 6 1 = 01
12765, 126eqtri 2778 . . . . . . 7 (0 + 1) = 01
12845mulid2i 10231 . . . . . . . . 9 (1 · 3) = 3
129128, 65oveq12i 6821 . . . . . . . 8 ((1 · 3) + (0 + 1)) = (3 + 1)
130129, 47eqtri 2778 . . . . . . 7 ((1 · 3) + (0 + 1)) = 4
131 3t3e9 11368 . . . . . . . . 9 (3 · 3) = 9
132131oveq1i 6819 . . . . . . . 8 ((3 · 3) + 1) = (9 + 1)
133 9p1e10 11684 . . . . . . . 8 (9 + 1) = 10
134132, 133eqtri 2778 . . . . . . 7 ((3 · 3) + 1) = 10
1352, 16, 22, 2, 103, 127, 16, 22, 2, 130, 134decmac 11754 . . . . . 6 ((13 · 3) + (0 + 1)) = 40
136 6t3e18 11830 . . . . . . 7 (6 · 3) = 18
1372, 20, 2, 136, 40decaddi 11767 . . . . . 6 ((6 · 3) + 1) = 19
13817, 18, 22, 2, 101, 126, 16, 35, 2, 135, 137decmac 11754 . . . . 5 ((136 · 3) + 1) = 409
1392, 16, 20, 2, 103, 104, 19, 35, 105, 125, 138decma2c 11756 . . . 4 ((136 · 13) + 81) = 1849
14016dec0h 11710 . . . . . 6 3 = 03
141120mulid2i 10231 . . . . . . . 8 (1 · 6) = 6
142141, 77oveq12i 6821 . . . . . . 7 ((1 · 6) + (0 + 2)) = (6 + 2)
143 6p2e8 11357 . . . . . . 7 (6 + 2) = 8
144142, 143eqtri 2778 . . . . . 6 ((1 · 6) + (0 + 2)) = 8
145120, 45, 136mulcomli 10235 . . . . . . 7 (3 · 6) = 18
146 1p1e2 11322 . . . . . . 7 (1 + 1) = 2
147 8p3e11 11800 . . . . . . 7 (8 + 3) = 11
1482, 20, 16, 145, 146, 2, 147decaddci 11768 . . . . . 6 ((3 · 6) + 3) = 21
1492, 16, 22, 16, 103, 140, 18, 2, 3, 144, 148decmac 11754 . . . . 5 ((13 · 6) + 3) = 81
150 6t6e36 11834 . . . . 5 (6 · 6) = 36
15118, 17, 18, 101, 18, 16, 149, 150decmul1c 11775 . . . 4 (136 · 6) = 816
15219, 17, 18, 101, 18, 102, 139, 151decmul2c 11777 . . 3 (136 · 136) = 18496
153100, 152eqtr4i 2781 . 2 ((14 · 𝑁) + 870) = (136 · 136)
1549, 10, 12, 15, 19, 23, 24, 34, 153mod2xi 15971 1 ((2↑34) mod 𝑁) = (870 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1628  (class class class)co 6809  0cc0 10124  1c1 10125   + caddc 10127   · cmul 10129  cn 11208  2c2 11258  3c3 11259  4c4 11260  5c5 11261  6c6 11262  7c7 11263  8c8 11264  9c9 11265  cdc 11681   mod cmo 12858  cexp 13050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201  ax-pre-sup 10202
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-sup 8509  df-inf 8510  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-nn 11209  df-2 11267  df-3 11268  df-4 11269  df-5 11270  df-6 11271  df-7 11272  df-8 11273  df-9 11274  df-n0 11481  df-z 11566  df-dec 11682  df-uz 11876  df-rp 12022  df-fl 12783  df-mod 12859  df-seq 12992  df-exp 13051
This theorem is referenced by:  1259lem3  16038  1259lem5  16040
  Copyright terms: Public domain W3C validator