Proof of Theorem lgslem1
Step | Hyp | Ref
| Expression |
1 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
2 | 1 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℙ) |
3 | | prmnn 15226 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ) |
5 | | simp1 1054 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
6 | | prmz 15227 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
7 | 2, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℤ) |
8 | | gcdcom 15073 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
9 | 5, 7, 8 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
10 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 𝐴) |
11 | | coprm 15261 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
12 | 2, 5, 11 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
13 | 10, 12 | mpbid 221 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 gcd 𝐴) = 1) |
14 | 9, 13 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = 1) |
15 | | eulerth 15326 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
16 | 4, 5, 14, 15 | syl3anc 1318 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
17 | | phiprm 15320 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
18 | 2, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − 1)) |
19 | | nnm1nn0 11211 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
20 | 4, 19 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
ℕ0) |
21 | 18, 20 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) ∈
ℕ0) |
22 | | zexpcl 12737 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑃) ∈
ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
23 | 5, 21, 22 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
24 | | 1zzd 11285 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈
ℤ) |
25 | | moddvds 14829 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
26 | 4, 23, 24, 25 | syl3anc 1318 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
27 | 16, 26 | mpbid 221 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)) |
28 | 20 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈ ℂ) |
29 | | 2cnd 10970 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℂ) |
30 | | 2ne0 10990 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
31 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ≠
0) |
32 | 28, 29, 31 | divcan1d 10681 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1)) |
33 | 18, 32 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (((𝑃 − 1) / 2) ·
2)) |
34 | 33 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑(((𝑃 − 1) / 2) ·
2))) |
35 | 5 | zcnd 11359 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ) |
36 | | 2nn0 11186 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℕ0) |
38 | | oddprm 15353 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
39 | 38 | 3ad2ant2 1076 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ) |
40 | 39 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ0) |
41 | 35, 37, 40 | expmuld 12873 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(((𝑃 − 1) / 2) · 2)) = ((𝐴↑((𝑃 − 1) / 2))↑2)) |
42 | 34, 41 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = ((𝐴↑((𝑃 − 1) / 2))↑2)) |
43 | 42 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
1)) |
44 | | sq1 12820 |
. . . . . . . 8
⊢
(1↑2) = 1 |
45 | 44 | oveq2i 6560 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
1) |
46 | 43, 45 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2))) |
47 | | zexpcl 12737 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
48 | 5, 40, 47 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
49 | 48 | zcnd 11359 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℂ) |
50 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
51 | | subsq 12834 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2)) ∈ ℂ ∧ 1
∈ ℂ) → (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
52 | 49, 50, 51 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
53 | 46, 52 | eqtrd 2644 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
54 | 27, 53 | breqtrd 4609 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
55 | 48 | peano2zd 11361 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈
ℤ) |
56 | | peano2zm 11297 |
. . . . . 6
⊢ ((𝐴↑((𝑃 − 1) / 2)) ∈ ℤ →
((𝐴↑((𝑃 − 1) / 2)) − 1)
∈ ℤ) |
57 | 48, 56 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) − 1) ∈
ℤ) |
58 | | euclemma 15263 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ ∧
((𝐴↑((𝑃 − 1) / 2)) − 1)
∈ ℤ) → (𝑃
∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) ·
((𝐴↑((𝑃 − 1) / 2)) − 1))
↔ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1)))) |
59 | 2, 55, 57, 58 | syl3anc 1318 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1)))) |
60 | 54, 59 | mpbid 221 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
61 | | dvdsval3 14825 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
→ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0)) |
62 | 4, 55, 61 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0)) |
63 | | 2z 11286 |
. . . . . . 7
⊢ 2 ∈
ℤ |
64 | 63 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℤ) |
65 | | moddvds 14829 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ ∧
2 ∈ ℤ) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
2))) |
66 | 4, 55, 64, 65 | syl3anc 1318 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
2))) |
67 | | 2re 10967 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
68 | 67 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℝ) |
69 | 4 | nnrpd 11746 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
70 | | 0le2 10988 |
. . . . . . . 8
⊢ 0 ≤
2 |
71 | 70 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 0 ≤
2) |
72 | | prmuz2 15246 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
73 | 2, 72 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈
(ℤ≥‘2)) |
74 | | eluzle 11576 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
75 | 73, 74 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ≤ 𝑃) |
76 | | eldifsni 4261 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
77 | 76 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ≠ 2) |
78 | 4 | nnred 10912 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℝ) |
79 | 68, 78 | ltlend 10061 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (2 < 𝑃 ↔ (2 ≤ 𝑃 ∧ 𝑃 ≠ 2))) |
80 | 75, 77, 79 | mpbir2and 959 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 < 𝑃) |
81 | | modid 12557 |
. . . . . . 7
⊢ (((2
∈ ℝ ∧ 𝑃
∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2) |
82 | 68, 69, 71, 80, 81 | syl22anc 1319 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (2 mod 𝑃) = 2) |
83 | 82 | eqeq2d 2620 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
84 | | df-2 10956 |
. . . . . . . 8
⊢ 2 = (1 +
1) |
85 | 84 | oveq2i 6560 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 +
1)) |
86 | 50 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈
ℂ) |
87 | 49, 86, 86 | pnpcan2d 10309 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 + 1)) =
((𝐴↑((𝑃 − 1) / 2)) −
1)) |
88 | 85, 87 | syl5eq 2656 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = ((𝐴↑((𝑃 − 1) / 2)) −
1)) |
89 | 88 | breq2d 4595 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) ↔
𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
90 | 66, 83, 89 | 3bitr3rd 298 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
91 | 62, 90 | orbi12d 742 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔
((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))) |
92 | 60, 91 | mpbid 221 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
93 | | ovex 6577 |
. . 3
⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ V |
94 | 93 | elpr 4146 |
. 2
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2} ↔ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
95 | 92, 94 | sylibr 223 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2}) |