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

Theorem 4001prm 17141
Description: 4001 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
4001prm.1 𝑁 = 4001
Assertion
Ref Expression
4001prm 𝑁 ∈ ℙ

Proof of Theorem 4001prm
StepHypRef Expression
1 5prm 17105 . 2 5 ∈ ℙ
2 8nn 12352 . . . 4 8 ∈ ℕ
32decnncl2 12746 . . 3 80 ∈ ℕ
43decnncl2 12746 . 2 800 ∈ ℕ
5 4nn0 12536 . . . . . . . 8 4 ∈ ℕ0
6 0nn0 12532 . . . . . . . 8 0 ∈ ℕ0
75, 6deccl 12737 . . . . . . 7 40 ∈ ℕ0
87, 6deccl 12737 . . . . . 6 400 ∈ ℕ0
98, 6deccl 12737 . . . . 5 4000 ∈ ℕ0
109nn0cni 12529 . . . 4 4000 ∈ ℂ
11 ax-1cn 11206 . . . 4 1 ∈ ℂ
12 4001prm.1 . . . . 5 𝑁 = 4001
1311addlidi 11442 . . . . . 6 (0 + 1) = 1
14 eqid 2726 . . . . . 6 4000 = 4000
158, 6, 13, 14decsuc 12753 . . . . 5 (4000 + 1) = 4001
1612, 15eqtr4i 2757 . . . 4 𝑁 = (4000 + 1)
1710, 11, 16mvrraddi 11517 . . 3 (𝑁 − 1) = 4000
18 5nn0 12537 . . . 4 5 ∈ ℕ0
19 8nn0 12540 . . . . 5 8 ∈ ℕ0
2019, 6deccl 12737 . . . 4 80 ∈ ℕ0
21 eqid 2726 . . . 4 800 = 800
22 eqid 2726 . . . . 5 80 = 80
23 8t5e40 12840 . . . . 5 (8 · 5) = 40
24 5cn 12345 . . . . . 6 5 ∈ ℂ
2524mul02i 11443 . . . . 5 (0 · 5) = 0
2618, 19, 6, 22, 23, 25decmul1 12786 . . . 4 (80 · 5) = 400
2718, 20, 6, 21, 26, 25decmul1 12786 . . 3 (800 · 5) = 4000
2817, 27eqtr4i 2757 . 2 (𝑁 − 1) = (800 · 5)
29 1nn0 12533 . . . . . . 7 1 ∈ ℕ0
308, 29deccl 12737 . . . . . 6 4001 ∈ ℕ0
3112, 30eqeltri 2822 . . . . 5 𝑁 ∈ ℕ0
3231nn0cni 12529 . . . 4 𝑁 ∈ ℂ
33 npcan 11509 . . . 4 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
3432, 11, 33mp2an 690 . . 3 ((𝑁 − 1) + 1) = 𝑁
3534eqcomi 2735 . 2 𝑁 = ((𝑁 − 1) + 1)
36 3nn0 12535 . . 3 3 ∈ ℕ0
37 2nn 12330 . . 3 2 ∈ ℕ
3836, 37decnncl 12742 . 2 32 ∈ ℕ
39 3nn 12336 . 2 3 ∈ ℕ
40 2nn0 12534 . . . . 5 2 ∈ ℕ0
4136, 40deccl 12737 . . . 4 32 ∈ ℕ0
4229, 40deccl 12737 . . . 4 12 ∈ ℕ0
43 2p1e3 12399 . . . . 5 (2 + 1) = 3
4424sqvali 14191 . . . . . . 7 (5↑2) = (5 · 5)
45 5t5e25 12825 . . . . . . 7 (5 · 5) = 25
4644, 45eqtri 2754 . . . . . 6 (5↑2) = 25
47 2cn 12332 . . . . . . . 8 2 ∈ ℂ
48 5t2e10 12822 . . . . . . . 8 (5 · 2) = 10
4924, 47, 48mulcomli 11263 . . . . . . 7 (2 · 5) = 10
5047addlidi 11442 . . . . . . 7 (0 + 2) = 2
5129, 6, 40, 49, 50decaddi 12782 . . . . . 6 ((2 · 5) + 2) = 12
5218, 40, 18, 46, 18, 40, 51, 45decmul1c 12787 . . . . 5 ((5↑2) · 5) = 125
5318, 40, 43, 52numexpp1 17074 . . . 4 (5↑3) = 125
54 6nn0 12538 . . . . 5 6 ∈ ℕ0
5529, 54deccl 12737 . . . 4 16 ∈ ℕ0
56 eqid 2726 . . . . 5 12 = 12
57 eqid 2726 . . . . 5 16 = 16
58 7nn0 12539 . . . . 5 7 ∈ ℕ0
59 7cn 12351 . . . . . . . 8 7 ∈ ℂ
60 7p1e8 12406 . . . . . . . 8 (7 + 1) = 8
6159, 11, 60addcomli 11446 . . . . . . 7 (1 + 7) = 8
6261, 19eqeltri 2822 . . . . . 6 (1 + 7) ∈ ℕ0
63 eqid 2726 . . . . . 6 32 = 32
64 3t1e3 12422 . . . . . . . 8 (3 · 1) = 3
6564oveq1i 7425 . . . . . . 7 ((3 · 1) + 1) = (3 + 1)
66 3p1e4 12402 . . . . . . 7 (3 + 1) = 4
6765, 66eqtri 2754 . . . . . 6 ((3 · 1) + 1) = 4
68 2t1e2 12420 . . . . . . . 8 (2 · 1) = 2
6968, 61oveq12i 7427 . . . . . . 7 ((2 · 1) + (1 + 7)) = (2 + 8)
70 8cn 12354 . . . . . . . 8 8 ∈ ℂ
71 8p2e10 12802 . . . . . . . 8 (8 + 2) = 10
7270, 47, 71addcomli 11446 . . . . . . 7 (2 + 8) = 10
7369, 72eqtri 2754 . . . . . 6 ((2 · 1) + (1 + 7)) = 10
7436, 40, 62, 63, 29, 6, 29, 67, 73decrmac 12780 . . . . 5 ((32 · 1) + (1 + 7)) = 40
75 3t2e6 12423 . . . . . . . 8 (3 · 2) = 6
7675oveq1i 7425 . . . . . . 7 ((3 · 2) + 1) = (6 + 1)
77 6p1e7 12405 . . . . . . 7 (6 + 1) = 7
7876, 77eqtri 2754 . . . . . 6 ((3 · 2) + 1) = 7
79 2t2e4 12421 . . . . . . . 8 (2 · 2) = 4
8079oveq1i 7425 . . . . . . 7 ((2 · 2) + 6) = (4 + 6)
81 6cn 12348 . . . . . . . 8 6 ∈ ℂ
82 4cn 12342 . . . . . . . 8 4 ∈ ℂ
83 6p4e10 12794 . . . . . . . 8 (6 + 4) = 10
8481, 82, 83addcomli 11446 . . . . . . 7 (4 + 6) = 10
8580, 84eqtri 2754 . . . . . 6 ((2 · 2) + 6) = 10
8636, 40, 54, 63, 40, 6, 29, 78, 85decrmac 12780 . . . . 5 ((32 · 2) + 6) = 70
8729, 40, 29, 54, 56, 57, 41, 6, 58, 74, 86decma2c 12775 . . . 4 ((32 · 12) + 16) = 400
88 5p1e6 12404 . . . . . 6 (5 + 1) = 6
89 3cn 12338 . . . . . . 7 3 ∈ ℂ
90 5t3e15 12823 . . . . . . 7 (5 · 3) = 15
9124, 89, 90mulcomli 11263 . . . . . 6 (3 · 5) = 15
9229, 18, 88, 91decsuc 12753 . . . . 5 ((3 · 5) + 1) = 16
9318, 36, 40, 63, 6, 29, 92, 49decmul1c 12787 . . . 4 (32 · 5) = 160
9441, 42, 18, 53, 6, 55, 87, 93decmul2c 12788 . . 3 (32 · (5↑3)) = 4000
9517, 94eqtr4i 2757 . 2 (𝑁 − 1) = (32 · (5↑3))
96 2lt10 12860 . . . 4 2 < 10
97 1nn 12268 . . . . 5 1 ∈ ℕ
98 3lt10 12859 . . . . 5 3 < 10
9997, 40, 36, 98declti 12760 . . . 4 3 < 12
10036, 42, 40, 18, 96, 99decltc 12751 . . 3 32 < 125
101100, 53breqtrri 5172 . 2 32 < (5↑3)
102124001lem3 17139 . 2 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
103124001lem4 17140 . 2 (((2↑800) − 1) gcd 𝑁) = 1
1041, 4, 28, 35, 38, 39, 37, 95, 101, 102, 103pockthi 16903 1 𝑁 ∈ ℙ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  wcel 2099  (class class class)co 7415  cc 11146  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153   < clt 11288  cmin 11484  2c2 12312  3c3 12313  4c4 12314  5c5 12315  6c6 12316  7c7 12317  8c8 12318  0cn0 12517  cdc 12722  cexp 14074  cprime 16666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7737  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 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366  df-rab 3421  df-v 3466  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3968  df-nul 4325  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4908  df-int 4949  df-iun 4997  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6497  df-fun 6547  df-fn 6548  df-f 6549  df-f1 6550  df-fo 6551  df-f1o 6552  df-fv 6553  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7868  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-er 8725  df-en 8966  df-dom 8967  df-sdom 8968  df-fin 8969  df-sup 9477  df-inf 9478  df-dju 9936  df-card 9974  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 12258  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326  df-9 12327  df-n0 12518  df-xnn0 12590  df-z 12604  df-dec 12723  df-uz 12868  df-q 12978  df-rp 13022  df-fz 13532  df-fzo 13675  df-fl 13805  df-mod 13883  df-seq 14015  df-exp 14075  df-hash 14342  df-cj 15098  df-re 15099  df-im 15100  df-sqrt 15234  df-abs 15235  df-dvds 16251  df-gcd 16489  df-prm 16667  df-odz 16761  df-phi 16762  df-pc 16833
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator