Step | Hyp | Ref
| Expression |
1 | | lgsqr.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | 1 | eldifad 3809 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) |
3 | | lgsqr.y |
. . . . . . . . . . . . 13
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
4 | 3 | znfld 20267 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) |
5 | 2, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Field) |
6 | | fldidom 19665 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ IDomn) |
8 | | isidom 19664 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn)) |
9 | 8 | simplbi 493 |
. . . . . . . . . 10
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ CRing) |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ CRing) |
11 | | crngring 18911 |
. . . . . . . . 9
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ Ring) |
13 | | lgsqr.l |
. . . . . . . . 9
⊢ 𝐿 = (ℤRHom‘𝑌) |
14 | 13 | zrhrhm 20219 |
. . . . . . . 8
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
𝑌)) |
16 | | zringbas 20183 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
17 | | eqid 2824 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
18 | 16, 17 | rhmf 19081 |
. . . . . . 7
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
19 | 15, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
20 | 19 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) |
21 | | elfzelz 12634 |
. . . . . . 7
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ) |
22 | 21 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℤ) |
23 | | zsqcl 13227 |
. . . . . 6
⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈
ℤ) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑2) ∈
ℤ) |
25 | 20, 24 | ffvelrnd 6608 |
. . . 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 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖
{2})) |
36 | | elfznn 12662 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ) |
37 | 36 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℕ) |
38 | 37 | nncnd 11367 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℂ) |
39 | | oddprm 15885 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
40 | 1, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
41 | 40 | nnnn0d 11677 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
42 | 41 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈
ℕ0) |
43 | | 2nn0 11636 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℕ0) |
45 | 38, 42, 44 | expmuld 13304 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = ((𝑦↑2)↑((𝑃 − 1) /
2))) |
46 | | prmnn 15759 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
47 | 2, 46 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℕ) |
48 | 47 | nnred 11366 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℝ) |
49 | | peano2rem 10668 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
51 | 50 | recnd 10384 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
52 | | 2cnd 11428 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) |
53 | | 2ne0 11461 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
54 | 53 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 0) |
55 | 51, 52, 54 | divcan2d 11128 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
56 | | phiprm 15852 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
57 | 2, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1)) |
58 | 55, 57 | eqtr4d 2863 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) =
(ϕ‘𝑃)) |
59 | 58 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (2 ·
((𝑃 − 1) / 2)) =
(ϕ‘𝑃)) |
60 | 59 | oveq2d 6920 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = (𝑦↑(ϕ‘𝑃))) |
61 | 45, 60 | eqtr3d 2862 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑2)↑((𝑃 − 1) / 2)) = (𝑦↑(ϕ‘𝑃))) |
62 | 61 | oveq1d 6919 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (((𝑦↑2)↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑦↑(ϕ‘𝑃)) mod 𝑃)) |
63 | 2 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ) |
64 | 63, 46 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
65 | 47 | nnzd 11808 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) |
66 | 65 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ) |
67 | | gcdcom 15607 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦)) |
68 | 22, 66, 67 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦)) |
69 | 37 | nnred 11366 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℝ) |
70 | 50 | rehalfcld 11604 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℝ) |
71 | 70 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈
ℝ) |
72 | 48 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ) |
73 | | elfzle2 12637 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2)) |
74 | 73 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ≤ ((𝑃 − 1) / 2)) |
75 | | prmuz2 15779 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
76 | 2, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
77 | | uz2m1nn 12045 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 1) ∈ ℕ) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 − 1) ∈ ℕ) |
79 | 78 | nnrpd 12153 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 1) ∈
ℝ+) |
80 | | rphalflt 12142 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 − 1) ∈
ℝ+ → ((𝑃 − 1) / 2) < (𝑃 − 1)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑃 − 1) / 2) < (𝑃 − 1)) |
82 | 48 | ltm1d 11285 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 1) < 𝑃) |
83 | 70, 50, 48, 81, 82 | lttrd 10516 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 1) / 2) < 𝑃) |
84 | 83 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) < 𝑃) |
85 | 69, 71, 72, 74, 84 | lelttrd 10513 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 < 𝑃) |
86 | 69, 72 | ltnled 10502 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑦)) |
87 | 85, 86 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ≤ 𝑦) |
88 | | dvdsle 15408 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦)) |
89 | 66, 37, 88 | syl2anc 581 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦)) |
90 | 87, 89 | mtod 190 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ 𝑦) |
91 | | coprm 15793 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ) → (¬
𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1)) |
92 | 63, 22, 91 | syl2anc 581 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1)) |
93 | 90, 92 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑦) = 1) |
94 | 68, 93 | eqtrd 2860 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = 1) |
95 | | eulerth 15858 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ (𝑦 gcd 𝑃) = 1) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
96 | 64, 22, 94, 95 | syl3anc 1496 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
97 | 62, 96 | eqtrd 2860 |
. . . . 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 25483 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)) |
99 | | eqid 2824 |
. . . . . . . 8
⊢ (𝑌 ↑s
(Base‘𝑌)) = (𝑌 ↑s
(Base‘𝑌)) |
100 | | eqid 2824 |
. . . . . . . 8
⊢
(Base‘(𝑌
↑s (Base‘𝑌))) = (Base‘(𝑌 ↑s (Base‘𝑌))) |
101 | | fvexd 6447 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑌) ∈ V) |
102 | 29, 26, 99, 17 | evl1rhm 20055 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ CRing → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌)))) |
103 | 10, 102 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌)))) |
104 | 27, 100 | rhmf 19081 |
. . . . . . . . . 10
⊢ (𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌))) → 𝑂:𝐵⟶(Base‘(𝑌 ↑s (Base‘𝑌)))) |
105 | 103, 104 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑌 ↑s (Base‘𝑌)))) |
106 | 26 | ply1ring 19977 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑆 ∈ Ring) |
107 | 12, 106 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Ring) |
108 | | ringgrp 18905 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ Grp) |
110 | | eqid 2824 |
. . . . . . . . . . . . . 14
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
111 | 110 | ringmgp 18906 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
112 | 107, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
113 | 31, 26, 27 | vr1cl 19946 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑋 ∈ 𝐵) |
114 | 12, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
115 | 110, 27 | mgpbas 18848 |
. . . . . . . . . . . . 13
⊢ 𝐵 =
(Base‘(mulGrp‘𝑆)) |
116 | 115, 30 | mulgnn0cl 17910 |
. . . . . . . . . . . 12
⊢
(((mulGrp‘𝑆)
∈ Mnd ∧ ((𝑃
− 1) / 2) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵) |
117 | 112, 41, 114, 116 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵) |
118 | 27, 33 | ringidcl 18921 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 1 ∈ 𝐵) |
119 | 107, 118 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈ 𝐵) |
120 | 27, 32 | grpsubcl 17848 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Grp ∧ (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
121 | 109, 117,
119, 120 | syl3anc 1496 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
122 | 34, 121 | syl5eqel 2909 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ 𝐵) |
123 | 105, 122 | ffvelrnd 6608 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘𝑇) ∈ (Base‘(𝑌 ↑s (Base‘𝑌)))) |
124 | 99, 17, 100, 5, 101, 123 | pwselbas 16501 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘𝑇):(Base‘𝑌)⟶(Base‘𝑌)) |
125 | 124 | ffnd 6278 |
. . . . . 6
⊢ (𝜑 → (𝑂‘𝑇) Fn (Base‘𝑌)) |
126 | 125 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑂‘𝑇) Fn (Base‘𝑌)) |
127 | | fniniseg 6586 |
. . . . 5
⊢ ((𝑂‘𝑇) Fn (Base‘𝑌) → ((𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ ((𝐿‘(𝑦↑2)) ∈ (Base‘𝑌) ∧ ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)))) |
128 | 126, 127 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ ((𝐿‘(𝑦↑2)) ∈ (Base‘𝑌) ∧ ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)))) |
129 | 25, 98, 128 | mpbir2and 706 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
130 | | lgsqr.g |
. . 3
⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2))) |
131 | 129, 130 | fmptd 6632 |
. 2
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))⟶(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
132 | | fvoveq1 6927 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑥↑2))) |
133 | | fvex 6445 |
. . . . . . . 8
⊢ (𝐿‘(𝑥↑2)) ∈ V |
134 | 132, 130,
133 | fvmpt 6528 |
. . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2))) |
135 | 134 | ad2antrl 721 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2))) |
136 | | fvoveq1 6927 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑧↑2))) |
137 | | fvex 6445 |
. . . . . . . 8
⊢ (𝐿‘(𝑧↑2)) ∈ V |
138 | 136, 130,
137 | fvmpt 6528 |
. . . . . . 7
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2))) |
139 | 138 | ad2antll 722 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2))) |
140 | 135, 139 | eqeq12d 2839 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ (𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)))) |
141 | 47 | nnnn0d 11677 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
142 | 141 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈
ℕ0) |
143 | | elfzelz 12634 |
. . . . . . . 8
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ) |
144 | 143 | ad2antrl 721 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℤ) |
145 | | zsqcl 13227 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈
ℤ) |
146 | 144, 145 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥↑2) ∈
ℤ) |
147 | | elfzelz 12634 |
. . . . . . . 8
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℤ) |
148 | 147 | ad2antll 722 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℤ) |
149 | | zsqcl 13227 |
. . . . . . 7
⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈
ℤ) |
150 | 148, 149 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧↑2) ∈
ℤ) |
151 | 3, 13 | zndvds 20256 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ0
∧ (𝑥↑2) ∈
ℤ ∧ (𝑧↑2)
∈ ℤ) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2)))) |
152 | 142, 146,
150, 151 | syl3anc 1496 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2)))) |
153 | | elfznn 12662 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
154 | 153 | ad2antrl 721 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℕ) |
155 | 154 | nncnd 11367 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℂ) |
156 | | elfznn 12662 |
. . . . . . . . 9
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℕ) |
157 | 156 | ad2antll 722 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℕ) |
158 | 157 | nncnd 11367 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℂ) |
159 | | subsq 13265 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧))) |
160 | 155, 158,
159 | syl2anc 581 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧))) |
161 | 160 | breq2d 4884 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥↑2) − (𝑧↑2)) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)))) |
162 | 140, 152,
161 | 3bitrd 297 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)))) |
163 | 2 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ) |
164 | 144, 148 | zaddcld 11813 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℤ) |
165 | 144, 148 | zsubcld 11814 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 − 𝑧) ∈ ℤ) |
166 | | euclemma 15795 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 + 𝑧) ∈ ℤ ∧ (𝑥 − 𝑧) ∈ ℤ) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)))) |
167 | 163, 164,
165, 166 | syl3anc 1496 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)))) |
168 | 163, 46 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ) |
169 | 168 | nnzd 11808 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ) |
170 | 154, 157 | nnaddcld 11402 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℕ) |
171 | | dvdsle 15408 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ (𝑥 + 𝑧) ∈ ℕ) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧))) |
172 | 169, 170,
171 | syl2anc 581 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧))) |
173 | 170 | nnred 11366 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℝ) |
174 | 168 | nnred 11366 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ) |
175 | 174, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈
ℝ) |
176 | 154 | nnred 11366 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℝ) |
177 | 157 | nnred 11366 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℝ) |
178 | 70 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈
ℝ) |
179 | | elfzle2 12637 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
180 | 179 | ad2antrl 721 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
181 | | elfzle2 12637 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ≤ ((𝑃 − 1) / 2)) |
182 | 181 | ad2antll 722 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ≤ ((𝑃 − 1) / 2)) |
183 | 176, 177,
178, 178, 180, 182 | le2addd 10970 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))) |
184 | 51 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈
ℂ) |
185 | 184 | 2halvesd 11603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
186 | 183, 185 | breqtrd 4898 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (𝑃 − 1)) |
187 | 174 | ltm1d 11285 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) < 𝑃) |
188 | 173, 175,
174, 186, 187 | lelttrd 10513 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) < 𝑃) |
189 | 173, 174 | ltnled 10502 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 + 𝑧) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑥 + 𝑧))) |
190 | 188, 189 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ≤ (𝑥 + 𝑧)) |
191 | 190 | pm2.21d 119 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ≤ (𝑥 + 𝑧) → 𝑥 = 𝑧)) |
192 | 172, 191 | syld 47 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑥 = 𝑧)) |
193 | | moddvds 15367 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧))) |
194 | 168, 144,
148, 193 | syl3anc 1496 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧))) |
195 | 168 | nnrpd 12153 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈
ℝ+) |
196 | 154 | nnnn0d 11677 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℕ0) |
197 | 196 | nn0ge0d 11680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑥) |
198 | 83 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) < 𝑃) |
199 | 176, 178,
174, 180, 198 | lelttrd 10513 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 < 𝑃) |
200 | | modid 12989 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑃)) → (𝑥 mod 𝑃) = 𝑥) |
201 | 176, 195,
197, 199, 200 | syl22anc 874 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 mod 𝑃) = 𝑥) |
202 | 157 | nnnn0d 11677 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℕ0) |
203 | 202 | nn0ge0d 11680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑧) |
204 | 177, 178,
174, 182, 198 | lelttrd 10513 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 < 𝑃) |
205 | | modid 12989 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑧 ∧ 𝑧 < 𝑃)) → (𝑧 mod 𝑃) = 𝑧) |
206 | 177, 195,
203, 204, 205 | syl22anc 874 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧 mod 𝑃) = 𝑧) |
207 | 201, 206 | eqeq12d 2839 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑥 = 𝑧)) |
208 | 194, 207 | bitr3d 273 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) ↔ 𝑥 = 𝑧)) |
209 | 208 | biimpd 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) → 𝑥 = 𝑧)) |
210 | 192, 209 | jaod 892 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)) → 𝑥 = 𝑧)) |
211 | 167, 210 | sylbid 232 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) → 𝑥 = 𝑧)) |
212 | 162, 211 | sylbid 232 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)) |
213 | 212 | ralrimivva 3179 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)) |
214 | | dff13 6766 |
. 2
⊢ (𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ (𝐺:(1...((𝑃 − 1) / 2))⟶(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∧ ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧))) |
215 | 131, 213,
214 | sylanbrc 580 |
1
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |