Proof of Theorem 2503prm
| Step | Hyp | Ref
| Expression |
| 1 | | 139prm 17161 |
. 2
⊢ ;;139 ∈ ℙ |
| 2 | | 1nn0 12542 |
. . 3
⊢ 1 ∈
ℕ0 |
| 3 | | 8nn 12361 |
. . 3
⊢ 8 ∈
ℕ |
| 4 | 2, 3 | decnncl 12753 |
. 2
⊢ ;18 ∈ ℕ |
| 5 | | 2503prm.1 |
. . . . 5
⊢ 𝑁 = ;;;2503 |
| 6 | | 2nn0 12543 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
| 7 | | 5nn0 12546 |
. . . . . . . 8
⊢ 5 ∈
ℕ0 |
| 8 | 6, 7 | deccl 12748 |
. . . . . . 7
⊢ ;25 ∈
ℕ0 |
| 9 | | 0nn0 12541 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
| 10 | 8, 9 | deccl 12748 |
. . . . . 6
⊢ ;;250 ∈ ℕ0 |
| 11 | | 2p1e3 12408 |
. . . . . 6
⊢ (2 + 1) =
3 |
| 12 | | eqid 2737 |
. . . . . 6
⊢ ;;;2502 =
;;;2502 |
| 13 | 10, 6, 11, 12 | decsuc 12764 |
. . . . 5
⊢ (;;;2502 +
1) = ;;;2503 |
| 14 | 5, 13 | eqtr4i 2768 |
. . . 4
⊢ 𝑁 = (;;;2502 + 1) |
| 15 | 14 | oveq1i 7441 |
. . 3
⊢ (𝑁 − 1) = ((;;;2502 +
1) − 1) |
| 16 | | 8nn0 12549 |
. . . . . 6
⊢ 8 ∈
ℕ0 |
| 17 | 2, 16 | deccl 12748 |
. . . . 5
⊢ ;18 ∈
ℕ0 |
| 18 | | 3nn0 12544 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
| 19 | 2, 18 | deccl 12748 |
. . . . 5
⊢ ;13 ∈
ℕ0 |
| 20 | | 9nn0 12550 |
. . . . 5
⊢ 9 ∈
ℕ0 |
| 21 | | eqid 2737 |
. . . . 5
⊢ ;;139 = ;;139 |
| 22 | | 6nn0 12547 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
| 23 | 2, 22 | deccl 12748 |
. . . . 5
⊢ ;16 ∈
ℕ0 |
| 24 | | eqid 2737 |
. . . . . 6
⊢ ;13 = ;13 |
| 25 | | eqid 2737 |
. . . . . 6
⊢ ;16 = ;16 |
| 26 | | 7nn0 12548 |
. . . . . . 7
⊢ 7 ∈
ℕ0 |
| 27 | | eqid 2737 |
. . . . . . 7
⊢ ;18 = ;18 |
| 28 | | 6cn 12357 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
| 29 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 30 | | 6p1e7 12414 |
. . . . . . . . 9
⊢ (6 + 1) =
7 |
| 31 | 28, 29, 30 | addcomli 11453 |
. . . . . . . 8
⊢ (1 + 6) =
7 |
| 32 | 26 | dec0h 12755 |
. . . . . . . 8
⊢ 7 = ;07 |
| 33 | 31, 32 | eqtri 2765 |
. . . . . . 7
⊢ (1 + 6) =
;07 |
| 34 | 29 | mulridi 11265 |
. . . . . . . . 9
⊢ (1
· 1) = 1 |
| 35 | 29 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
| 36 | 34, 35 | oveq12i 7443 |
. . . . . . . 8
⊢ ((1
· 1) + (0 + 1)) = (1 + 1) |
| 37 | | 1p1e2 12391 |
. . . . . . . 8
⊢ (1 + 1) =
2 |
| 38 | 36, 37 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 1) + (0 + 1)) = 2 |
| 39 | | 8cn 12363 |
. . . . . . . . . 10
⊢ 8 ∈
ℂ |
| 40 | 39 | mulridi 11265 |
. . . . . . . . 9
⊢ (8
· 1) = 8 |
| 41 | 40 | oveq1i 7441 |
. . . . . . . 8
⊢ ((8
· 1) + 7) = (8 + 7) |
| 42 | | 8p7e15 12818 |
. . . . . . . 8
⊢ (8 + 7) =
;15 |
| 43 | 41, 42 | eqtri 2765 |
. . . . . . 7
⊢ ((8
· 1) + 7) = ;15 |
| 44 | 2, 16, 9, 26, 27, 33, 2, 7, 2,
38, 43 | decmac 12785 |
. . . . . 6
⊢ ((;18 · 1) + (1 + 6)) = ;25 |
| 45 | 22 | dec0h 12755 |
. . . . . . 7
⊢ 6 = ;06 |
| 46 | | 3cn 12347 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
| 47 | 46 | mullidi 11266 |
. . . . . . . . 9
⊢ (1
· 3) = 3 |
| 48 | 46 | addlidi 11449 |
. . . . . . . . 9
⊢ (0 + 3) =
3 |
| 49 | 47, 48 | oveq12i 7443 |
. . . . . . . 8
⊢ ((1
· 3) + (0 + 3)) = (3 + 3) |
| 50 | | 3p3e6 12418 |
. . . . . . . 8
⊢ (3 + 3) =
6 |
| 51 | 49, 50 | eqtri 2765 |
. . . . . . 7
⊢ ((1
· 3) + (0 + 3)) = 6 |
| 52 | | 4nn0 12545 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
| 53 | | 8t3e24 12849 |
. . . . . . . 8
⊢ (8
· 3) = ;24 |
| 54 | | 4cn 12351 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
| 55 | | 6p4e10 12805 |
. . . . . . . . 9
⊢ (6 + 4) =
;10 |
| 56 | 28, 54, 55 | addcomli 11453 |
. . . . . . . 8
⊢ (4 + 6) =
;10 |
| 57 | 6, 52, 22, 53, 11, 56 | decaddci2 12795 |
. . . . . . 7
⊢ ((8
· 3) + 6) = ;30 |
| 58 | 2, 16, 9, 22, 27, 45, 18, 9, 18, 51, 57 | decmac 12785 |
. . . . . 6
⊢ ((;18 · 3) + 6) = ;60 |
| 59 | 2, 18, 2, 22, 24, 25, 17, 9, 22, 44, 58 | decma2c 12786 |
. . . . 5
⊢ ((;18 · ;13) + ;16) = ;;250 |
| 60 | | 9cn 12366 |
. . . . . . . . 9
⊢ 9 ∈
ℂ |
| 61 | 60 | mullidi 11266 |
. . . . . . . 8
⊢ (1
· 9) = 9 |
| 62 | 61 | oveq1i 7441 |
. . . . . . 7
⊢ ((1
· 9) + 7) = (9 + 7) |
| 63 | | 9p7e16 12825 |
. . . . . . 7
⊢ (9 + 7) =
;16 |
| 64 | 62, 63 | eqtri 2765 |
. . . . . 6
⊢ ((1
· 9) + 7) = ;16 |
| 65 | | 9t8e72 12861 |
. . . . . . 7
⊢ (9
· 8) = ;72 |
| 66 | 60, 39, 65 | mulcomli 11270 |
. . . . . 6
⊢ (8
· 9) = ;72 |
| 67 | 20, 2, 16, 27, 6, 26, 64, 66 | decmul1c 12798 |
. . . . 5
⊢ (;18 · 9) = ;;162 |
| 68 | 17, 19, 20, 21, 6, 23, 59, 67 | decmul2c 12799 |
. . . 4
⊢ (;18 · ;;139) =
;;;2502 |
| 69 | 10, 6 | deccl 12748 |
. . . . . 6
⊢ ;;;2502
∈ ℕ0 |
| 70 | 69 | nn0cni 12538 |
. . . . 5
⊢ ;;;2502
∈ ℂ |
| 71 | 70, 29 | pncan3oi 11524 |
. . . 4
⊢ ((;;;2502 +
1) − 1) = ;;;2502 |
| 72 | 68, 71 | eqtr4i 2768 |
. . 3
⊢ (;18 · ;;139) =
((;;;2502 +
1) − 1) |
| 73 | 15, 72 | eqtr4i 2768 |
. 2
⊢ (𝑁 − 1) = (;18 · ;;139) |
| 74 | 10, 18 | deccl 12748 |
. . . . . 6
⊢ ;;;2503
∈ ℕ0 |
| 75 | 5, 74 | eqeltri 2837 |
. . . . 5
⊢ 𝑁 ∈
ℕ0 |
| 76 | 75 | nn0cni 12538 |
. . . 4
⊢ 𝑁 ∈ ℂ |
| 77 | | npcan 11517 |
. . . 4
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
| 78 | 76, 29, 77 | mp2an 692 |
. . 3
⊢ ((𝑁 − 1) + 1) = 𝑁 |
| 79 | 78 | eqcomi 2746 |
. 2
⊢ 𝑁 = ((𝑁 − 1) + 1) |
| 80 | | 1nn 12277 |
. 2
⊢ 1 ∈
ℕ |
| 81 | | 2nn 12339 |
. 2
⊢ 2 ∈
ℕ |
| 82 | 19, 20 | deccl 12748 |
. . . . 5
⊢ ;;139 ∈ ℕ0 |
| 83 | 82 | numexp1 17114 |
. . . 4
⊢ (;;139↑1) = ;;139 |
| 84 | 83 | oveq2i 7442 |
. . 3
⊢ (;18 · (;;139↑1)) = (;18 · ;;139) |
| 85 | 73, 84 | eqtr4i 2768 |
. 2
⊢ (𝑁 − 1) = (;18 · (;;139↑1)) |
| 86 | | 8lt10 12865 |
. . . 4
⊢ 8 <
;10 |
| 87 | | 1lt10 12872 |
. . . . 5
⊢ 1 <
;10 |
| 88 | 80, 18, 2, 87 | declti 12771 |
. . . 4
⊢ 1 <
;13 |
| 89 | 2, 19, 16, 20, 86, 88 | decltc 12762 |
. . 3
⊢ ;18 < ;;139 |
| 90 | 89, 83 | breqtrri 5170 |
. 2
⊢ ;18 < (;;139↑1) |
| 91 | 5 | 2503lem2 17175 |
. 2
⊢
((2↑(𝑁 −
1)) mod 𝑁) = (1 mod 𝑁) |
| 92 | 5 | 2503lem3 17176 |
. 2
⊢
(((2↑;18) − 1)
gcd 𝑁) = 1 |
| 93 | 1, 4, 73, 79, 4, 80, 81, 85, 90, 91, 92 | pockthi 16945 |
1
⊢ 𝑁 ∈ ℙ |