Proof of Theorem lgslem1
Step | Hyp | Ref
| Expression |
1 | | eldifi 4061 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
2 | 1 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℙ) |
3 | | prmnn 16379 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ) |
5 | | simp1 1135 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
6 | | prmz 16380 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
7 | 2, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℤ) |
8 | 5, 7 | gcdcomd 16221 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
9 | | simp3 1137 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 𝐴) |
10 | | coprm 16416 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
11 | 2, 5, 10 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
12 | 9, 11 | mpbid 231 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 gcd 𝐴) = 1) |
13 | 8, 12 | eqtrd 2778 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = 1) |
14 | | eulerth 16484 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
15 | 4, 5, 13, 14 | syl3anc 1370 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
16 | | phiprm 16478 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
17 | 2, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − 1)) |
18 | | nnm1nn0 12274 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
19 | 4, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
ℕ0) |
20 | 17, 19 | eqeltrd 2839 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) ∈
ℕ0) |
21 | | zexpcl 13797 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑃) ∈
ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
22 | 5, 20, 21 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
23 | | 1zzd 12351 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈
ℤ) |
24 | | moddvds 15974 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
25 | 4, 22, 23, 24 | syl3anc 1370 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
26 | 15, 25 | mpbid 231 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)) |
27 | 19 | nn0cnd 12295 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈ ℂ) |
28 | | 2cnd 12051 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℂ) |
29 | | 2ne0 12077 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ≠
0) |
31 | 27, 28, 30 | divcan1d 11752 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1)) |
32 | 17, 31 | eqtr4d 2781 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (((𝑃 − 1) / 2) ·
2)) |
33 | 32 | oveq2d 7291 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑(((𝑃 − 1) / 2) ·
2))) |
34 | 5 | zcnd 12427 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ) |
35 | | 2nn0 12250 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
36 | 35 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℕ0) |
37 | | oddprm 16511 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
38 | 37 | 3ad2ant2 1133 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ) |
39 | 38 | nnnn0d 12293 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ0) |
40 | 34, 36, 39 | expmuld 13867 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(((𝑃 − 1) / 2) · 2)) = ((𝐴↑((𝑃 − 1) / 2))↑2)) |
41 | 33, 40 | eqtrd 2778 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = ((𝐴↑((𝑃 − 1) / 2))↑2)) |
42 | 41 | oveq1d 7290 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
1)) |
43 | | sq1 13912 |
. . . . . . . 8
⊢
(1↑2) = 1 |
44 | 43 | oveq2i 7286 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
1) |
45 | 42, 44 | eqtr4di 2796 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2))) |
46 | | zexpcl 13797 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
47 | 5, 39, 46 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
48 | 47 | zcnd 12427 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℂ) |
49 | | ax-1cn 10929 |
. . . . . . 7
⊢ 1 ∈
ℂ |
50 | | subsq 13926 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2)) ∈ ℂ ∧ 1
∈ ℂ) → (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
51 | 48, 49, 50 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
52 | 45, 51 | eqtrd 2778 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
53 | 26, 52 | breqtrd 5100 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
54 | 47 | peano2zd 12429 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈
ℤ) |
55 | | peano2zm 12363 |
. . . . . 6
⊢ ((𝐴↑((𝑃 − 1) / 2)) ∈ ℤ →
((𝐴↑((𝑃 − 1) / 2)) − 1)
∈ ℤ) |
56 | 47, 55 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) − 1) ∈
ℤ) |
57 | | euclemma 16418 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ ∧
((𝐴↑((𝑃 − 1) / 2)) − 1)
∈ ℤ) → (𝑃
∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) ·
((𝐴↑((𝑃 − 1) / 2)) − 1))
↔ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1)))) |
58 | 2, 54, 56, 57 | syl3anc 1370 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1)))) |
59 | 53, 58 | mpbid 231 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
60 | | dvdsval3 15967 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
→ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0)) |
61 | 4, 54, 60 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0)) |
62 | | 2z 12352 |
. . . . . . 7
⊢ 2 ∈
ℤ |
63 | 62 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℤ) |
64 | | moddvds 15974 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ ∧
2 ∈ ℤ) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
2))) |
65 | 4, 54, 63, 64 | syl3anc 1370 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
2))) |
66 | | 2re 12047 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
67 | 66 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℝ) |
68 | 4 | nnrpd 12770 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
69 | | 0le2 12075 |
. . . . . . . 8
⊢ 0 ≤
2 |
70 | 69 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 0 ≤
2) |
71 | 4 | nnred 11988 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℝ) |
72 | | prmuz2 16401 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
73 | 2, 72 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈
(ℤ≥‘2)) |
74 | | eluzle 12595 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
75 | 73, 74 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ≤ 𝑃) |
76 | | eldifsni 4723 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
77 | 76 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ≠ 2) |
78 | 67, 71, 75, 77 | leneltd 11129 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 < 𝑃) |
79 | | modid 13616 |
. . . . . . 7
⊢ (((2
∈ ℝ ∧ 𝑃
∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2) |
80 | 67, 68, 70, 78, 79 | syl22anc 836 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (2 mod 𝑃) = 2) |
81 | 80 | eqeq2d 2749 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
82 | | df-2 12036 |
. . . . . . . 8
⊢ 2 = (1 +
1) |
83 | 82 | oveq2i 7286 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 +
1)) |
84 | 49 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈
ℂ) |
85 | 48, 84, 84 | pnpcan2d 11370 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 + 1)) =
((𝐴↑((𝑃 − 1) / 2)) −
1)) |
86 | 83, 85 | eqtrid 2790 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = ((𝐴↑((𝑃 − 1) / 2)) −
1)) |
87 | 86 | breq2d 5086 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) ↔
𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
88 | 65, 81, 87 | 3bitr3rd 310 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
89 | 61, 88 | orbi12d 916 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔
((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))) |
90 | 59, 89 | mpbid 231 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
91 | | ovex 7308 |
. . 3
⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ V |
92 | 91 | elpr 4584 |
. 2
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2} ↔ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
93 | 90, 92 | sylibr 233 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2}) |