Proof of Theorem 41prothprmlem2
| Step | Hyp | Ref
| Expression |
| 1 | | 41prothprm.p |
. . . . 5
⊢ 𝑃 = ;41 |
| 2 | 1 | 41prothprmlem1 47604 |
. . . 4
⊢ ((𝑃 − 1) / 2) = ;20 |
| 3 | 2 | oveq2i 7442 |
. . 3
⊢
(3↑((𝑃 −
1) / 2)) = (3↑;20) |
| 4 | 3 | oveq1i 7441 |
. 2
⊢
((3↑((𝑃 −
1) / 2)) mod 𝑃) =
((3↑;20) mod 𝑃) |
| 5 | | 5cn 12354 |
. . . . . . . . 9
⊢ 5 ∈
ℂ |
| 6 | | 4cn 12351 |
. . . . . . . . 9
⊢ 4 ∈
ℂ |
| 7 | | 5t4e20 12835 |
. . . . . . . . 9
⊢ (5
· 4) = ;20 |
| 8 | 5, 6, 7 | mulcomli 11270 |
. . . . . . . 8
⊢ (4
· 5) = ;20 |
| 9 | 8 | eqcomi 2746 |
. . . . . . 7
⊢ ;20 = (4 · 5) |
| 10 | 9 | oveq2i 7442 |
. . . . . 6
⊢
(3↑;20) = (3↑(4
· 5)) |
| 11 | | 3cn 12347 |
. . . . . . 7
⊢ 3 ∈
ℂ |
| 12 | | 4nn0 12545 |
. . . . . . 7
⊢ 4 ∈
ℕ0 |
| 13 | | 5nn0 12546 |
. . . . . . 7
⊢ 5 ∈
ℕ0 |
| 14 | | expmul 14148 |
. . . . . . 7
⊢ ((3
∈ ℂ ∧ 4 ∈ ℕ0 ∧ 5 ∈
ℕ0) → (3↑(4 · 5)) =
((3↑4)↑5)) |
| 15 | 11, 12, 13, 14 | mp3an 1463 |
. . . . . 6
⊢
(3↑(4 · 5)) = ((3↑4)↑5) |
| 16 | 10, 15 | eqtri 2765 |
. . . . 5
⊢
(3↑;20) =
((3↑4)↑5) |
| 17 | 16 | oveq1i 7441 |
. . . 4
⊢
((3↑;20) mod ;41) = (((3↑4)↑5) mod ;41) |
| 18 | | 3z 12650 |
. . . . . . 7
⊢ 3 ∈
ℤ |
| 19 | | zexpcl 14117 |
. . . . . . 7
⊢ ((3
∈ ℤ ∧ 4 ∈ ℕ0) → (3↑4) ∈
ℤ) |
| 20 | 18, 12, 19 | mp2an 692 |
. . . . . 6
⊢
(3↑4) ∈ ℤ |
| 21 | | neg1z 12653 |
. . . . . 6
⊢ -1 ∈
ℤ |
| 22 | 20, 21 | pm3.2i 470 |
. . . . 5
⊢
((3↑4) ∈ ℤ ∧ -1 ∈ ℤ) |
| 23 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 24 | 12, 23 | decnncl 12753 |
. . . . . . 7
⊢ ;41 ∈ ℕ |
| 25 | | nnrp 13046 |
. . . . . . 7
⊢ (;41 ∈ ℕ → ;41 ∈
ℝ+) |
| 26 | 24, 25 | ax-mp 5 |
. . . . . 6
⊢ ;41 ∈
ℝ+ |
| 27 | 13, 26 | pm3.2i 470 |
. . . . 5
⊢ (5 ∈
ℕ0 ∧ ;41
∈ ℝ+) |
| 28 | | 3exp4mod41 47603 |
. . . . 5
⊢
((3↑4) mod ;41) = (-1
mod ;41) |
| 29 | | modexp 14277 |
. . . . 5
⊢
((((3↑4) ∈ ℤ ∧ -1 ∈ ℤ) ∧ (5 ∈
ℕ0 ∧ ;41
∈ ℝ+) ∧ ((3↑4) mod ;41) = (-1 mod ;41)) → (((3↑4)↑5) mod ;41) = ((-1↑5) mod ;41)) |
| 30 | 22, 27, 28, 29 | mp3an 1463 |
. . . 4
⊢
(((3↑4)↑5) mod ;41) = ((-1↑5) mod ;41) |
| 31 | | 3p2e5 12417 |
. . . . . . . 8
⊢ (3 + 2) =
5 |
| 32 | 31 | eqcomi 2746 |
. . . . . . 7
⊢ 5 = (3 +
2) |
| 33 | 32 | oveq2i 7442 |
. . . . . 6
⊢
(-1↑5) = (-1↑(3 + 2)) |
| 34 | | 2z 12649 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
| 35 | | m1expaddsub 19516 |
. . . . . . . 8
⊢ ((3
∈ ℤ ∧ 2 ∈ ℤ) → (-1↑(3 − 2)) =
(-1↑(3 + 2))) |
| 36 | 18, 34, 35 | mp2an 692 |
. . . . . . 7
⊢
(-1↑(3 − 2)) = (-1↑(3 + 2)) |
| 37 | 36 | eqcomi 2746 |
. . . . . 6
⊢
(-1↑(3 + 2)) = (-1↑(3 − 2)) |
| 38 | | 2cn 12341 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
| 39 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 40 | | 2p1e3 12408 |
. . . . . . . . 9
⊢ (2 + 1) =
3 |
| 41 | 11, 38, 39, 40 | subaddrii 11598 |
. . . . . . . 8
⊢ (3
− 2) = 1 |
| 42 | 41 | oveq2i 7442 |
. . . . . . 7
⊢
(-1↑(3 − 2)) = (-1↑1) |
| 43 | | neg1cn 12380 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
| 44 | | exp1 14108 |
. . . . . . . 8
⊢ (-1
∈ ℂ → (-1↑1) = -1) |
| 45 | 43, 44 | ax-mp 5 |
. . . . . . 7
⊢
(-1↑1) = -1 |
| 46 | 42, 45 | eqtri 2765 |
. . . . . 6
⊢
(-1↑(3 − 2)) = -1 |
| 47 | 33, 37, 46 | 3eqtri 2769 |
. . . . 5
⊢
(-1↑5) = -1 |
| 48 | 47 | oveq1i 7441 |
. . . 4
⊢
((-1↑5) mod ;41) = (-1
mod ;41) |
| 49 | 17, 30, 48 | 3eqtri 2769 |
. . 3
⊢
((3↑;20) mod ;41) = (-1 mod ;41) |
| 50 | 1 | oveq2i 7442 |
. . 3
⊢
((3↑;20) mod 𝑃) = ((3↑;20) mod ;41) |
| 51 | 1 | oveq2i 7442 |
. . 3
⊢ (-1 mod
𝑃) = (-1 mod ;41) |
| 52 | 49, 50, 51 | 3eqtr4i 2775 |
. 2
⊢
((3↑;20) mod 𝑃) = (-1 mod 𝑃) |
| 53 | 4, 52 | eqtri 2765 |
1
⊢
((3↑((𝑃 −
1) / 2)) mod 𝑃) = (-1 mod
𝑃) |