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

Theorem 4001lem3 16057
Description: Lemma for 4001prm 16059. Calculate a power mod. In decimal, we calculate 2↑1000 = 2↑800 · 2↑200≡2311 · 902 = 521𝑁 + 1 and finally 2↑(𝑁 − 1) = (2↑1000)↑4≡1↑4 = 1. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
4001prm.1 𝑁 = 4001
Assertion
Ref Expression
4001lem3 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)

Proof of Theorem 4001lem3
StepHypRef Expression
1 4001prm.1 . . 3 𝑁 = 4001
2 4nn0 11574 . . . . . 6 4 ∈ ℕ0
3 0nn0 11570 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11770 . . . . 5 40 ∈ ℕ0
54, 3deccl 11770 . . . 4 400 ∈ ℕ0
6 1nn 11312 . . . 4 1 ∈ ℕ
75, 6decnncl 11775 . . 3 4001 ∈ ℕ
81, 7eqeltri 2881 . 2 𝑁 ∈ ℕ
9 2nn 11458 . 2 2 ∈ ℕ
10 2nn0 11572 . . . . 5 2 ∈ ℕ0
1110, 3deccl 11770 . . . 4 20 ∈ ℕ0
1211, 3deccl 11770 . . 3 200 ∈ ℕ0
1312, 3deccl 11770 . 2 2000 ∈ ℕ0
14 0z 11650 . 2 0 ∈ ℤ
15 1nn0 11571 . 2 1 ∈ ℕ0
16 10nn0 11773 . . . . 5 10 ∈ ℕ0
1716, 3deccl 11770 . . . 4 100 ∈ ℕ0
1817, 3deccl 11770 . . 3 1000 ∈ ℕ0
19 8nn0 11578 . . . . . 6 8 ∈ ℕ0
2019, 3deccl 11770 . . . . 5 80 ∈ ℕ0
2120, 3deccl 11770 . . . 4 800 ∈ ℕ0
22 5nn0 11575 . . . . . . 7 5 ∈ ℕ0
2322, 10deccl 11770 . . . . . 6 52 ∈ ℕ0
2423, 15deccl 11770 . . . . 5 521 ∈ ℕ0
2524nn0zi 11664 . . . 4 521 ∈ ℤ
26 3nn0 11573 . . . . . . 7 3 ∈ ℕ0
2710, 26deccl 11770 . . . . . 6 23 ∈ ℕ0
2827, 15deccl 11770 . . . . 5 231 ∈ ℕ0
2928, 15deccl 11770 . . . 4 2311 ∈ ℕ0
30 9nn0 11579 . . . . . 6 9 ∈ ℕ0
3130, 3deccl 11770 . . . . 5 90 ∈ ℕ0
3231, 10deccl 11770 . . . 4 902 ∈ ℕ0
3314001lem2 16056 . . . 4 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
3414001lem1 16055 . . . 4 ((2↑200) mod 𝑁) = (902 mod 𝑁)
35 eqid 2806 . . . . 5 800 = 800
36 eqid 2806 . . . . 5 200 = 200
37 eqid 2806 . . . . . 6 80 = 80
38 eqid 2806 . . . . . 6 20 = 20
39 8p2e10 11835 . . . . . 6 (8 + 2) = 10
40 00id 10492 . . . . . 6 (0 + 0) = 0
4119, 3, 10, 3, 37, 38, 39, 40decadd 11809 . . . . 5 (80 + 20) = 100
4220, 3, 11, 3, 35, 36, 41, 40decadd 11809 . . . 4 (800 + 200) = 1000
4315dec0h 11777 . . . . . 6 1 = 01
44 eqid 2806 . . . . . . 7 400 = 400
4523nn0cni 11567 . . . . . . . 8 52 ∈ ℂ
4645addid2i 10505 . . . . . . 7 (0 + 52) = 52
47 eqid 2806 . . . . . . . 8 40 = 40
48 5cn 11380 . . . . . . . . . 10 5 ∈ ℂ
4948addid1i 10504 . . . . . . . . 9 (5 + 0) = 5
5022dec0h 11777 . . . . . . . . 9 5 = 05
5149, 50eqtri 2828 . . . . . . . 8 (5 + 0) = 05
5240, 3eqeltri 2881 . . . . . . . . 9 (0 + 0) ∈ ℕ0
53 eqid 2806 . . . . . . . . 9 521 = 521
54 eqid 2806 . . . . . . . . . 10 52 = 52
55 5t4e20 11857 . . . . . . . . . 10 (5 · 4) = 20
56 4cn 11378 . . . . . . . . . . 11 4 ∈ ℂ
57 2cn 11371 . . . . . . . . . . 11 2 ∈ ℂ
58 4t2e8 11455 . . . . . . . . . . 11 (4 · 2) = 8
5956, 57, 58mulcomli 10330 . . . . . . . . . 10 (2 · 4) = 8
602, 22, 10, 54, 19, 55, 59decmul1 11819 . . . . . . . . 9 (52 · 4) = 208
6156mulid2i 10326 . . . . . . . . . . 11 (1 · 4) = 4
6261, 40oveq12i 6882 . . . . . . . . . 10 ((1 · 4) + (0 + 0)) = (4 + 0)
6356addid1i 10504 . . . . . . . . . 10 (4 + 0) = 4
6462, 63eqtri 2828 . . . . . . . . 9 ((1 · 4) + (0 + 0)) = 4
6523, 15, 52, 53, 2, 60, 64decrmanc 11812 . . . . . . . 8 ((521 · 4) + (0 + 0)) = 2084
6624nn0cni 11567 . . . . . . . . . . 11 521 ∈ ℂ
6766mul01i 10507 . . . . . . . . . 10 (521 · 0) = 0
6867oveq1i 6880 . . . . . . . . 9 ((521 · 0) + 5) = (0 + 5)
6948addid2i 10505 . . . . . . . . 9 (0 + 5) = 5
7068, 69, 503eqtri 2832 . . . . . . . 8 ((521 · 0) + 5) = 05
712, 3, 3, 22, 47, 51, 24, 22, 3, 65, 70decma2c 11808 . . . . . . 7 ((521 · 40) + (5 + 0)) = 20845
7267oveq1i 6880 . . . . . . . 8 ((521 · 0) + 2) = (0 + 2)
7357addid2i 10505 . . . . . . . 8 (0 + 2) = 2
7410dec0h 11777 . . . . . . . 8 2 = 02
7572, 73, 743eqtri 2832 . . . . . . 7 ((521 · 0) + 2) = 02
764, 3, 22, 10, 44, 46, 24, 10, 3, 71, 75decma2c 11808 . . . . . 6 ((521 · 400) + (0 + 52)) = 208452
7745mulid1i 10325 . . . . . . 7 (52 · 1) = 52
78 ax-1cn 10275 . . . . . . . . . 10 1 ∈ ℂ
7978mulid2i 10326 . . . . . . . . 9 (1 · 1) = 1
8079oveq1i 6880 . . . . . . . 8 ((1 · 1) + 1) = (1 + 1)
81 1p1e2 11413 . . . . . . . 8 (1 + 1) = 2
8280, 81eqtri 2828 . . . . . . 7 ((1 · 1) + 1) = 2
8323, 15, 15, 53, 15, 77, 82decrmanc 11812 . . . . . 6 ((521 · 1) + 1) = 522
845, 15, 3, 15, 1, 43, 24, 10, 23, 76, 83decma2c 11808 . . . . 5 ((521 · 𝑁) + 1) = 2084522
85 eqid 2806 . . . . . 6 902 = 902
86 6nn0 11576 . . . . . . . 8 6 ∈ ℕ0
872, 86deccl 11770 . . . . . . 7 46 ∈ ℕ0
8887, 10deccl 11770 . . . . . 6 462 ∈ ℕ0
89 eqid 2806 . . . . . . 7 90 = 90
90 eqid 2806 . . . . . . 7 462 = 462
91 eqid 2806 . . . . . . . 8 2311 = 2311
9287nn0cni 11567 . . . . . . . . 9 46 ∈ ℂ
9392addid1i 10504 . . . . . . . 8 (46 + 0) = 46
94 4p1e5 11433 . . . . . . . . . 10 (4 + 1) = 5
9594, 22eqeltri 2881 . . . . . . . . 9 (4 + 1) ∈ ℕ0
96 eqid 2806 . . . . . . . . 9 231 = 231
97 eqid 2806 . . . . . . . . . 10 23 = 23
98 9cn 11388 . . . . . . . . . . . 12 9 ∈ ℂ
99 9t2e18 11877 . . . . . . . . . . . 12 (9 · 2) = 18
10098, 57, 99mulcomli 10330 . . . . . . . . . . 11 (2 · 9) = 18
10115, 19, 10, 100, 81, 39decaddci2 11817 . . . . . . . . . 10 ((2 · 9) + 2) = 20
102 7nn0 11577 . . . . . . . . . . 11 7 ∈ ℕ0
103 7p1e8 11436 . . . . . . . . . . 11 (7 + 1) = 8
104 3cn 11375 . . . . . . . . . . . 12 3 ∈ ℂ
105 9t3e27 11878 . . . . . . . . . . . 12 (9 · 3) = 27
10698, 104, 105mulcomli 10330 . . . . . . . . . . 11 (3 · 9) = 27
10710, 102, 103, 106decsuc 11786 . . . . . . . . . 10 ((3 · 9) + 1) = 28
10810, 26, 15, 97, 30, 19, 10, 101, 107decrmac 11813 . . . . . . . . 9 ((23 · 9) + 1) = 208
10998mulid2i 10326 . . . . . . . . . . 11 (1 · 9) = 9
110109, 94oveq12i 6882 . . . . . . . . . 10 ((1 · 9) + (4 + 1)) = (9 + 5)
111 9p5e14 11845 . . . . . . . . . 10 (9 + 5) = 14
112110, 111eqtri 2828 . . . . . . . . 9 ((1 · 9) + (4 + 1)) = 14
11327, 15, 95, 96, 30, 2, 15, 108, 112decrmac 11813 . . . . . . . 8 ((231 · 9) + (4 + 1)) = 2084
114109oveq1i 6880 . . . . . . . . 9 ((1 · 9) + 6) = (9 + 6)
115 9p6e15 11846 . . . . . . . . 9 (9 + 6) = 15
116114, 115eqtri 2828 . . . . . . . 8 ((1 · 9) + 6) = 15
11728, 15, 2, 86, 91, 93, 30, 22, 15, 113, 116decmac 11807 . . . . . . 7 ((2311 · 9) + (46 + 0)) = 20845
11829nn0cni 11567 . . . . . . . . . 10 2311 ∈ ℂ
119118mul01i 10507 . . . . . . . . 9 (2311 · 0) = 0
120119oveq1i 6880 . . . . . . . 8 ((2311 · 0) + 2) = (0 + 2)
121120, 73, 743eqtri 2832 . . . . . . 7 ((2311 · 0) + 2) = 02
12230, 3, 87, 10, 89, 90, 29, 10, 3, 117, 121decma2c 11808 . . . . . 6 ((2311 · 90) + 462) = 208452
123 2t2e4 11451 . . . . . . . . 9 (2 · 2) = 4
124 3t2e6 11453 . . . . . . . . 9 (3 · 2) = 6
12510, 10, 26, 97, 86, 123, 124decmul1 11819 . . . . . . . 8 (23 · 2) = 46
12657mulid2i 10326 . . . . . . . 8 (1 · 2) = 2
12710, 27, 15, 96, 10, 125, 126decmul1 11819 . . . . . . 7 (231 · 2) = 462
12810, 28, 15, 91, 10, 127, 126decmul1 11819 . . . . . 6 (2311 · 2) = 4622
12929, 31, 10, 85, 10, 88, 122, 128decmul2c 11821 . . . . 5 (2311 · 902) = 2084522
13084, 129eqtr4i 2831 . . . 4 ((521 · 𝑁) + 1) = (2311 · 902)
1318, 9, 21, 25, 29, 15, 12, 32, 33, 34, 42, 130modxai 15985 . . 3 ((2↑1000) mod 𝑁) = (1 mod 𝑁)
13218nn0cni 11567 . . . 4 1000 ∈ ℂ
133 eqid 2806 . . . . 5 1000 = 1000
134 eqid 2806 . . . . . 6 100 = 100
13510dec0u 11776 . . . . . 6 (10 · 2) = 20
13657mul02i 10506 . . . . . 6 (0 · 2) = 0
13710, 16, 3, 134, 3, 135, 136decmul1 11819 . . . . 5 (100 · 2) = 200
13810, 17, 3, 133, 3, 137, 136decmul1 11819 . . . 4 (1000 · 2) = 2000
139132, 57, 138mulcomli 10330 . . 3 (2 · 1000) = 2000
1408nncni 11311 . . . . . 6 𝑁 ∈ ℂ
141140mul02i 10506 . . . . 5 (0 · 𝑁) = 0
142141oveq1i 6880 . . . 4 ((0 · 𝑁) + 1) = (0 + 1)
14378addid2i 10505 . . . . 5 (0 + 1) = 1
14479, 143eqtr4i 2831 . . . 4 (1 · 1) = (0 + 1)
145142, 144eqtr4i 2831 . . 3 ((0 · 𝑁) + 1) = (1 · 1)
1468, 9, 18, 14, 15, 15, 131, 139, 145mod2xi 15986 . 2 ((2↑2000) mod 𝑁) = (1 mod 𝑁)
14713nn0cni 11567 . . . 4 2000 ∈ ℂ
148 eqid 2806 . . . . 5 2000 = 2000
14910, 10, 3, 38, 3, 123, 136decmul1 11819 . . . . . 6 (20 · 2) = 40
15010, 11, 3, 36, 3, 149, 136decmul1 11819 . . . . 5 (200 · 2) = 400
15110, 12, 3, 148, 3, 150, 136decmul1 11819 . . . 4 (2000 · 2) = 4000
152147, 57, 151mulcomli 10330 . . 3 (2 · 2000) = 4000
1535, 3deccl 11770 . . . . 5 4000 ∈ ℕ0
154153nn0cni 11567 . . . 4 4000 ∈ ℂ
155 eqid 2806 . . . . . 6 4000 = 4000
1565, 3, 143, 155decsuc 11786 . . . . 5 (4000 + 1) = 4001
1571, 156eqtr4i 2831 . . . 4 𝑁 = (4000 + 1)
158154, 78, 157mvrraddi 10579 . . 3 (𝑁 − 1) = 4000
159152, 158eqtr4i 2831 . 2 (2 · 2000) = (𝑁 − 1)
1608, 9, 13, 14, 15, 15, 146, 159, 145mod2xi 15986 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  (class class class)co 6870  0cc0 10217  1c1 10218   + caddc 10220   · cmul 10222  cmin 10547  cn 11301  2c2 11352  3c3 11353  4c4 11354  5c5 11355  6c6 11356  7c7 11357  8c8 11358  9c9 11359  0cn0 11555  cdc 11755   mod cmo 12888  cexp 13079
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-sup 8583  df-inf 8584  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-rp 12043  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080
This theorem is referenced by:  4001prm  16059
  Copyright terms: Public domain W3C validator