Proof of Theorem fermltl
Step | Hyp | Ref
| Expression |
1 | | prmnn 15226 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
2 | | dvdsval3 14825 |
. . . 4
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ 𝐴 ↔ (𝐴 mod 𝑃) = 0)) |
3 | 1, 2 | sylan 487 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ 𝐴 ↔ (𝐴 mod 𝑃) = 0)) |
4 | | simp2 1055 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → 𝐴 ∈ ℤ) |
5 | | 0zd 11266 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → 0 ∈
ℤ) |
6 | 1 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → 𝑃 ∈ ℕ) |
7 | 6 | nnnn0d 11228 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → 𝑃 ∈
ℕ0) |
8 | 6 | nnrpd 11746 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → 𝑃 ∈
ℝ+) |
9 | | simp3 1056 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → (𝐴 mod 𝑃) = 0) |
10 | | 0mod 12563 |
. . . . . . . 8
⊢ (𝑃 ∈ ℝ+
→ (0 mod 𝑃) =
0) |
11 | 8, 10 | syl 17 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → (0 mod 𝑃) = 0) |
12 | 9, 11 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → (𝐴 mod 𝑃) = (0 mod 𝑃)) |
13 | | modexp 12861 |
. . . . . 6
⊢ (((𝐴 ∈ ℤ ∧ 0 ∈
ℤ) ∧ (𝑃 ∈
ℕ0 ∧ 𝑃
∈ ℝ+) ∧ (𝐴 mod 𝑃) = (0 mod 𝑃)) → ((𝐴↑𝑃) mod 𝑃) = ((0↑𝑃) mod 𝑃)) |
14 | 4, 5, 7, 8, 12, 13 | syl221anc 1329 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → ((𝐴↑𝑃) mod 𝑃) = ((0↑𝑃) mod 𝑃)) |
15 | 6 | 0expd 12886 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → (0↑𝑃) = 0) |
16 | 15 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → ((0↑𝑃) mod 𝑃) = (0 mod 𝑃)) |
17 | 12, 16 | eqtr4d 2647 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → (𝐴 mod 𝑃) = ((0↑𝑃) mod 𝑃)) |
18 | 14, 17 | eqtr4d 2647 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 mod 𝑃) = 0) → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃)) |
19 | 18 | 3expia 1259 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑃) = 0 → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃))) |
20 | 3, 19 | sylbid 229 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ 𝐴 → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃))) |
21 | | coprm 15261 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
22 | | prmz 15227 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
23 | | gcdcom 15073 |
. . . . . 6
⊢ ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑃 gcd 𝐴) = (𝐴 gcd 𝑃)) |
24 | 22, 23 | sylan 487 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 gcd 𝐴) = (𝐴 gcd 𝑃)) |
25 | 24 | eqeq1d 2612 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝑃 gcd 𝐴) = 1 ↔ (𝐴 gcd 𝑃) = 1)) |
26 | 21, 25 | bitrd 267 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝐴 gcd 𝑃) = 1)) |
27 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 𝐴 ∈ ℤ) |
28 | 1 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 𝑃 ∈ ℕ) |
29 | 28 | phicld 15315 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (ϕ‘𝑃) ∈
ℕ) |
30 | 29 | nnnn0d 11228 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (ϕ‘𝑃) ∈
ℕ0) |
31 | | zexpcl 12737 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑃) ∈
ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
32 | 27, 30, 31 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
33 | 32 | zred 11358 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (𝐴↑(ϕ‘𝑃)) ∈ ℝ) |
34 | | 1red 9934 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 1 ∈
ℝ) |
35 | 28 | nnrpd 11746 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 𝑃 ∈
ℝ+) |
36 | | eulerth 15326 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
37 | 1, 36 | syl3an1 1351 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
38 | | modmul1 12585 |
. . . . . 6
⊢ ((((𝐴↑(ϕ‘𝑃)) ∈ ℝ ∧ 1 ∈
ℝ) ∧ (𝐴 ∈
ℤ ∧ 𝑃 ∈
ℝ+) ∧ ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) → (((𝐴↑(ϕ‘𝑃)) · 𝐴) mod 𝑃) = ((1 · 𝐴) mod 𝑃)) |
39 | 33, 34, 27, 35, 37, 38 | syl221anc 1329 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (((𝐴↑(ϕ‘𝑃)) · 𝐴) mod 𝑃) = ((1 · 𝐴) mod 𝑃)) |
40 | | phiprm 15320 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
41 | 40 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (ϕ‘𝑃) = (𝑃 − 1)) |
42 | 41 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑(𝑃 − 1))) |
43 | 42 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) · 𝐴) = ((𝐴↑(𝑃 − 1)) · 𝐴)) |
44 | 27 | zcnd 11359 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → 𝐴 ∈ ℂ) |
45 | | expm1t 12750 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑃 ∈ ℕ) → (𝐴↑𝑃) = ((𝐴↑(𝑃 − 1)) · 𝐴)) |
46 | 44, 28, 45 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (𝐴↑𝑃) = ((𝐴↑(𝑃 − 1)) · 𝐴)) |
47 | 43, 46 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) · 𝐴) = (𝐴↑𝑃)) |
48 | 47 | oveq1d 6564 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (((𝐴↑(ϕ‘𝑃)) · 𝐴) mod 𝑃) = ((𝐴↑𝑃) mod 𝑃)) |
49 | 44 | mulid2d 9937 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → (1 · 𝐴) = 𝐴) |
50 | 49 | oveq1d 6564 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((1 · 𝐴) mod 𝑃) = (𝐴 mod 𝑃)) |
51 | 39, 48, 50 | 3eqtr3d 2652 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃)) |
52 | 51 | 3expia 1259 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝑃) = 1 → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃))) |
53 | 26, 52 | sylbid 229 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃))) |
54 | 20, 53 | pm2.61d 169 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃)) |