Step | Hyp | Ref
| Expression |
1 | | lgsqr.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
2 | 1 | eldifad 3922 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) |
3 | | lgsqr.y |
. . . . . . . . . . . . 13
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
4 | 3 | znfld 20967 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) |
5 | 2, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Field) |
6 | | fldidom 20775 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ IDomn) |
8 | | isidom 20774 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn)) |
9 | 8 | simplbi 498 |
. . . . . . . . . 10
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ CRing) |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ CRing) |
11 | | crngring 19976 |
. . . . . . . . 9
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ Ring) |
13 | | lgsqr.l |
. . . . . . . . 9
⊢ 𝐿 = (ℤRHom‘𝑌) |
14 | 13 | zrhrhm 20912 |
. . . . . . . 8
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
𝑌)) |
16 | | zringbas 20875 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
17 | | eqid 2736 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
18 | 16, 17 | rhmf 20158 |
. . . . . . 7
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
19 | 15, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
20 | 19 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) |
21 | | elfzelz 13441 |
. . . . . . 7
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ) |
22 | 21 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℤ) |
23 | | zsqcl 14034 |
. . . . . 6
⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈
ℤ) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑2) ∈
ℤ) |
25 | 20, 24 | ffvelcdmd 7036 |
. . . 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 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖
{2})) |
36 | | elfznn 13470 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ) |
37 | 36 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℕ) |
38 | 37 | nncnd 12169 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℂ) |
39 | | oddprm 16682 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
40 | 1, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
41 | 40 | nnnn0d 12473 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
42 | 41 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈
ℕ0) |
43 | | 2nn0 12430 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℕ0) |
45 | 38, 42, 44 | expmuld 14054 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = ((𝑦↑2)↑((𝑃 − 1) /
2))) |
46 | | prmnn 16550 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
47 | 2, 46 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℕ) |
48 | 47 | nnred 12168 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℝ) |
49 | | peano2rem 11468 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
51 | 50 | recnd 11183 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
52 | | 2cnd 12231 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) |
53 | | 2ne0 12257 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
54 | 53 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 0) |
55 | 51, 52, 54 | divcan2d 11933 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
56 | | phiprm 16649 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
57 | 2, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1)) |
58 | 55, 57 | eqtr4d 2779 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) =
(ϕ‘𝑃)) |
59 | 58 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (2 ·
((𝑃 − 1) / 2)) =
(ϕ‘𝑃)) |
60 | 59 | oveq2d 7373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = (𝑦↑(ϕ‘𝑃))) |
61 | 45, 60 | eqtr3d 2778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑2)↑((𝑃 − 1) / 2)) = (𝑦↑(ϕ‘𝑃))) |
62 | 61 | oveq1d 7372 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (((𝑦↑2)↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑦↑(ϕ‘𝑃)) mod 𝑃)) |
63 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ) |
64 | 63, 46 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ) |
65 | 47 | nnzd 12526 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) |
66 | 65 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ) |
67 | 22, 66 | gcdcomd 16394 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦)) |
68 | 37 | nnred 12168 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℝ) |
69 | 50 | rehalfcld 12400 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℝ) |
70 | 69 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈
ℝ) |
71 | 48 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ) |
72 | | elfzle2 13445 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2)) |
73 | 72 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ≤ ((𝑃 − 1) / 2)) |
74 | | prmuz2 16572 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
75 | 2, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
76 | | uz2m1nn 12848 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 1) ∈ ℕ) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 − 1) ∈ ℕ) |
78 | 77 | nnrpd 12955 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 1) ∈
ℝ+) |
79 | | rphalflt 12944 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 − 1) ∈
ℝ+ → ((𝑃 − 1) / 2) < (𝑃 − 1)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑃 − 1) / 2) < (𝑃 − 1)) |
81 | 48 | ltm1d 12087 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 1) < 𝑃) |
82 | 69, 50, 48, 80, 81 | lttrd 11316 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 1) / 2) < 𝑃) |
83 | 82 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) < 𝑃) |
84 | 68, 70, 71, 73, 83 | lelttrd 11313 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 < 𝑃) |
85 | 68, 71 | ltnled 11302 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑦)) |
86 | 84, 85 | mpbid 231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ≤ 𝑦) |
87 | | dvdsle 16192 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦)) |
88 | 66, 37, 87 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦)) |
89 | 86, 88 | mtod 197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ 𝑦) |
90 | | coprm 16587 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ) → (¬
𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1)) |
91 | 63, 22, 90 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1)) |
92 | 89, 91 | mpbid 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑦) = 1) |
93 | 67, 92 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = 1) |
94 | | eulerth 16655 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ (𝑦 gcd 𝑃) = 1) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
95 | 64, 22, 93, 94 | syl3anc 1371 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
96 | 62, 95 | eqtrd 2776 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (((𝑦↑2)↑((𝑃 − 1) / 2)) mod 𝑃) = (1 mod 𝑃)) |
97 | 3, 26, 27, 28, 29, 30, 31, 32, 33, 34, 13, 35, 24, 96 | lgsqrlem1 26694 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)) |
98 | | eqid 2736 |
. . . . . . . 8
⊢ (𝑌 ↑s
(Base‘𝑌)) = (𝑌 ↑s
(Base‘𝑌)) |
99 | | eqid 2736 |
. . . . . . . 8
⊢
(Base‘(𝑌
↑s (Base‘𝑌))) = (Base‘(𝑌 ↑s (Base‘𝑌))) |
100 | | fvexd 6857 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑌) ∈ V) |
101 | 29, 26, 98, 17 | evl1rhm 21698 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ CRing → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌)))) |
102 | 10, 101 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌)))) |
103 | 27, 99 | rhmf 20158 |
. . . . . . . . . 10
⊢ (𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌))) → 𝑂:𝐵⟶(Base‘(𝑌 ↑s (Base‘𝑌)))) |
104 | 102, 103 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑌 ↑s (Base‘𝑌)))) |
105 | 26 | ply1ring 21619 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑆 ∈ Ring) |
106 | 12, 105 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Ring) |
107 | | ringgrp 19969 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ Grp) |
109 | | eqid 2736 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
110 | 109, 27 | mgpbas 19902 |
. . . . . . . . . . . 12
⊢ 𝐵 =
(Base‘(mulGrp‘𝑆)) |
111 | 109 | ringmgp 19970 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
112 | 106, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
113 | 31, 26, 27 | vr1cl 21588 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑋 ∈ 𝐵) |
114 | 12, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
115 | 110, 30, 112, 41, 114 | mulgnn0cld 18897 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵) |
116 | 27, 33 | ringidcl 19989 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 1 ∈ 𝐵) |
117 | 106, 116 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈ 𝐵) |
118 | 27, 32 | grpsubcl 18827 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Grp ∧ (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
119 | 108, 115,
117, 118 | syl3anc 1371 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
120 | 34, 119 | eqeltrid 2842 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ 𝐵) |
121 | 104, 120 | ffvelcdmd 7036 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘𝑇) ∈ (Base‘(𝑌 ↑s (Base‘𝑌)))) |
122 | 98, 17, 99, 5, 100, 121 | pwselbas 17371 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘𝑇):(Base‘𝑌)⟶(Base‘𝑌)) |
123 | 122 | ffnd 6669 |
. . . . . 6
⊢ (𝜑 → (𝑂‘𝑇) Fn (Base‘𝑌)) |
124 | 123 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑂‘𝑇) Fn (Base‘𝑌)) |
125 | | fniniseg 7010 |
. . . . 5
⊢ ((𝑂‘𝑇) Fn (Base‘𝑌) → ((𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ ((𝐿‘(𝑦↑2)) ∈ (Base‘𝑌) ∧ ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)))) |
126 | 124, 125 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ ((𝐿‘(𝑦↑2)) ∈ (Base‘𝑌) ∧ ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)))) |
127 | 25, 97, 126 | mpbir2and 711 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
128 | | lgsqr.g |
. . 3
⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2))) |
129 | 127, 128 | fmptd 7062 |
. 2
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))⟶(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
130 | | fvoveq1 7380 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑥↑2))) |
131 | | fvex 6855 |
. . . . . . . 8
⊢ (𝐿‘(𝑥↑2)) ∈ V |
132 | 130, 128,
131 | fvmpt 6948 |
. . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2))) |
133 | 132 | ad2antrl 726 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2))) |
134 | | fvoveq1 7380 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑧↑2))) |
135 | | fvex 6855 |
. . . . . . . 8
⊢ (𝐿‘(𝑧↑2)) ∈ V |
136 | 134, 128,
135 | fvmpt 6948 |
. . . . . . 7
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2))) |
137 | 136 | ad2antll 727 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2))) |
138 | 133, 137 | eqeq12d 2752 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ (𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)))) |
139 | 47 | nnnn0d 12473 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
140 | 139 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈
ℕ0) |
141 | | elfzelz 13441 |
. . . . . . . 8
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ) |
142 | 141 | ad2antrl 726 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℤ) |
143 | | zsqcl 14034 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈
ℤ) |
144 | 142, 143 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥↑2) ∈
ℤ) |
145 | | elfzelz 13441 |
. . . . . . . 8
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℤ) |
146 | 145 | ad2antll 727 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℤ) |
147 | | zsqcl 14034 |
. . . . . . 7
⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈
ℤ) |
148 | 146, 147 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧↑2) ∈
ℤ) |
149 | 3, 13 | zndvds 20956 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ0
∧ (𝑥↑2) ∈
ℤ ∧ (𝑧↑2)
∈ ℤ) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2)))) |
150 | 140, 144,
148, 149 | syl3anc 1371 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2)))) |
151 | | elfznn 13470 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
152 | 151 | ad2antrl 726 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℕ) |
153 | 152 | nncnd 12169 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℂ) |
154 | | elfznn 13470 |
. . . . . . . . 9
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℕ) |
155 | 154 | ad2antll 727 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℕ) |
156 | 155 | nncnd 12169 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℂ) |
157 | | subsq 14114 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧))) |
158 | 153, 156,
157 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧))) |
159 | 158 | breq2d 5117 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥↑2) − (𝑧↑2)) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)))) |
160 | 138, 150,
159 | 3bitrd 304 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)))) |
161 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ) |
162 | 142, 146 | zaddcld 12611 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℤ) |
163 | 142, 146 | zsubcld 12612 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 − 𝑧) ∈ ℤ) |
164 | | euclemma 16589 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 + 𝑧) ∈ ℤ ∧ (𝑥 − 𝑧) ∈ ℤ) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)))) |
165 | 161, 162,
163, 164 | syl3anc 1371 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)))) |
166 | 161, 46 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ) |
167 | 166 | nnzd 12526 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ) |
168 | 152, 155 | nnaddcld 12205 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℕ) |
169 | | dvdsle 16192 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ (𝑥 + 𝑧) ∈ ℕ) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧))) |
170 | 167, 168,
169 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧))) |
171 | 168 | nnred 12168 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℝ) |
172 | 166 | nnred 12168 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ) |
173 | 172, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈
ℝ) |
174 | 152 | nnred 12168 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℝ) |
175 | 155 | nnred 12168 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℝ) |
176 | 69 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈
ℝ) |
177 | | elfzle2 13445 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
178 | 177 | ad2antrl 726 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
179 | | elfzle2 13445 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ≤ ((𝑃 − 1) / 2)) |
180 | 179 | ad2antll 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ≤ ((𝑃 − 1) / 2)) |
181 | 174, 175,
176, 176, 178, 180 | le2addd 11774 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))) |
182 | 51 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈
ℂ) |
183 | 182 | 2halvesd 12399 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
184 | 181, 183 | breqtrd 5131 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (𝑃 − 1)) |
185 | 172 | ltm1d 12087 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) < 𝑃) |
186 | 171, 173,
172, 184, 185 | lelttrd 11313 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) < 𝑃) |
187 | 171, 172 | ltnled 11302 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 + 𝑧) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑥 + 𝑧))) |
188 | 186, 187 | mpbid 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ≤ (𝑥 + 𝑧)) |
189 | 188 | pm2.21d 121 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ≤ (𝑥 + 𝑧) → 𝑥 = 𝑧)) |
190 | 170, 189 | syld 47 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑥 = 𝑧)) |
191 | | moddvds 16147 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧))) |
192 | 166, 142,
146, 191 | syl3anc 1371 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧))) |
193 | 166 | nnrpd 12955 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈
ℝ+) |
194 | 152 | nnnn0d 12473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℕ0) |
195 | 194 | nn0ge0d 12476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑥) |
196 | 82 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) < 𝑃) |
197 | 174, 176,
172, 178, 196 | lelttrd 11313 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 < 𝑃) |
198 | | modid 13801 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑃)) → (𝑥 mod 𝑃) = 𝑥) |
199 | 174, 193,
195, 197, 198 | syl22anc 837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 mod 𝑃) = 𝑥) |
200 | 155 | nnnn0d 12473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℕ0) |
201 | 200 | nn0ge0d 12476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑧) |
202 | 175, 176,
172, 180, 196 | lelttrd 11313 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 < 𝑃) |
203 | | modid 13801 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑧 ∧ 𝑧 < 𝑃)) → (𝑧 mod 𝑃) = 𝑧) |
204 | 175, 193,
201, 202, 203 | syl22anc 837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧 mod 𝑃) = 𝑧) |
205 | 199, 204 | eqeq12d 2752 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑥 = 𝑧)) |
206 | 192, 205 | bitr3d 280 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) ↔ 𝑥 = 𝑧)) |
207 | 206 | biimpd 228 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) → 𝑥 = 𝑧)) |
208 | 190, 207 | jaod 857 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)) → 𝑥 = 𝑧)) |
209 | 165, 208 | sylbid 239 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) → 𝑥 = 𝑧)) |
210 | 160, 209 | sylbid 239 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)) |
211 | 210 | ralrimivva 3197 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)) |
212 | | dff13 7202 |
. 2
⊢ (𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ (𝐺:(1...((𝑃 − 1) / 2))⟶(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∧ ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧))) |
213 | 129, 211,
212 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |