Proof of Theorem vfermltlALT
| Step | Hyp | Ref
| Expression |
| 1 | | 2m1e1 12392 |
. . . . . . . . . . 11
⊢ (2
− 1) = 1 |
| 2 | 1 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → (2
− 1) = 1) |
| 3 | 2 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 1 = (2
− 1)) |
| 4 | 3 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → (𝑃 − 1) = (𝑃 − (2 − 1))) |
| 5 | | prmz 16712 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 6 | 5 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℂ) |
| 7 | | 2cnd 12344 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 2 ∈
ℂ) |
| 8 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 1 ∈
ℂ) |
| 9 | 6, 7, 8 | subsubd 11648 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → (𝑃 − (2 − 1)) =
((𝑃 − 2) +
1)) |
| 10 | 4, 9 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → (𝑃 − 1) = ((𝑃 − 2) +
1)) |
| 11 | 10 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 1) = ((𝑃 − 2) + 1)) |
| 12 | 11 | oveq2d 7447 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 1)) = (𝐴↑((𝑃 − 2) + 1))) |
| 13 | | zcn 12618 |
. . . . . . 7
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
| 14 | 13 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ) |
| 15 | | prmm2nn0 16735 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈
ℕ0) |
| 16 | 15 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝑃 − 2) ∈
ℕ0) |
| 17 | 14, 16 | expp1d 14187 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 2) + 1)) = ((𝐴↑(𝑃 − 2)) · 𝐴)) |
| 18 | 12, 17 | eqtrd 2777 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 1)) = ((𝐴↑(𝑃 − 2)) · 𝐴)) |
| 19 | 18 | oveq1d 7446 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 1)) mod 𝑃) = (((𝐴↑(𝑃 − 2)) · 𝐴) mod 𝑃)) |
| 20 | 15 | anim1i 615 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝑃 − 2) ∈
ℕ0 ∧ 𝐴
∈ ℤ)) |
| 21 | 20 | ancomd 461 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0)) |
| 22 | | zexpcl 14117 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
| 23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
| 24 | 23 | zred 12722 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
| 25 | 24 | 3adant3 1133 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
| 26 | | simp2 1138 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
| 27 | | prmnn 16711 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 28 | 27 | nnrpd 13075 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ+) |
| 29 | 28 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
| 30 | | modmulmod 13977 |
. . . 4
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℝ+)
→ ((((𝐴↑(𝑃 − 2)) mod 𝑃) · 𝐴) mod 𝑃) = (((𝐴↑(𝑃 − 2)) · 𝐴) mod 𝑃)) |
| 31 | 25, 26, 29, 30 | syl3anc 1373 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((((𝐴↑(𝑃 − 2)) mod 𝑃) · 𝐴) mod 𝑃) = (((𝐴↑(𝑃 − 2)) · 𝐴) mod 𝑃)) |
| 32 | | zre 12617 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
| 33 | 32 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝐴 ∈
ℝ) |
| 34 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 − 2) ∈
ℕ0) |
| 35 | 33, 34 | reexpcld 14203 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
| 36 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝑃 ∈
ℝ+) |
| 37 | 35, 36 | modcld 13915 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ ℝ) |
| 38 | 37 | recnd 11289 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ ℂ) |
| 39 | 13 | adantl 481 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝐴 ∈
ℂ) |
| 40 | 38, 39 | mulcomd 11282 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (((𝐴↑(𝑃 − 2)) mod 𝑃) · 𝐴) = (𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃))) |
| 41 | 40 | 3adant3 1133 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(𝑃 − 2)) mod 𝑃) · 𝐴) = (𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃))) |
| 42 | 41 | oveq1d 7446 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((((𝐴↑(𝑃 − 2)) mod 𝑃) · 𝐴) mod 𝑃) = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 43 | 19, 31, 42 | 3eqtr2d 2783 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 1)) mod 𝑃) = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 44 | | eqid 2737 |
. . . 4
⊢ ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃) |
| 45 | 44 | modprminv 16837 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) |
| 46 | 45 | simprd 495 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) |
| 47 | 43, 46 | eqtrd 2777 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 1)) mod 𝑃) = 1) |