Step | Hyp | Ref
| Expression |
1 | | lgsqr.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | 1 | eldifad 3552 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) |
3 | | lgsqr.y |
. . . . . . . . . . . . 13
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
4 | 3 | znfld 19728 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) |
5 | 2, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Field) |
6 | | fldidom 19126 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ IDomn) |
8 | | isidom 19125 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn)) |
9 | 8 | simplbi 475 |
. . . . . . . . . 10
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ CRing) |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ CRing) |
11 | | crngring 18381 |
. . . . . . . . 9
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ Ring) |
13 | | lgsqr.l |
. . . . . . . . 9
⊢ 𝐿 = (ℤRHom‘𝑌) |
14 | 13 | zrhrhm 19679 |
. . . . . . . 8
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
𝑌)) |
16 | | zringbas 19643 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
17 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
18 | 16, 17 | rhmf 18549 |
. . . . . . 7
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
19 | 15, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) |
21 | | elfzelz 12213 |
. . . . . . 7
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ) |
22 | 21 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℤ) |
23 | | zsqcl 12796 |
. . . . . 6
⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈
ℤ) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑2) ∈
ℤ) |
25 | 20, 24 | ffvelrnd 6268 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(𝑦↑2)) ∈ (Base‘𝑌)) |
26 | | lgsqr.s |
. . . . 5
⊢ 𝑆 = (Poly1‘𝑌) |
27 | | lgsqr.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑆) |
28 | | lgsqr.d |
. . . . 5
⊢ 𝐷 = ( deg1
‘𝑌) |
29 | | lgsqr.o |
. . . . 5
⊢ 𝑂 = (eval1‘𝑌) |
30 | | lgsqr.e |
. . . . 5
⊢ ↑ =
(.g‘(mulGrp‘𝑆)) |
31 | | lgsqr.x |
. . . . 5
⊢ 𝑋 = (var1‘𝑌) |
32 | | lgsqr.m |
. . . . 5
⊢ − =
(-g‘𝑆) |
33 | | lgsqr.u |
. . . . 5
⊢ 1 =
(1r‘𝑆) |
34 | | lgsqr.t |
. . . . 5
⊢ 𝑇 = ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) |
35 | 1 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖
{2})) |
36 | | elfznn 12241 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ) |
37 | 36 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℕ) |
38 | 37 | nncnd 10913 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℂ) |
39 | | oddprm 15353 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
40 | 1, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
41 | 40 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈
ℕ0) |
43 | | 2nn0 11186 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℕ0) |
45 | 38, 42, 44 | expmuld 12873 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = ((𝑦↑2)↑((𝑃 − 1) /
2))) |
46 | | prmnn 15226 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
47 | 2, 46 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℕ) |
48 | 47 | nnred 10912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℝ) |
49 | | peano2rem 10227 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
51 | 50 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
52 | | 2cnd 10970 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) |
53 | | 2ne0 10990 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
54 | 53 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 0) |
55 | 51, 52, 54 | divcan2d 10682 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
56 | | phiprm 15320 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
57 | 2, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1)) |
58 | 55, 57 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) =
(ϕ‘𝑃)) |
59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (2 ·
((𝑃 − 1) / 2)) =
(ϕ‘𝑃)) |
60 | 59 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = (𝑦↑(ϕ‘𝑃))) |
61 | 45, 60 | eqtr3d 2646 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑2)↑((𝑃 − 1) / 2)) = (𝑦↑(ϕ‘𝑃))) |
62 | 61 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (((𝑦↑2)↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑦↑(ϕ‘𝑃)) mod 𝑃)) |
63 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ) |
64 | 63, 46 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
65 | 47 | nnzd 11357 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) |
66 | 65 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ) |
67 | | gcdcom 15073 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦)) |
68 | 22, 66, 67 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦)) |
69 | 37 | nnred 10912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℝ) |
70 | 50 | rehalfcld 11156 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℝ) |
71 | 70 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈
ℝ) |
72 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ) |
73 | | elfzle2 12216 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2)) |
74 | 73 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ≤ ((𝑃 − 1) / 2)) |
75 | | prmuz2 15246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
76 | 2, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
77 | | uz2m1nn 11639 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 1) ∈ ℕ) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 − 1) ∈ ℕ) |
79 | 78 | nnrpd 11746 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 1) ∈
ℝ+) |
80 | | rphalflt 11736 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 − 1) ∈
ℝ+ → ((𝑃 − 1) / 2) < (𝑃 − 1)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑃 − 1) / 2) < (𝑃 − 1)) |
82 | 48 | ltm1d 10835 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 1) < 𝑃) |
83 | 70, 50, 48, 81, 82 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 1) / 2) < 𝑃) |
84 | 83 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) < 𝑃) |
85 | 69, 71, 72, 74, 84 | lelttrd 10074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 < 𝑃) |
86 | 69, 72 | ltnled 10063 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑦)) |
87 | 85, 86 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ≤ 𝑦) |
88 | | dvdsle 14870 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦)) |
89 | 66, 37, 88 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦)) |
90 | 87, 89 | mtod 188 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ 𝑦) |
91 | | coprm 15261 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ) → (¬
𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1)) |
92 | 63, 22, 91 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1)) |
93 | 90, 92 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑦) = 1) |
94 | 68, 93 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = 1) |
95 | | eulerth 15326 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ (𝑦 gcd 𝑃) = 1) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
96 | 64, 22, 94, 95 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
97 | 62, 96 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (((𝑦↑2)↑((𝑃 − 1) / 2)) mod 𝑃) = (1 mod 𝑃)) |
98 | 3, 26, 27, 28, 29, 30, 31, 32, 33, 34, 13, 35, 24, 97 | lgsqrlem1 24871 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)) |
99 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑌 ↑s
(Base‘𝑌)) = (𝑌 ↑s
(Base‘𝑌)) |
100 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(𝑌
↑s (Base‘𝑌))) = (Base‘(𝑌 ↑s (Base‘𝑌))) |
101 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑌)
∈ V |
102 | 101 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑌) ∈ V) |
103 | 29, 26, 99, 17 | evl1rhm 19517 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ CRing → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌)))) |
104 | 10, 103 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌)))) |
105 | 27, 100 | rhmf 18549 |
. . . . . . . . . 10
⊢ (𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌))) → 𝑂:𝐵⟶(Base‘(𝑌 ↑s (Base‘𝑌)))) |
106 | 104, 105 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑌 ↑s (Base‘𝑌)))) |
107 | 26 | ply1ring 19439 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑆 ∈ Ring) |
108 | 12, 107 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Ring) |
109 | | ringgrp 18375 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ Grp) |
111 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
112 | 111 | ringmgp 18376 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
113 | 108, 112 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
114 | 31, 26, 27 | vr1cl 19408 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑋 ∈ 𝐵) |
115 | 12, 114 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
116 | 111, 27 | mgpbas 18318 |
. . . . . . . . . . . . 13
⊢ 𝐵 =
(Base‘(mulGrp‘𝑆)) |
117 | 116, 30 | mulgnn0cl 17381 |
. . . . . . . . . . . 12
⊢
(((mulGrp‘𝑆)
∈ Mnd ∧ ((𝑃
− 1) / 2) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵) |
118 | 113, 41, 115, 117 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵) |
119 | 27, 33 | ringidcl 18391 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 1 ∈ 𝐵) |
120 | 108, 119 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈ 𝐵) |
121 | 27, 32 | grpsubcl 17318 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Grp ∧ (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
122 | 110, 118,
120, 121 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
123 | 34, 122 | syl5eqel 2692 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ 𝐵) |
124 | 106, 123 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘𝑇) ∈ (Base‘(𝑌 ↑s (Base‘𝑌)))) |
125 | 99, 17, 100, 5, 102, 124 | pwselbas 15972 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘𝑇):(Base‘𝑌)⟶(Base‘𝑌)) |
126 | | ffn 5958 |
. . . . . . 7
⊢ ((𝑂‘𝑇):(Base‘𝑌)⟶(Base‘𝑌) → (𝑂‘𝑇) Fn (Base‘𝑌)) |
127 | 125, 126 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑂‘𝑇) Fn (Base‘𝑌)) |
128 | 127 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑂‘𝑇) Fn (Base‘𝑌)) |
129 | | fniniseg 6246 |
. . . . 5
⊢ ((𝑂‘𝑇) Fn (Base‘𝑌) → ((𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ ((𝐿‘(𝑦↑2)) ∈ (Base‘𝑌) ∧ ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)))) |
130 | 128, 129 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ ((𝐿‘(𝑦↑2)) ∈ (Base‘𝑌) ∧ ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)))) |
131 | 25, 98, 130 | mpbir2and 959 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
132 | | lgsqr.g |
. . 3
⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2))) |
133 | 131, 132 | fmptd 6292 |
. 2
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))⟶(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
134 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦↑2) = (𝑥↑2)) |
135 | 134 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑥↑2))) |
136 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐿‘(𝑥↑2)) ∈ V |
137 | 135, 132,
136 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2))) |
138 | 137 | ad2antrl 760 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2))) |
139 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑦↑2) = (𝑧↑2)) |
140 | 139 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑧↑2))) |
141 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐿‘(𝑧↑2)) ∈ V |
142 | 140, 132,
141 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2))) |
143 | 142 | ad2antll 761 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2))) |
144 | 138, 143 | eqeq12d 2625 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ (𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)))) |
145 | 47 | nnnn0d 11228 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
146 | 145 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈
ℕ0) |
147 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ) |
148 | 147 | ad2antrl 760 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℤ) |
149 | | zsqcl 12796 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈
ℤ) |
150 | 148, 149 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥↑2) ∈
ℤ) |
151 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℤ) |
152 | 151 | ad2antll 761 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℤ) |
153 | | zsqcl 12796 |
. . . . . . 7
⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈
ℤ) |
154 | 152, 153 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧↑2) ∈
ℤ) |
155 | 3, 13 | zndvds 19717 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ0
∧ (𝑥↑2) ∈
ℤ ∧ (𝑧↑2)
∈ ℤ) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2)))) |
156 | 146, 150,
154, 155 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2)))) |
157 | | elfznn 12241 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
158 | 157 | ad2antrl 760 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℕ) |
159 | 158 | nncnd 10913 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℂ) |
160 | | elfznn 12241 |
. . . . . . . . 9
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℕ) |
161 | 160 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℕ) |
162 | 161 | nncnd 10913 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℂ) |
163 | | subsq 12834 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧))) |
164 | 159, 162,
163 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧))) |
165 | 164 | breq2d 4595 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥↑2) − (𝑧↑2)) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)))) |
166 | 144, 156,
165 | 3bitrd 293 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)))) |
167 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ) |
168 | 148, 152 | zaddcld 11362 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℤ) |
169 | 148, 152 | zsubcld 11363 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 − 𝑧) ∈ ℤ) |
170 | | euclemma 15263 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 + 𝑧) ∈ ℤ ∧ (𝑥 − 𝑧) ∈ ℤ) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)))) |
171 | 167, 168,
169, 170 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)))) |
172 | 167, 46 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ) |
173 | 172 | nnzd 11357 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ) |
174 | 158, 161 | nnaddcld 10944 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℕ) |
175 | | dvdsle 14870 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ (𝑥 + 𝑧) ∈ ℕ) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧))) |
176 | 173, 174,
175 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧))) |
177 | 174 | nnred 10912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℝ) |
178 | 172 | nnred 10912 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ) |
179 | 178, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈
ℝ) |
180 | 158 | nnred 10912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℝ) |
181 | 161 | nnred 10912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℝ) |
182 | 70 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈
ℝ) |
183 | | elfzle2 12216 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
184 | 183 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
185 | | elfzle2 12216 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ≤ ((𝑃 − 1) / 2)) |
186 | 185 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ≤ ((𝑃 − 1) / 2)) |
187 | 180, 181,
182, 182, 184, 186 | le2addd 10525 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))) |
188 | 51 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈
ℂ) |
189 | 188 | 2halvesd 11155 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
190 | 187, 189 | breqtrd 4609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (𝑃 − 1)) |
191 | 178 | ltm1d 10835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) < 𝑃) |
192 | 177, 179,
178, 190, 191 | lelttrd 10074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) < 𝑃) |
193 | 177, 178 | ltnled 10063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 + 𝑧) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑥 + 𝑧))) |
194 | 192, 193 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ≤ (𝑥 + 𝑧)) |
195 | 194 | pm2.21d 117 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ≤ (𝑥 + 𝑧) → 𝑥 = 𝑧)) |
196 | 176, 195 | syld 46 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑥 = 𝑧)) |
197 | | moddvds 14829 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧))) |
198 | 172, 148,
152, 197 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧))) |
199 | 172 | nnrpd 11746 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈
ℝ+) |
200 | 158 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℕ0) |
201 | 200 | nn0ge0d 11231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑥) |
202 | 83 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) < 𝑃) |
203 | 180, 182,
178, 184, 202 | lelttrd 10074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 < 𝑃) |
204 | | modid 12557 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑃)) → (𝑥 mod 𝑃) = 𝑥) |
205 | 180, 199,
201, 203, 204 | syl22anc 1319 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 mod 𝑃) = 𝑥) |
206 | 161 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℕ0) |
207 | 206 | nn0ge0d 11231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑧) |
208 | 181, 182,
178, 186, 202 | lelttrd 10074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 < 𝑃) |
209 | | modid 12557 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑧 ∧ 𝑧 < 𝑃)) → (𝑧 mod 𝑃) = 𝑧) |
210 | 181, 199,
207, 208, 209 | syl22anc 1319 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧 mod 𝑃) = 𝑧) |
211 | 205, 210 | eqeq12d 2625 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑥 = 𝑧)) |
212 | 198, 211 | bitr3d 269 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) ↔ 𝑥 = 𝑧)) |
213 | 212 | biimpd 218 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) → 𝑥 = 𝑧)) |
214 | 196, 213 | jaod 394 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)) → 𝑥 = 𝑧)) |
215 | 171, 214 | sylbid 229 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) → 𝑥 = 𝑧)) |
216 | 166, 215 | sylbid 229 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)) |
217 | 216 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)) |
218 | | dff13 6416 |
. 2
⊢ (𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ (𝐺:(1...((𝑃 − 1) / 2))⟶(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∧ ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧))) |
219 | 133, 217,
218 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |