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

Theorem 1259lem2 17110
Description: Lemma for 1259prm 17114. 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 12528 . . . . . 6 1 ∈ ℕ0
3 2nn0 12529 . . . . . 6 2 ∈ ℕ0
42, 3deccl 12732 . . . . 5 12 ∈ ℕ0
5 5nn0 12532 . . . . 5 5 ∈ ℕ0
64, 5deccl 12732 . . . 4 125 ∈ ℕ0
7 9nn 12350 . . . 4 9 ∈ ℕ
86, 7decnncl 12737 . . 3 1259 ∈ ℕ
91, 8eqeltri 2825 . 2 𝑁 ∈ ℕ
10 2nn 12325 . 2 2 ∈ ℕ
11 7nn0 12534 . . 3 7 ∈ ℕ0
122, 11deccl 12732 . 2 17 ∈ ℕ0
13 4nn0 12531 . . . 4 4 ∈ ℕ0
142, 13deccl 12732 . . 3 14 ∈ ℕ0
1514nn0zi 12627 . 2 14 ∈ ℤ
16 3nn0 12530 . . . 4 3 ∈ ℕ0
172, 16deccl 12732 . . 3 13 ∈ ℕ0
18 6nn0 12533 . . 3 6 ∈ ℕ0
1917, 18deccl 12732 . 2 136 ∈ ℕ0
20 8nn0 12535 . . . 4 8 ∈ ℕ0
2120, 11deccl 12732 . . 3 87 ∈ ℕ0
22 0nn0 12527 . . 3 0 ∈ ℕ0
2321, 22deccl 12732 . 2 870 ∈ ℕ0
2411259lem1 17109 . 2 ((2↑17) mod 𝑁) = (136 mod 𝑁)
25 eqid 2728 . . 3 17 = 17
26 2cn 12327 . . . . . 6 2 ∈ ℂ
2726mulridi 11258 . . . . 5 (2 · 1) = 2
2827oveq1i 7436 . . . 4 ((2 · 1) + 1) = (2 + 1)
29 2p1e3 12394 . . . 4 (2 + 1) = 3
3028, 29eqtri 2756 . . 3 ((2 · 1) + 1) = 3
31 7cn 12346 . . . 4 7 ∈ ℂ
32 7t2e14 12826 . . . 4 (7 · 2) = 14
3331, 26, 32mulcomli 11263 . . 3 (2 · 7) = 14
343, 2, 11, 25, 13, 2, 30, 33decmul2c 12783 . 2 (2 · 17) = 34
35 9nn0 12536 . . . 4 9 ∈ ℕ0
36 eqid 2728 . . . 4 870 = 870
37 eqid 2728 . . . . 5 125 = 125
38 eqid 2728 . . . . . 6 87 = 87
39 eqid 2728 . . . . . 6 12 = 12
40 8p1e9 12402 . . . . . 6 (8 + 1) = 9
41 7p2e9 12413 . . . . . 6 (7 + 2) = 9
4220, 11, 2, 3, 38, 39, 40, 41decadd 12771 . . . . 5 (87 + 12) = 99
43 9p7e16 12809 . . . . . 6 (9 + 7) = 16
44 eqid 2728 . . . . . . 7 14 = 14
45 3cn 12333 . . . . . . . . 9 3 ∈ ℂ
46 ax-1cn 11206 . . . . . . . . 9 1 ∈ ℂ
47 3p1e4 12397 . . . . . . . . 9 (3 + 1) = 4
4845, 46, 47addcomli 11446 . . . . . . . 8 (1 + 3) = 4
4913dec0h 12739 . . . . . . . 8 4 = 04
5048, 49eqtri 2756 . . . . . . 7 (1 + 3) = 04
5146mulridi 11258 . . . . . . . . 9 (1 · 1) = 1
52 00id 11429 . . . . . . . . 9 (0 + 0) = 0
5351, 52oveq12i 7438 . . . . . . . 8 ((1 · 1) + (0 + 0)) = (1 + 0)
5446addridi 11441 . . . . . . . 8 (1 + 0) = 1
5553, 54eqtri 2756 . . . . . . 7 ((1 · 1) + (0 + 0)) = 1
56 4cn 12337 . . . . . . . . . 10 4 ∈ ℂ
5756mulridi 11258 . . . . . . . . 9 (4 · 1) = 4
5857oveq1i 7436 . . . . . . . 8 ((4 · 1) + 4) = (4 + 4)
59 4p4e8 12407 . . . . . . . 8 (4 + 4) = 8
6020dec0h 12739 . . . . . . . 8 8 = 08
6158, 59, 603eqtri 2760 . . . . . . 7 ((4 · 1) + 4) = 08
622, 13, 22, 13, 44, 50, 2, 20, 22, 55, 61decmac 12769 . . . . . 6 ((14 · 1) + (1 + 3)) = 18
6318dec0h 12739 . . . . . . 7 6 = 06
6426mullidi 11259 . . . . . . . . 9 (1 · 2) = 2
6546addlidi 11442 . . . . . . . . 9 (0 + 1) = 1
6664, 65oveq12i 7438 . . . . . . . 8 ((1 · 2) + (0 + 1)) = (2 + 1)
6766, 29eqtri 2756 . . . . . . 7 ((1 · 2) + (0 + 1)) = 3
68 4t2e8 12420 . . . . . . . . 9 (4 · 2) = 8
6968oveq1i 7436 . . . . . . . 8 ((4 · 2) + 6) = (8 + 6)
70 8p6e14 12801 . . . . . . . 8 (8 + 6) = 14
7169, 70eqtri 2756 . . . . . . 7 ((4 · 2) + 6) = 14
722, 13, 22, 18, 44, 63, 3, 13, 2, 67, 71decmac 12769 . . . . . 6 ((14 · 2) + 6) = 34
732, 3, 2, 18, 39, 43, 14, 13, 16, 62, 72decma2c 12770 . . . . 5 ((14 · 12) + (9 + 7)) = 184
7435dec0h 12739 . . . . . 6 9 = 09
75 5cn 12340 . . . . . . . . 9 5 ∈ ℂ
7675mullidi 11259 . . . . . . . 8 (1 · 5) = 5
7726addlidi 11442 . . . . . . . 8 (0 + 2) = 2
7876, 77oveq12i 7438 . . . . . . 7 ((1 · 5) + (0 + 2)) = (5 + 2)
79 5p2e7 12408 . . . . . . 7 (5 + 2) = 7
8078, 79eqtri 2756 . . . . . 6 ((1 · 5) + (0 + 2)) = 7
81 5t4e20 12819 . . . . . . . 8 (5 · 4) = 20
8275, 56, 81mulcomli 11263 . . . . . . 7 (4 · 5) = 20
83 9cn 12352 . . . . . . . 8 9 ∈ ℂ
8483addlidi 11442 . . . . . . 7 (0 + 9) = 9
853, 22, 35, 82, 84decaddi 12777 . . . . . 6 ((4 · 5) + 9) = 29
862, 13, 22, 35, 44, 74, 5, 35, 3, 80, 85decmac 12769 . . . . 5 ((14 · 5) + 9) = 79
874, 5, 35, 35, 37, 42, 14, 35, 11, 73, 86decma2c 12770 . . . 4 ((14 · 125) + (87 + 12)) = 1849
8883mullidi 11259 . . . . . . . . 9 (1 · 9) = 9
8988oveq1i 7436 . . . . . . . 8 ((1 · 9) + 3) = (9 + 3)
90 9p3e12 12805 . . . . . . . 8 (9 + 3) = 12
9189, 90eqtri 2756 . . . . . . 7 ((1 · 9) + 3) = 12
92 9t4e36 12841 . . . . . . . 8 (9 · 4) = 36
9383, 56, 92mulcomli 11263 . . . . . . 7 (4 · 9) = 36
9435, 2, 13, 44, 18, 16, 91, 93decmul1c 12782 . . . . . 6 (14 · 9) = 126
9594oveq1i 7436 . . . . 5 ((14 · 9) + 0) = (126 + 0)
964, 18deccl 12732 . . . . . . 7 126 ∈ ℕ0
9796nn0cni 12524 . . . . . 6 126 ∈ ℂ
9897addridi 11441 . . . . 5 (126 + 0) = 126
9995, 98eqtri 2756 . . . 4 ((14 · 9) + 0) = 126
1006, 35, 21, 22, 1, 36, 14, 18, 4, 87, 99decma2c 12770 . . 3 ((14 · 𝑁) + 870) = 18496
101 eqid 2728 . . . 4 136 = 136
10220, 2deccl 12732 . . . 4 81 ∈ ℕ0
103 eqid 2728 . . . . 5 13 = 13
104 eqid 2728 . . . . 5 81 = 81
10513, 22deccl 12732 . . . . 5 40 ∈ ℕ0
106 eqid 2728 . . . . . . 7 40 = 40
10756addlidi 11442 . . . . . . 7 (0 + 4) = 4
108 8cn 12349 . . . . . . . 8 8 ∈ ℂ
109108addridi 11441 . . . . . . 7 (8 + 0) = 8
11022, 20, 13, 22, 60, 106, 107, 109decadd 12771 . . . . . 6 (8 + 40) = 48
111 4p1e5 12398 . . . . . . . 8 (4 + 1) = 5
1125dec0h 12739 . . . . . . . 8 5 = 05
113111, 112eqtri 2756 . . . . . . 7 (4 + 1) = 05
11445mulridi 11258 . . . . . . . . 9 (3 · 1) = 3
115114oveq1i 7436 . . . . . . . 8 ((3 · 1) + 5) = (3 + 5)
116 5p3e8 12409 . . . . . . . . 9 (5 + 3) = 8
11775, 45, 116addcomli 11446 . . . . . . . 8 (3 + 5) = 8
118115, 117, 603eqtri 2760 . . . . . . 7 ((3 · 1) + 5) = 08
1192, 16, 22, 5, 103, 113, 2, 20, 22, 55, 118decmac 12769 . . . . . 6 ((13 · 1) + (4 + 1)) = 18
120 6cn 12343 . . . . . . . . 9 6 ∈ ℂ
121120mulridi 11258 . . . . . . . 8 (6 · 1) = 6
122121oveq1i 7436 . . . . . . 7 ((6 · 1) + 8) = (6 + 8)
123108, 120, 70addcomli 11446 . . . . . . 7 (6 + 8) = 14
124122, 123eqtri 2756 . . . . . 6 ((6 · 1) + 8) = 14
12517, 18, 13, 20, 101, 110, 2, 13, 2, 119, 124decmac 12769 . . . . 5 ((136 · 1) + (8 + 40)) = 184
1262dec0h 12739 . . . . . 6 1 = 01
12765, 126eqtri 2756 . . . . . . 7 (0 + 1) = 01
12845mullidi 11259 . . . . . . . . 9 (1 · 3) = 3
129128, 65oveq12i 7438 . . . . . . . 8 ((1 · 3) + (0 + 1)) = (3 + 1)
130129, 47eqtri 2756 . . . . . . 7 ((1 · 3) + (0 + 1)) = 4
131 3t3e9 12419 . . . . . . . . 9 (3 · 3) = 9
132131oveq1i 7436 . . . . . . . 8 ((3 · 3) + 1) = (9 + 1)
133 9p1e10 12719 . . . . . . . 8 (9 + 1) = 10
134132, 133eqtri 2756 . . . . . . 7 ((3 · 3) + 1) = 10
1352, 16, 22, 2, 103, 127, 16, 22, 2, 130, 134decmac 12769 . . . . . 6 ((13 · 3) + (0 + 1)) = 40
136 6t3e18 12822 . . . . . . 7 (6 · 3) = 18
1372, 20, 2, 136, 40decaddi 12777 . . . . . 6 ((6 · 3) + 1) = 19
13817, 18, 22, 2, 101, 126, 16, 35, 2, 135, 137decmac 12769 . . . . 5 ((136 · 3) + 1) = 409
1392, 16, 20, 2, 103, 104, 19, 35, 105, 125, 138decma2c 12770 . . . 4 ((136 · 13) + 81) = 1849
14016dec0h 12739 . . . . . 6 3 = 03
141120mullidi 11259 . . . . . . . 8 (1 · 6) = 6
142141, 77oveq12i 7438 . . . . . . 7 ((1 · 6) + (0 + 2)) = (6 + 2)
143 6p2e8 12411 . . . . . . 7 (6 + 2) = 8
144142, 143eqtri 2756 . . . . . 6 ((1 · 6) + (0 + 2)) = 8
145120, 45, 136mulcomli 11263 . . . . . . 7 (3 · 6) = 18
146 1p1e2 12377 . . . . . . 7 (1 + 1) = 2
147 8p3e11 12798 . . . . . . 7 (8 + 3) = 11
1482, 20, 16, 145, 146, 2, 147decaddci 12778 . . . . . 6 ((3 · 6) + 3) = 21
1492, 16, 22, 16, 103, 140, 18, 2, 3, 144, 148decmac 12769 . . . . 5 ((13 · 6) + 3) = 81
150 6t6e36 12825 . . . . 5 (6 · 6) = 36
15118, 17, 18, 101, 18, 16, 149, 150decmul1c 12782 . . . 4 (136 · 6) = 816
15219, 17, 18, 101, 18, 102, 139, 151decmul2c 12783 . . 3 (136 · 136) = 18496
153100, 152eqtr4i 2759 . 2 ((14 · 𝑁) + 870) = (136 · 136)
1549, 10, 12, 15, 19, 23, 24, 34, 153mod2xi 17047 1 ((2↑34) mod 𝑁) = (870 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  (class class class)co 7426  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153  cn 12252  2c2 12307  3c3 12308  4c4 12309  5c5 12310  6c6 12311  7c7 12312  8c8 12313  9c9 12314  cdc 12717   mod cmo 13876  cexp 14068
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 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226
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 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  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 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  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 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-en 8973  df-dom 8974  df-sdom 8975  df-sup 9475  df-inf 9476  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-z 12599  df-dec 12718  df-uz 12863  df-rp 13017  df-fl 13799  df-mod 13877  df-seq 14009  df-exp 14069
This theorem is referenced by:  1259lem3  17111  1259lem5  17113
  Copyright terms: Public domain W3C validator