Proof of Theorem lgslem1
Step | Hyp | Ref
| Expression |
1 | | eldifi 4106 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
2 | 1 | 3ad2ant2 1130 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℙ) |
3 | | prmnn 16021 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ) |
5 | | simp1 1132 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
6 | | prmz 16022 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
7 | 2, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℤ) |
8 | | gcdcom 15865 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
9 | 5, 7, 8 | syl2anc 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
10 | | simp3 1134 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 𝐴) |
11 | | coprm 16058 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
12 | 2, 5, 11 | syl2anc 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
13 | 10, 12 | mpbid 234 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 gcd 𝐴) = 1) |
14 | 9, 13 | eqtrd 2859 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = 1) |
15 | | eulerth 16123 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
16 | 4, 5, 14, 15 | syl3anc 1367 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
17 | | phiprm 16117 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
18 | 2, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − 1)) |
19 | | nnm1nn0 11941 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
20 | 4, 19 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
ℕ0) |
21 | 18, 20 | eqeltrd 2916 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) ∈
ℕ0) |
22 | | zexpcl 13447 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑃) ∈
ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
23 | 5, 21, 22 | syl2anc 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
24 | | 1zzd 12016 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈
ℤ) |
25 | | moddvds 15621 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
26 | 4, 23, 24, 25 | syl3anc 1367 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
27 | 16, 26 | mpbid 234 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)) |
28 | 20 | nn0cnd 11960 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈ ℂ) |
29 | | 2cnd 11718 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℂ) |
30 | | 2ne0 11744 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
31 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ≠
0) |
32 | 28, 29, 31 | divcan1d 11420 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1)) |
33 | 18, 32 | eqtr4d 2862 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (((𝑃 − 1) / 2) ·
2)) |
34 | 33 | oveq2d 7175 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑(((𝑃 − 1) / 2) ·
2))) |
35 | 5 | zcnd 12091 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ) |
36 | | 2nn0 11917 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℕ0) |
38 | | oddprm 16150 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
39 | 38 | 3ad2ant2 1130 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ) |
40 | 39 | nnnn0d 11958 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ0) |
41 | 35, 37, 40 | expmuld 13516 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(((𝑃 − 1) / 2) · 2)) = ((𝐴↑((𝑃 − 1) / 2))↑2)) |
42 | 34, 41 | eqtrd 2859 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = ((𝐴↑((𝑃 − 1) / 2))↑2)) |
43 | 42 | oveq1d 7174 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
1)) |
44 | | sq1 13561 |
. . . . . . . 8
⊢
(1↑2) = 1 |
45 | 44 | oveq2i 7170 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
1) |
46 | 43, 45 | syl6eqr 2877 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2))) |
47 | | zexpcl 13447 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
48 | 5, 40, 47 | syl2anc 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
49 | 48 | zcnd 12091 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℂ) |
50 | | ax-1cn 10598 |
. . . . . . 7
⊢ 1 ∈
ℂ |
51 | | subsq 13575 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2)) ∈ ℂ ∧ 1
∈ ℂ) → (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
52 | 49, 50, 51 | sylancl 588 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
53 | 46, 52 | eqtrd 2859 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
54 | 27, 53 | breqtrd 5095 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
55 | 48 | peano2zd 12093 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈
ℤ) |
56 | | peano2zm 12028 |
. . . . . 6
⊢ ((𝐴↑((𝑃 − 1) / 2)) ∈ ℤ →
((𝐴↑((𝑃 − 1) / 2)) − 1)
∈ ℤ) |
57 | 48, 56 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) − 1) ∈
ℤ) |
58 | | euclemma 16060 |
. . . . 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 1367 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1)))) |
60 | 54, 59 | mpbid 234 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
61 | | dvdsval3 15614 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
→ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0)) |
62 | 4, 55, 61 | syl2anc 586 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0)) |
63 | | 2z 12017 |
. . . . . . 7
⊢ 2 ∈
ℤ |
64 | 63 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℤ) |
65 | | moddvds 15621 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ ∧
2 ∈ ℤ) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
2))) |
66 | 4, 55, 64, 65 | syl3anc 1367 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
2))) |
67 | | 2re 11714 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
68 | 67 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℝ) |
69 | 4 | nnrpd 12432 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
70 | | 0le2 11742 |
. . . . . . . 8
⊢ 0 ≤
2 |
71 | 70 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 0 ≤
2) |
72 | 4 | nnred 11656 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℝ) |
73 | | prmuz2 16043 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
74 | 2, 73 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈
(ℤ≥‘2)) |
75 | | eluzle 12259 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
76 | 74, 75 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ≤ 𝑃) |
77 | | eldifsni 4725 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
78 | 77 | 3ad2ant2 1130 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ≠ 2) |
79 | 68, 72, 76, 78 | leneltd 10797 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 < 𝑃) |
80 | | modid 13267 |
. . . . . . 7
⊢ (((2
∈ ℝ ∧ 𝑃
∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2) |
81 | 68, 69, 71, 79, 80 | syl22anc 836 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (2 mod 𝑃) = 2) |
82 | 81 | eqeq2d 2835 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
83 | | df-2 11703 |
. . . . . . . 8
⊢ 2 = (1 +
1) |
84 | 83 | oveq2i 7170 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 +
1)) |
85 | 50 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈
ℂ) |
86 | 49, 85, 85 | pnpcan2d 11038 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 + 1)) =
((𝐴↑((𝑃 − 1) / 2)) −
1)) |
87 | 84, 86 | syl5eq 2871 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = ((𝐴↑((𝑃 − 1) / 2)) −
1)) |
88 | 87 | breq2d 5081 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) ↔
𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
89 | 66, 82, 88 | 3bitr3rd 312 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
90 | 62, 89 | orbi12d 915 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔
((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))) |
91 | 60, 90 | mpbid 234 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
92 | | ovex 7192 |
. . 3
⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ V |
93 | 92 | elpr 4593 |
. 2
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2} ↔ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
94 | 91, 93 | sylibr 236 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2}) |