Proof of Theorem lgslem1
Step | Hyp | Ref
| Expression |
1 | | eldifi 4054 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) |
2 | 1 | 3ad2ant2 1131 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℙ) |
3 | | prmnn 16008 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℕ) |
5 | | simp1 1133 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℤ) |
6 | | prmz 16009 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
7 | 2, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℤ) |
8 | | gcdcom 15852 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
9 | 5, 7, 8 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = (𝑃 gcd 𝐴)) |
10 | | simp3 1135 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ¬ 𝑃 ∥ 𝐴) |
11 | | coprm 16045 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (¬
𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
12 | 2, 5, 11 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (¬ 𝑃 ∥ 𝐴 ↔ (𝑃 gcd 𝐴) = 1)) |
13 | 10, 12 | mpbid 235 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 gcd 𝐴) = 1) |
14 | 9, 13 | eqtrd 2833 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴 gcd 𝑃) = 1) |
15 | | eulerth 16110 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑃) = 1) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
16 | 4, 5, 14, 15 | syl3anc 1368 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
17 | | phiprm 16104 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
18 | 2, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (𝑃 − 1)) |
19 | | nnm1nn0 11926 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
20 | 4, 19 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈
ℕ0) |
21 | 18, 20 | eqeltrd 2890 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) ∈
ℕ0) |
22 | | zexpcl 13440 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧
(ϕ‘𝑃) ∈
ℕ0) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
23 | 5, 21, 22 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) ∈ ℤ) |
24 | | 1zzd 12001 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈
ℤ) |
25 | | moddvds 15610 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ (𝐴↑(ϕ‘𝑃)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
26 | 4, 23, 24, 25 | syl3anc 1368 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1))) |
27 | 16, 26 | mpbid 235 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ ((𝐴↑(ϕ‘𝑃)) − 1)) |
28 | 20 | nn0cnd 11945 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 − 1) ∈ ℂ) |
29 | | 2cnd 11703 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℂ) |
30 | | 2ne0 11729 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
31 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ≠
0) |
32 | 28, 29, 31 | divcan1d 11406 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1)) |
33 | 18, 32 | eqtr4d 2836 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (ϕ‘𝑃) = (((𝑃 − 1) / 2) ·
2)) |
34 | 33 | oveq2d 7151 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = (𝐴↑(((𝑃 − 1) / 2) ·
2))) |
35 | 5 | zcnd 12076 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝐴 ∈ ℂ) |
36 | | 2nn0 11902 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
37 | 36 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℕ0) |
38 | | oddprm 16137 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
39 | 38 | 3ad2ant2 1131 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ) |
40 | 39 | nnnn0d 11943 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 − 1) / 2) ∈
ℕ0) |
41 | 35, 37, 40 | expmuld 13509 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(((𝑃 − 1) / 2) · 2)) = ((𝐴↑((𝑃 − 1) / 2))↑2)) |
42 | 34, 41 | eqtrd 2833 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑(ϕ‘𝑃)) = ((𝐴↑((𝑃 − 1) / 2))↑2)) |
43 | 42 | oveq1d 7150 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
1)) |
44 | | sq1 13554 |
. . . . . . . 8
⊢
(1↑2) = 1 |
45 | 44 | oveq2i 7146 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
1) |
46 | 43, 45 | eqtr4di 2851 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2))) |
47 | | zexpcl 13440 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
48 | 5, 40, 47 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℤ) |
49 | 48 | zcnd 12076 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝐴↑((𝑃 − 1) / 2)) ∈
ℂ) |
50 | | ax-1cn 10584 |
. . . . . . 7
⊢ 1 ∈
ℂ |
51 | | subsq 13568 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2)) ∈ ℂ ∧ 1
∈ ℂ) → (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
52 | 49, 50, 51 | sylancl 589 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2))↑2) −
(1↑2)) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
53 | 46, 52 | eqtrd 2833 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(ϕ‘𝑃)) − 1) = (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
54 | 27, 53 | breqtrd 5056 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
55 | 48 | peano2zd 12078 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈
ℤ) |
56 | | peano2zm 12013 |
. . . . . 6
⊢ ((𝐴↑((𝑃 − 1) / 2)) ∈ ℤ →
((𝐴↑((𝑃 − 1) / 2)) − 1)
∈ ℤ) |
57 | 48, 56 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑((𝑃 − 1) / 2)) − 1) ∈
ℤ) |
58 | | euclemma 16047 |
. . . . 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 1368 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) · ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1)))) |
60 | 54, 59 | mpbid 235 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
61 | | dvdsval3 15603 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ)
→ (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0)) |
62 | 4, 55, 61 | syl2anc 587 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0)) |
63 | | 2z 12002 |
. . . . . . 7
⊢ 2 ∈
ℤ |
64 | 63 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℤ) |
65 | | moddvds 15610 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∈ ℤ ∧
2 ∈ ℤ) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
2))) |
66 | 4, 55, 64, 65 | syl3anc 1368 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ 𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) −
2))) |
67 | | 2re 11699 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
68 | 67 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ∈
ℝ) |
69 | 4 | nnrpd 12417 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈
ℝ+) |
70 | | 0le2 11727 |
. . . . . . . 8
⊢ 0 ≤
2 |
71 | 70 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 0 ≤
2) |
72 | 4 | nnred 11640 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈ ℝ) |
73 | | prmuz2 16030 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
74 | 2, 73 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ∈
(ℤ≥‘2)) |
75 | | eluzle 12244 |
. . . . . . . . 9
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) |
76 | 74, 75 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 ≤ 𝑃) |
77 | | eldifsni 4683 |
. . . . . . . . 9
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ≠
2) |
78 | 77 | 3ad2ant2 1131 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 𝑃 ≠ 2) |
79 | 68, 72, 76, 78 | leneltd 10783 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 2 < 𝑃) |
80 | | modid 13259 |
. . . . . . 7
⊢ (((2
∈ ℝ ∧ 𝑃
∈ ℝ+) ∧ (0 ≤ 2 ∧ 2 < 𝑃)) → (2 mod 𝑃) = 2) |
81 | 68, 69, 71, 79, 80 | syl22anc 837 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (2 mod 𝑃) = 2) |
82 | 81 | eqeq2d 2809 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = (2 mod 𝑃) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
83 | | df-2 11688 |
. . . . . . . 8
⊢ 2 = (1 +
1) |
84 | 83 | oveq2i 7146 |
. . . . . . 7
⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 +
1)) |
85 | 50 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → 1 ∈
ℂ) |
86 | 49, 85, 85 | pnpcan2d 11024 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − (1 + 1)) =
((𝐴↑((𝑃 − 1) / 2)) −
1)) |
87 | 84, 86 | syl5eq 2845 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) = ((𝐴↑((𝑃 − 1) / 2)) −
1)) |
88 | 87 | breq2d 5042 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ (((𝐴↑((𝑃 − 1) / 2)) + 1) − 2) ↔
𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) −
1))) |
89 | 66, 82, 88 | 3bitr3rd 313 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1) ↔ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
90 | 62, 89 | orbi12d 916 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) + 1) ∨ 𝑃 ∥ ((𝐴↑((𝑃 − 1) / 2)) − 1)) ↔
((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2))) |
91 | 60, 90 | mpbid 235 |
. 2
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
92 | | ovex 7168 |
. . 3
⊢ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ V |
93 | 92 | elpr 4548 |
. 2
⊢ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2} ↔ ((((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 0 ∨ (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) = 2)) |
94 | 91, 93 | sylibr 237 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})
∧ ¬ 𝑃 ∥ 𝐴) → (((𝐴↑((𝑃 − 1) / 2)) + 1) mod 𝑃) ∈ {0, 2}) |