Proof of Theorem powm2modprm
| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝑃 ∈ ℙ) |
| 2 | | simpr 484 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝐴 ∈
ℤ) |
| 3 | 2 | adantr 480 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝐴 ∈ ℤ) |
| 4 | | m1dvdsndvds 16836 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ (𝐴 − 1) → ¬ 𝑃 ∥ 𝐴)) |
| 5 | 4 | imp 406 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ¬ 𝑃 ∥ 𝐴) |
| 6 | | eqid 2737 |
. . . . . 6
⊢ ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃) |
| 7 | 6 | modprminv 16837 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) |
| 8 | | simpr 484 |
. . . . . 6
⊢ ((((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) → ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) |
| 9 | 8 | eqcomd 2743 |
. . . . 5
⊢ ((((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) → 1 = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 10 | 7, 9 | syl 17 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → 1 = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 11 | 1, 3, 5, 10 | syl3anc 1373 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 1 = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 12 | | modprm1div 16835 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑃) = 1 ↔ 𝑃 ∥ (𝐴 − 1))) |
| 13 | 12 | biimpar 477 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (𝐴 mod 𝑃) = 1) |
| 14 | 13 | oveq1d 7446 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴 mod 𝑃) · ((𝐴↑(𝑃 − 2)) mod 𝑃)) = (1 · ((𝐴↑(𝑃 − 2)) mod 𝑃))) |
| 15 | 14 | oveq1d 7446 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (((𝐴 mod 𝑃) · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((1 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 16 | | zre 12617 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
| 17 | 16 | ad2antlr 727 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝐴 ∈ ℝ) |
| 18 | | prmm2nn0 16735 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈
ℕ0) |
| 19 | 18 | anim1ci 616 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0)) |
| 20 | 19 | adantr 480 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0)) |
| 21 | | zexpcl 14117 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
| 22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
| 23 | | prmnn 16711 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝑃 ∈
ℕ) |
| 25 | 24 | adantr 480 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝑃 ∈ ℕ) |
| 26 | 22, 25 | zmodcld 13932 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈
ℕ0) |
| 27 | 26 | nn0zd 12639 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ ℤ) |
| 28 | 23 | nnrpd 13075 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ+) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝑃 ∈
ℝ+) |
| 30 | 29 | adantr 480 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝑃 ∈
ℝ+) |
| 31 | | modmulmod 13977 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℝ+) → (((𝐴 mod 𝑃) · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 32 | 17, 27, 30, 31 | syl3anc 1373 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (((𝐴 mod 𝑃) · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 33 | 19, 21 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
| 34 | 33, 24 | zmodcld 13932 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈
ℕ0) |
| 35 | 34 | nn0cnd 12589 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ ℂ) |
| 36 | 35 | mullidd 11279 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (1
· ((𝐴↑(𝑃 − 2)) mod 𝑃)) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
| 37 | 36 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((1
· ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃)) |
| 38 | 37 | adantr 480 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((1 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃)) |
| 39 | | reexpcl 14119 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
| 40 | 16, 18, 39 | syl2anr 597 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
| 41 | 40, 29 | jca 511 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
| 42 | 41 | adantr 480 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
| 43 | | modabs2 13945 |
. . . . . 6
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
| 44 | 42, 43 | syl 17 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
| 45 | 38, 44 | eqtrd 2777 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((1 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
| 46 | 15, 32, 45 | 3eqtr3d 2785 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
| 47 | 11, 46 | eqtr2d 2778 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = 1) |
| 48 | 47 | ex 412 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ (𝐴 − 1) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = 1)) |