Proof of Theorem powm2modprm
Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝑃 ∈ ℙ) |
2 | | simpr 477 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝐴 ∈
ℤ) |
3 | 2 | adantr 481 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝐴 ∈ ℤ) |
4 | | m1dvdsndvds 15503 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ (𝐴 − 1) → ¬ 𝑃 ∥ 𝐴)) |
5 | 4 | imp 445 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ¬ 𝑃 ∥ 𝐴) |
6 | | eqid 2622 |
. . . . . 6
⊢ ((𝐴↑(𝑃 − 2)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃) |
7 | 6 | modprminv 15504 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬
𝑃 ∥ 𝐴) → (((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1)) |
8 | | simpr 477 |
. . . . . 6
⊢ ((((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) → ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = 1) |
9 | 8 | eqcomd 2628 |
. . . . 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 1326 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 1 = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
12 | | modprm1div 15502 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑃) = 1 ↔ 𝑃 ∥ (𝐴 − 1))) |
13 | 12 | biimpar 502 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (𝐴 mod 𝑃) = 1) |
14 | 13 | oveq1d 6665 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴 mod 𝑃) · ((𝐴↑(𝑃 − 2)) mod 𝑃)) = (1 · ((𝐴↑(𝑃 − 2)) mod 𝑃))) |
15 | 14 | oveq1d 6665 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (((𝐴 mod 𝑃) · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((1 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
16 | | zre 11381 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
17 | 16 | ad2antlr 763 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝐴 ∈ ℝ) |
18 | | prmm2nn0 15410 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈
ℕ0) |
19 | 18 | anim2i 593 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℙ) → (𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0)) |
20 | 19 | ancoms 469 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0)) |
21 | 20 | adantr 481 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0)) |
22 | | zexpcl 12875 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
24 | | prmnn 15388 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
25 | 24 | adantr 481 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝑃 ∈
ℕ) |
26 | 25 | adantr 481 |
. . . . . . 7
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝑃 ∈ ℕ) |
27 | 23, 26 | zmodcld 12691 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈
ℕ0) |
28 | 27 | nn0zd 11480 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ ℤ) |
29 | 24 | nnrpd 11870 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ+) |
30 | 29 | adantr 481 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → 𝑃 ∈
ℝ+) |
31 | 30 | adantr 481 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → 𝑃 ∈
ℝ+) |
32 | | modmulmod 12735 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℝ+) → (((𝐴 mod 𝑃) · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
33 | 17, 28, 31, 32 | syl3anc 1326 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (((𝐴 mod 𝑃) · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
34 | 20, 22 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴↑(𝑃 − 2)) ∈
ℤ) |
35 | 34, 25 | zmodcld 12691 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈
ℕ0) |
36 | 35 | nn0cnd 11353 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑(𝑃 − 2)) mod 𝑃) ∈ ℂ) |
37 | 36 | mulid2d 10058 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (1
· ((𝐴↑(𝑃 − 2)) mod 𝑃)) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
38 | 37 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((1
· ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃)) |
39 | 38 | adantr 481 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((1 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃)) |
40 | | reexpcl 12877 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝑃 − 2) ∈
ℕ0) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
41 | 16, 18, 40 | syl2anr 495 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝐴↑(𝑃 − 2)) ∈
ℝ) |
42 | 41, 30 | jca 554 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
43 | 42 | adantr 481 |
. . . . . 6
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈
ℝ+)) |
44 | | modabs2 12704 |
. . . . . 6
⊢ (((𝐴↑(𝑃 − 2)) ∈ ℝ ∧ 𝑃 ∈ ℝ+)
→ (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
45 | 43, 44 | syl 17 |
. . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → (((𝐴↑(𝑃 − 2)) mod 𝑃) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
46 | 39, 45 | eqtrd 2656 |
. . . 4
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((1 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
47 | 15, 33, 46 | 3eqtr3d 2664 |
. . 3
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴 · ((𝐴↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = ((𝐴↑(𝑃 − 2)) mod 𝑃)) |
48 | 11, 47 | eqtr2d 2657 |
. 2
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) ∧ 𝑃 ∥ (𝐴 − 1)) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = 1) |
49 | 48 | ex 450 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ (𝐴 − 1) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = 1)) |