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

Theorem 4001lem3 17121
Description: Lemma for 4001prm 17123. 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 12531 . . . . . 6 4 ∈ ℕ0
3 0nn0 12527 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12732 . . . . 5 40 ∈ ℕ0
54, 3deccl 12732 . . . 4 400 ∈ ℕ0
6 1nn 12263 . . . 4 1 ∈ ℕ
75, 6decnncl 12737 . . 3 4001 ∈ ℕ
81, 7eqeltri 2825 . 2 𝑁 ∈ ℕ
9 2nn 12325 . 2 2 ∈ ℕ
10 2nn0 12529 . . . . 5 2 ∈ ℕ0
1110, 3deccl 12732 . . . 4 20 ∈ ℕ0
1211, 3deccl 12732 . . 3 200 ∈ ℕ0
1312, 3deccl 12732 . 2 2000 ∈ ℕ0
14 0z 12609 . 2 0 ∈ ℤ
15 1nn0 12528 . 2 1 ∈ ℕ0
16 10nn0 12735 . . . . 5 10 ∈ ℕ0
1716, 3deccl 12732 . . . 4 100 ∈ ℕ0
1817, 3deccl 12732 . . 3 1000 ∈ ℕ0
19 8nn0 12535 . . . . . 6 8 ∈ ℕ0
2019, 3deccl 12732 . . . . 5 80 ∈ ℕ0
2120, 3deccl 12732 . . . 4 800 ∈ ℕ0
22 5nn0 12532 . . . . . . 7 5 ∈ ℕ0
2322, 10deccl 12732 . . . . . 6 52 ∈ ℕ0
2423, 15deccl 12732 . . . . 5 521 ∈ ℕ0
2524nn0zi 12627 . . . 4 521 ∈ ℤ
26 3nn0 12530 . . . . . . 7 3 ∈ ℕ0
2710, 26deccl 12732 . . . . . 6 23 ∈ ℕ0
2827, 15deccl 12732 . . . . 5 231 ∈ ℕ0
2928, 15deccl 12732 . . . 4 2311 ∈ ℕ0
30 9nn0 12536 . . . . . 6 9 ∈ ℕ0
3130, 3deccl 12732 . . . . 5 90 ∈ ℕ0
3231, 10deccl 12732 . . . 4 902 ∈ ℕ0
3314001lem2 17120 . . . 4 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
3414001lem1 17119 . . . 4 ((2↑200) mod 𝑁) = (902 mod 𝑁)
35 eqid 2728 . . . . 5 800 = 800
36 eqid 2728 . . . . 5 200 = 200
37 eqid 2728 . . . . . 6 80 = 80
38 eqid 2728 . . . . . 6 20 = 20
39 8p2e10 12797 . . . . . 6 (8 + 2) = 10
40 00id 11429 . . . . . 6 (0 + 0) = 0
4119, 3, 10, 3, 37, 38, 39, 40decadd 12771 . . . . 5 (80 + 20) = 100
4220, 3, 11, 3, 35, 36, 41, 40decadd 12771 . . . 4 (800 + 200) = 1000
4315dec0h 12739 . . . . . 6 1 = 01
44 eqid 2728 . . . . . . 7 400 = 400
4523nn0cni 12524 . . . . . . . 8 52 ∈ ℂ
4645addlidi 11442 . . . . . . 7 (0 + 52) = 52
47 eqid 2728 . . . . . . . 8 40 = 40
48 5cn 12340 . . . . . . . . . 10 5 ∈ ℂ
4948addridi 11441 . . . . . . . . 9 (5 + 0) = 5
5022dec0h 12739 . . . . . . . . 9 5 = 05
5149, 50eqtri 2756 . . . . . . . 8 (5 + 0) = 05
5240, 3eqeltri 2825 . . . . . . . . 9 (0 + 0) ∈ ℕ0
53 eqid 2728 . . . . . . . . 9 521 = 521
54 eqid 2728 . . . . . . . . . 10 52 = 52
55 5t4e20 12819 . . . . . . . . . 10 (5 · 4) = 20
56 4cn 12337 . . . . . . . . . . 11 4 ∈ ℂ
57 2cn 12327 . . . . . . . . . . 11 2 ∈ ℂ
58 4t2e8 12420 . . . . . . . . . . 11 (4 · 2) = 8
5956, 57, 58mulcomli 11263 . . . . . . . . . 10 (2 · 4) = 8
602, 22, 10, 54, 55, 59decmul1 12781 . . . . . . . . 9 (52 · 4) = 208
6156mullidi 11259 . . . . . . . . . . 11 (1 · 4) = 4
6261, 40oveq12i 7438 . . . . . . . . . 10 ((1 · 4) + (0 + 0)) = (4 + 0)
6356addridi 11441 . . . . . . . . . 10 (4 + 0) = 4
6462, 63eqtri 2756 . . . . . . . . 9 ((1 · 4) + (0 + 0)) = 4
6523, 15, 52, 53, 2, 60, 64decrmanc 12774 . . . . . . . 8 ((521 · 4) + (0 + 0)) = 2084
6624nn0cni 12524 . . . . . . . . . . 11 521 ∈ ℂ
6766mul01i 11444 . . . . . . . . . 10 (521 · 0) = 0
6867oveq1i 7436 . . . . . . . . 9 ((521 · 0) + 5) = (0 + 5)
6948addlidi 11442 . . . . . . . . 9 (0 + 5) = 5
7068, 69, 503eqtri 2760 . . . . . . . 8 ((521 · 0) + 5) = 05
712, 3, 3, 22, 47, 51, 24, 22, 3, 65, 70decma2c 12770 . . . . . . 7 ((521 · 40) + (5 + 0)) = 20845
7267oveq1i 7436 . . . . . . . 8 ((521 · 0) + 2) = (0 + 2)
7357addlidi 11442 . . . . . . . 8 (0 + 2) = 2
7410dec0h 12739 . . . . . . . 8 2 = 02
7572, 73, 743eqtri 2760 . . . . . . 7 ((521 · 0) + 2) = 02
764, 3, 22, 10, 44, 46, 24, 10, 3, 71, 75decma2c 12770 . . . . . 6 ((521 · 400) + (0 + 52)) = 208452
7745mulridi 11258 . . . . . . 7 (52 · 1) = 52
78 ax-1cn 11206 . . . . . . . . . 10 1 ∈ ℂ
7978mullidi 11259 . . . . . . . . 9 (1 · 1) = 1
8079oveq1i 7436 . . . . . . . 8 ((1 · 1) + 1) = (1 + 1)
81 1p1e2 12377 . . . . . . . 8 (1 + 1) = 2
8280, 81eqtri 2756 . . . . . . 7 ((1 · 1) + 1) = 2
8323, 15, 15, 53, 15, 77, 82decrmanc 12774 . . . . . 6 ((521 · 1) + 1) = 522
845, 15, 3, 15, 1, 43, 24, 10, 23, 76, 83decma2c 12770 . . . . 5 ((521 · 𝑁) + 1) = 2084522
85 eqid 2728 . . . . . 6 902 = 902
86 6nn0 12533 . . . . . . . 8 6 ∈ ℕ0
872, 86deccl 12732 . . . . . . 7 46 ∈ ℕ0
8887, 10deccl 12732 . . . . . 6 462 ∈ ℕ0
89 eqid 2728 . . . . . . 7 90 = 90
90 eqid 2728 . . . . . . 7 462 = 462
91 eqid 2728 . . . . . . . 8 2311 = 2311
9287nn0cni 12524 . . . . . . . . 9 46 ∈ ℂ
9392addridi 11441 . . . . . . . 8 (46 + 0) = 46
94 4p1e5 12398 . . . . . . . . . 10 (4 + 1) = 5
9594, 22eqeltri 2825 . . . . . . . . 9 (4 + 1) ∈ ℕ0
96 eqid 2728 . . . . . . . . 9 231 = 231
97 eqid 2728 . . . . . . . . . 10 23 = 23
98 9cn 12352 . . . . . . . . . . . 12 9 ∈ ℂ
99 9t2e18 12839 . . . . . . . . . . . 12 (9 · 2) = 18
10098, 57, 99mulcomli 11263 . . . . . . . . . . 11 (2 · 9) = 18
10115, 19, 10, 100, 81, 39decaddci2 12779 . . . . . . . . . 10 ((2 · 9) + 2) = 20
102 7nn0 12534 . . . . . . . . . . 11 7 ∈ ℕ0
103 7p1e8 12401 . . . . . . . . . . 11 (7 + 1) = 8
104 3cn 12333 . . . . . . . . . . . 12 3 ∈ ℂ
105 9t3e27 12840 . . . . . . . . . . . 12 (9 · 3) = 27
10698, 104, 105mulcomli 11263 . . . . . . . . . . 11 (3 · 9) = 27
10710, 102, 103, 106decsuc 12748 . . . . . . . . . 10 ((3 · 9) + 1) = 28
10810, 26, 15, 97, 30, 19, 10, 101, 107decrmac 12775 . . . . . . . . 9 ((23 · 9) + 1) = 208
10998mullidi 11259 . . . . . . . . . . 11 (1 · 9) = 9
110109, 94oveq12i 7438 . . . . . . . . . 10 ((1 · 9) + (4 + 1)) = (9 + 5)
111 9p5e14 12807 . . . . . . . . . 10 (9 + 5) = 14
112110, 111eqtri 2756 . . . . . . . . 9 ((1 · 9) + (4 + 1)) = 14
11327, 15, 95, 96, 30, 2, 15, 108, 112decrmac 12775 . . . . . . . 8 ((231 · 9) + (4 + 1)) = 2084
114109oveq1i 7436 . . . . . . . . 9 ((1 · 9) + 6) = (9 + 6)
115 9p6e15 12808 . . . . . . . . 9 (9 + 6) = 15
116114, 115eqtri 2756 . . . . . . . 8 ((1 · 9) + 6) = 15
11728, 15, 2, 86, 91, 93, 30, 22, 15, 113, 116decmac 12769 . . . . . . 7 ((2311 · 9) + (46 + 0)) = 20845
11829nn0cni 12524 . . . . . . . . . 10 2311 ∈ ℂ
119118mul01i 11444 . . . . . . . . 9 (2311 · 0) = 0
120119oveq1i 7436 . . . . . . . 8 ((2311 · 0) + 2) = (0 + 2)
121120, 73, 743eqtri 2760 . . . . . . 7 ((2311 · 0) + 2) = 02
12230, 3, 87, 10, 89, 90, 29, 10, 3, 117, 121decma2c 12770 . . . . . 6 ((2311 · 90) + 462) = 208452
123 2t2e4 12416 . . . . . . . . 9 (2 · 2) = 4
124 3t2e6 12418 . . . . . . . . 9 (3 · 2) = 6
12510, 10, 26, 97, 123, 124decmul1 12781 . . . . . . . 8 (23 · 2) = 46
12657mullidi 11259 . . . . . . . 8 (1 · 2) = 2
12710, 27, 15, 96, 125, 126decmul1 12781 . . . . . . 7 (231 · 2) = 462
12810, 28, 15, 91, 127, 126decmul1 12781 . . . . . 6 (2311 · 2) = 4622
12929, 31, 10, 85, 10, 88, 122, 128decmul2c 12783 . . . . 5 (2311 · 902) = 2084522
13084, 129eqtr4i 2759 . . . 4 ((521 · 𝑁) + 1) = (2311 · 902)
1318, 9, 21, 25, 29, 15, 12, 32, 33, 34, 42, 130modxai 17046 . . 3 ((2↑1000) mod 𝑁) = (1 mod 𝑁)
13218nn0cni 12524 . . . 4 1000 ∈ ℂ
133 eqid 2728 . . . . 5 1000 = 1000
134 eqid 2728 . . . . . 6 100 = 100
13510dec0u 12738 . . . . . 6 (10 · 2) = 20
13657mul02i 11443 . . . . . 6 (0 · 2) = 0
13710, 16, 3, 134, 135, 136decmul1 12781 . . . . 5 (100 · 2) = 200
13810, 17, 3, 133, 137, 136decmul1 12781 . . . 4 (1000 · 2) = 2000
139132, 57, 138mulcomli 11263 . . 3 (2 · 1000) = 2000
1408nncni 12262 . . . . . 6 𝑁 ∈ ℂ
141140mul02i 11443 . . . . 5 (0 · 𝑁) = 0
142141oveq1i 7436 . . . 4 ((0 · 𝑁) + 1) = (0 + 1)
14378addlidi 11442 . . . . 5 (0 + 1) = 1
14479, 143eqtr4i 2759 . . . 4 (1 · 1) = (0 + 1)
145142, 144eqtr4i 2759 . . 3 ((0 · 𝑁) + 1) = (1 · 1)
1468, 9, 18, 14, 15, 15, 131, 139, 145mod2xi 17047 . 2 ((2↑2000) mod 𝑁) = (1 mod 𝑁)
14713nn0cni 12524 . . . 4 2000 ∈ ℂ
148 eqid 2728 . . . . 5 2000 = 2000
14910, 10, 3, 38, 123, 136decmul1 12781 . . . . . 6 (20 · 2) = 40
15010, 11, 3, 36, 149, 136decmul1 12781 . . . . 5 (200 · 2) = 400
15110, 12, 3, 148, 150, 136decmul1 12781 . . . 4 (2000 · 2) = 4000
152147, 57, 151mulcomli 11263 . . 3 (2 · 2000) = 4000
1535, 3deccl 12732 . . . . 5 4000 ∈ ℕ0
154153nn0cni 12524 . . . 4 4000 ∈ ℂ
155 eqid 2728 . . . . . 6 4000 = 4000
1565, 3, 143, 155decsuc 12748 . . . . 5 (4000 + 1) = 4001
1571, 156eqtr4i 2759 . . . 4 𝑁 = (4000 + 1)
158154, 78, 157mvrraddi 11517 . . 3 (𝑁 − 1) = 4000
159152, 158eqtr4i 2759 . 2 (2 · 2000) = (𝑁 − 1)
1608, 9, 13, 14, 15, 15, 146, 159, 145mod2xi 17047 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  (class class class)co 7426  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153  cmin 11484  cn 12252  2c2 12307  3c3 12308  4c4 12309  5c5 12310  6c6 12311  7c7 12312  8c8 12313  9c9 12314  0cn0 12512  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:  4001prm  17123
  Copyright terms: Public domain W3C validator