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

Theorem 1259lem1 15819
Description: Lemma for 1259prm 15824. Calculate a power mod. In decimal, we calculate 2↑16 = 52𝑁 + 68≡68 and 2↑17≡68 · 2 = 136 in this lemma. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
1259prm.1 𝑁 = 1259
Assertion
Ref Expression
1259lem1 ((2↑17) mod 𝑁) = (136 mod 𝑁)

Proof of Theorem 1259lem1
StepHypRef Expression
1 1259prm.1 . . 3 𝑁 = 1259
2 1nn0 11293 . . . . . 6 1 ∈ ℕ0
3 2nn0 11294 . . . . . 6 2 ∈ ℕ0
42, 3deccl 11497 . . . . 5 12 ∈ ℕ0
5 5nn0 11297 . . . . 5 5 ∈ ℕ0
64, 5deccl 11497 . . . 4 125 ∈ ℕ0
7 9nn 11177 . . . 4 9 ∈ ℕ
86, 7decnncl 11503 . . 3 1259 ∈ ℕ
91, 8eqeltri 2695 . 2 𝑁 ∈ ℕ
10 2nn 11170 . 2 2 ∈ ℕ
11 6nn0 11298 . . 3 6 ∈ ℕ0
122, 11deccl 11497 . 2 16 ∈ ℕ0
13 0z 11373 . 2 0 ∈ ℤ
14 8nn0 11300 . . 3 8 ∈ ℕ0
1511, 14deccl 11497 . 2 68 ∈ ℕ0
16 3nn0 11295 . . . 4 3 ∈ ℕ0
172, 16deccl 11497 . . 3 13 ∈ ℕ0
1817, 11deccl 11497 . 2 136 ∈ ℕ0
195, 3deccl 11497 . . . 4 52 ∈ ℕ0
2019nn0zi 11387 . . 3 52 ∈ ℤ
213, 14nn0expcli 12869 . . 3 (2↑8) ∈ ℕ0
22 eqid 2620 . . 3 ((2↑8) mod 𝑁) = ((2↑8) mod 𝑁)
2314nn0cni 11289 . . . 4 8 ∈ ℂ
24 2cn 11076 . . . 4 2 ∈ ℂ
25 8t2e16 11639 . . . 4 (8 · 2) = 16
2623, 24, 25mulcomli 10032 . . 3 (2 · 8) = 16
27 9nn0 11301 . . . . 5 9 ∈ ℕ0
28 eqid 2620 . . . . 5 68 = 68
29 4nn0 11296 . . . . . 6 4 ∈ ℕ0
30 7nn0 11299 . . . . . 6 7 ∈ ℕ0
3129, 30deccl 11497 . . . . 5 47 ∈ ℕ0
32 eqid 2620 . . . . . 6 125 = 125
33 0nn0 11292 . . . . . . 7 0 ∈ ℕ0
3411dec0h 11507 . . . . . . 7 6 = 06
35 eqid 2620 . . . . . . 7 47 = 47
36 4cn 11083 . . . . . . . . . 10 4 ∈ ℂ
3736addid2i 10209 . . . . . . . . 9 (0 + 4) = 4
3837oveq1i 6645 . . . . . . . 8 ((0 + 4) + 1) = (4 + 1)
39 4p1e5 11139 . . . . . . . 8 (4 + 1) = 5
4038, 39eqtri 2642 . . . . . . 7 ((0 + 4) + 1) = 5
41 7cn 11089 . . . . . . . 8 7 ∈ ℂ
42 6cn 11087 . . . . . . . 8 6 ∈ ℂ
43 7p6e13 11593 . . . . . . . 8 (7 + 6) = 13
4441, 42, 43addcomli 10213 . . . . . . 7 (6 + 7) = 13
4533, 11, 29, 30, 34, 35, 40, 16, 44decaddc 11557 . . . . . 6 (6 + 47) = 53
463, 11deccl 11497 . . . . . 6 26 ∈ ℕ0
47 eqid 2620 . . . . . . 7 12 = 12
485dec0h 11507 . . . . . . . 8 5 = 05
49 eqid 2620 . . . . . . . 8 26 = 26
5024addid2i 10209 . . . . . . . . . 10 (0 + 2) = 2
5150oveq1i 6645 . . . . . . . . 9 ((0 + 2) + 1) = (2 + 1)
52 2p1e3 11136 . . . . . . . . 9 (2 + 1) = 3
5351, 52eqtri 2642 . . . . . . . 8 ((0 + 2) + 1) = 3
54 5cn 11085 . . . . . . . . 9 5 ∈ ℂ
55 6p5e11 11585 . . . . . . . . 9 (6 + 5) = 11
5642, 54, 55addcomli 10213 . . . . . . . 8 (5 + 6) = 11
5733, 5, 3, 11, 48, 49, 53, 2, 56decaddc 11557 . . . . . . 7 (5 + 26) = 31
58 10nn0 11501 . . . . . . 7 10 ∈ ℕ0
59 eqid 2620 . . . . . . . 8 52 = 52
6058nn0cni 11289 . . . . . . . . 9 10 ∈ ℂ
61 3cn 11080 . . . . . . . . 9 3 ∈ ℂ
62 dec10p 11538 . . . . . . . . 9 (10 + 3) = 13
6360, 61, 62addcomli 10213 . . . . . . . 8 (3 + 10) = 13
6454mulid1i 10027 . . . . . . . . . 10 (5 · 1) = 5
65 1p0e1 11118 . . . . . . . . . 10 (1 + 0) = 1
6664, 65oveq12i 6647 . . . . . . . . 9 ((5 · 1) + (1 + 0)) = (5 + 1)
67 5p1e6 11140 . . . . . . . . 9 (5 + 1) = 6
6866, 67eqtri 2642 . . . . . . . 8 ((5 · 1) + (1 + 0)) = 6
6924mulid1i 10027 . . . . . . . . . 10 (2 · 1) = 2
7069oveq1i 6645 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
71 3p2e5 11145 . . . . . . . . . 10 (3 + 2) = 5
7261, 24, 71addcomli 10213 . . . . . . . . 9 (2 + 3) = 5
7370, 72, 483eqtri 2646 . . . . . . . 8 ((2 · 1) + 3) = 05
745, 3, 2, 16, 59, 63, 2, 5, 33, 68, 73decmac 11551 . . . . . . 7 ((52 · 1) + (3 + 10)) = 65
752dec0h 11507 . . . . . . . 8 1 = 01
76 5t2e10 11619 . . . . . . . . . 10 (5 · 2) = 10
77 00id 10196 . . . . . . . . . 10 (0 + 0) = 0
7876, 77oveq12i 6647 . . . . . . . . 9 ((5 · 2) + (0 + 0)) = (10 + 0)
79 dec10p 11538 . . . . . . . . 9 (10 + 0) = 10
8078, 79eqtri 2642 . . . . . . . 8 ((5 · 2) + (0 + 0)) = 10
81 2t2e4 11162 . . . . . . . . . 10 (2 · 2) = 4
8281oveq1i 6645 . . . . . . . . 9 ((2 · 2) + 1) = (4 + 1)
8382, 39, 483eqtri 2646 . . . . . . . 8 ((2 · 2) + 1) = 05
845, 3, 33, 2, 59, 75, 3, 5, 33, 80, 83decmac 11551 . . . . . . 7 ((52 · 2) + 1) = 105
852, 3, 16, 2, 47, 57, 19, 5, 58, 74, 84decma2c 11553 . . . . . 6 ((52 · 12) + (5 + 26)) = 655
86 5t5e25 11624 . . . . . . . 8 (5 · 5) = 25
873, 5, 67, 86decsuc 11520 . . . . . . 7 ((5 · 5) + 1) = 26
8854, 24, 76mulcomli 10032 . . . . . . . 8 (2 · 5) = 10
8961addid2i 10209 . . . . . . . 8 (0 + 3) = 3
902, 33, 16, 88, 89decaddi 11564 . . . . . . 7 ((2 · 5) + 3) = 13
915, 3, 16, 59, 5, 16, 2, 87, 90decrmac 11562 . . . . . 6 ((52 · 5) + 3) = 263
924, 5, 5, 16, 32, 45, 19, 16, 46, 85, 91decma2c 11553 . . . . 5 ((52 · 125) + (6 + 47)) = 6553
93 9cn 11093 . . . . . . . 8 9 ∈ ℂ
94 9t5e45 11651 . . . . . . . 8 (9 · 5) = 45
9593, 54, 94mulcomli 10032 . . . . . . 7 (5 · 9) = 45
96 5p2e7 11150 . . . . . . 7 (5 + 2) = 7
9729, 5, 3, 95, 96decaddi 11564 . . . . . 6 ((5 · 9) + 2) = 47
98 9t2e18 11648 . . . . . . . 8 (9 · 2) = 18
9993, 24, 98mulcomli 10032 . . . . . . 7 (2 · 9) = 18
100 1p1e2 11119 . . . . . . 7 (1 + 1) = 2
101 8p8e16 11603 . . . . . . 7 (8 + 8) = 16
1022, 14, 14, 99, 100, 11, 101decaddci 11565 . . . . . 6 ((2 · 9) + 8) = 26
1035, 3, 14, 59, 27, 11, 3, 97, 102decrmac 11562 . . . . 5 ((52 · 9) + 8) = 476
1046, 27, 11, 14, 1, 28, 19, 11, 31, 92, 103decma2c 11553 . . . 4 ((52 · 𝑁) + 68) = 65536
105 2exp16 15778 . . . 4 (2↑16) = 65536
106 eqid 2620 . . . . 5 (2↑8) = (2↑8)
107 eqid 2620 . . . . 5 ((2↑8) · (2↑8)) = ((2↑8) · (2↑8))
1083, 14, 26, 106, 107numexp2x 15764 . . . 4 (2↑16) = ((2↑8) · (2↑8))
109104, 105, 1083eqtr2i 2648 . . 3 ((52 · 𝑁) + 68) = ((2↑8) · (2↑8))
1109, 10, 14, 20, 21, 15, 22, 26, 109mod2xi 15754 . 2 ((2↑16) mod 𝑁) = (68 mod 𝑁)
111 6p1e7 11141 . . 3 (6 + 1) = 7
112 eqid 2620 . . 3 16 = 16
1132, 11, 111, 112decsuc 11520 . 2 (16 + 1) = 17
11418nn0cni 11289 . . . 4 136 ∈ ℂ
115114addid2i 10209 . . 3 (0 + 136) = 136
1169nncni 11015 . . . . 5 𝑁 ∈ ℂ
117116mul02i 10210 . . . 4 (0 · 𝑁) = 0
118117oveq1i 6645 . . 3 ((0 · 𝑁) + 136) = (0 + 136)
119 6t2e12 11626 . . . . 5 (6 · 2) = 12
1202, 3, 52, 119decsuc 11520 . . . 4 ((6 · 2) + 1) = 13
1213, 11, 14, 28, 11, 2, 120, 25decmul1c 11572 . . 3 (68 · 2) = 136
122115, 118, 1213eqtr4i 2652 . 2 ((0 · 𝑁) + 136) = (68 · 2)
1239, 10, 12, 13, 15, 18, 110, 113, 122modxp1i 15755 1 ((2↑17) mod 𝑁) = (136 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  (class class class)co 6635  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926  cn 11005  2c2 11055  3c3 11056  4c4 11057  5c5 11058  6c6 11059  7c7 11060  8c8 11061  9c9 11062  cdc 11478   mod cmo 12651  cexp 12843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-sup 8333  df-inf 8334  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-rp 11818  df-fl 12576  df-mod 12652  df-seq 12785  df-exp 12844
This theorem is referenced by:  1259lem2  15820  1259lem4  15822
  Copyright terms: Public domain W3C validator