| Step | Hyp | Ref
| Expression |
| 1 | | lgsqr.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
| 2 | 1 | eldifad 3963 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 3 | | lgsqr.y |
. . . . . . . . . . . . 13
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
| 4 | 3 | znfld 21579 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) |
| 5 | 2, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ Field) |
| 6 | | fldidom 20771 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ IDomn) |
| 8 | | isidom 20725 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn)) |
| 9 | 8 | simplbi 497 |
. . . . . . . . . 10
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ CRing) |
| 10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ CRing) |
| 11 | | crngring 20242 |
. . . . . . . . 9
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
| 12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ Ring) |
| 13 | | lgsqr.l |
. . . . . . . . 9
⊢ 𝐿 = (ℤRHom‘𝑌) |
| 14 | 13 | zrhrhm 21522 |
. . . . . . . 8
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
| 15 | 12, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (ℤring RingHom
𝑌)) |
| 16 | | zringbas 21464 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 18 | 16, 17 | rhmf 20485 |
. . . . . . 7
⊢ (𝐿 ∈ (ℤring
RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
| 19 | 15, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌)) |
| 20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌)) |
| 21 | | elfzelz 13564 |
. . . . . . 7
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ) |
| 22 | 21 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℤ) |
| 23 | | zsqcl 14169 |
. . . . . 6
⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈
ℤ) |
| 24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑2) ∈
ℤ) |
| 25 | 20, 24 | ffvelcdmd 7105 |
. . . 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 13593 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ) |
| 37 | 36 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℕ) |
| 38 | 37 | nncnd 12282 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℂ) |
| 39 | | oddprm 16848 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
| 40 | 1, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
| 41 | 40 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
| 42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈
ℕ0) |
| 43 | | 2nn0 12543 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
| 44 | 43 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈
ℕ0) |
| 45 | 38, 42, 44 | expmuld 14189 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = ((𝑦↑2)↑((𝑃 − 1) /
2))) |
| 46 | | prmnn 16711 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 47 | 2, 46 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 48 | 47 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℝ) |
| 49 | | peano2rem 11576 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈
ℝ) |
| 50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
| 51 | 50 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
| 52 | | 2cnd 12344 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) |
| 53 | | 2ne0 12370 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
| 54 | 53 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 0) |
| 55 | 51, 52, 54 | divcan2d 12045 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
| 56 | | phiprm 16814 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
| 57 | 2, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1)) |
| 58 | 55, 57 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) =
(ϕ‘𝑃)) |
| 59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (2 ·
((𝑃 − 1) / 2)) =
(ϕ‘𝑃)) |
| 60 | 59 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = (𝑦↑(ϕ‘𝑃))) |
| 61 | 45, 60 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑2)↑((𝑃 − 1) / 2)) = (𝑦↑(ϕ‘𝑃))) |
| 62 | 61 | oveq1d 7446 |
. . . . . 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 12640 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 66 | 65 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ) |
| 67 | 22, 66 | gcdcomd 16551 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦)) |
| 68 | 37 | nnred 12281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℝ) |
| 69 | 50 | rehalfcld 12513 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℝ) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈
ℝ) |
| 71 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ) |
| 72 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2)) |
| 73 | 72 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ≤ ((𝑃 − 1) / 2)) |
| 74 | | prmuz2 16733 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
| 75 | 2, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
| 76 | | uz2m1nn 12965 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(ℤ≥‘2) → (𝑃 − 1) ∈ ℕ) |
| 77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 − 1) ∈ ℕ) |
| 78 | 77 | nnrpd 13075 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 1) ∈
ℝ+) |
| 79 | | rphalflt 13064 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 − 1) ∈
ℝ+ → ((𝑃 − 1) / 2) < (𝑃 − 1)) |
| 80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑃 − 1) / 2) < (𝑃 − 1)) |
| 81 | 48 | ltm1d 12200 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 − 1) < 𝑃) |
| 82 | 69, 50, 48, 80, 81 | lttrd 11422 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑃 − 1) / 2) < 𝑃) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) < 𝑃) |
| 84 | 68, 70, 71, 73, 83 | lelttrd 11419 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 < 𝑃) |
| 85 | 68, 71 | ltnled 11408 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑦)) |
| 86 | 84, 85 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ≤ 𝑦) |
| 87 | | dvdsle 16347 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦)) |
| 88 | 66, 37, 87 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦)) |
| 89 | 86, 88 | mtod 198 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ 𝑦) |
| 90 | | coprm 16748 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ) → (¬
𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1)) |
| 91 | 63, 22, 90 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1)) |
| 92 | 89, 91 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑦) = 1) |
| 93 | 67, 92 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = 1) |
| 94 | | eulerth 16820 |
. . . . . . 7
⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ (𝑦 gcd 𝑃) = 1) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
| 95 | 64, 22, 93, 94 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃)) |
| 96 | 62, 95 | eqtrd 2777 |
. . . . 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 27390 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0g‘𝑌)) |
| 98 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑌 ↑s
(Base‘𝑌)) = (𝑌 ↑s
(Base‘𝑌)) |
| 99 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝑌
↑s (Base‘𝑌))) = (Base‘(𝑌 ↑s (Base‘𝑌))) |
| 100 | | fvexd 6921 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝑌) ∈ V) |
| 101 | 29, 26, 98, 17 | evl1rhm 22336 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ CRing → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌)))) |
| 102 | 10, 101 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌)))) |
| 103 | 27, 99 | rhmf 20485 |
. . . . . . . . . 10
⊢ (𝑂 ∈ (𝑆 RingHom (𝑌 ↑s (Base‘𝑌))) → 𝑂:𝐵⟶(Base‘(𝑌 ↑s (Base‘𝑌)))) |
| 104 | 102, 103 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑌 ↑s (Base‘𝑌)))) |
| 105 | 26 | ply1ring 22249 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑆 ∈ Ring) |
| 106 | 12, 105 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Ring) |
| 107 | | ringgrp 20235 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp) |
| 108 | 106, 107 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ Grp) |
| 109 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
| 110 | 109, 27 | mgpbas 20142 |
. . . . . . . . . . . 12
⊢ 𝐵 =
(Base‘(mulGrp‘𝑆)) |
| 111 | 109 | ringmgp 20236 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
| 112 | 106, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
| 113 | 31, 26, 27 | vr1cl 22219 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Ring → 𝑋 ∈ 𝐵) |
| 114 | 12, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 115 | 110, 30, 112, 41, 114 | mulgnn0cld 19113 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵) |
| 116 | 27, 33 | ringidcl 20262 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 1 ∈ 𝐵) |
| 117 | 106, 116 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈ 𝐵) |
| 118 | 27, 32 | grpsubcl 19038 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Grp ∧ (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
| 119 | 108, 115,
117, 118 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
| 120 | 34, 119 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ 𝐵) |
| 121 | 104, 120 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘𝑇) ∈ (Base‘(𝑌 ↑s (Base‘𝑌)))) |
| 122 | 98, 17, 99, 5, 100, 121 | pwselbas 17534 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘𝑇):(Base‘𝑌)⟶(Base‘𝑌)) |
| 123 | 122 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → (𝑂‘𝑇) Fn (Base‘𝑌)) |
| 124 | 123 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑂‘𝑇) Fn (Base‘𝑌)) |
| 125 | | fniniseg 7080 |
. . . . 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 713 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(𝑦↑2)) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 128 | | lgsqr.g |
. . 3
⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2))) |
| 129 | 127, 128 | fmptd 7134 |
. 2
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))⟶(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 130 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑥↑2))) |
| 131 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐿‘(𝑥↑2)) ∈ V |
| 132 | 130, 128,
131 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2))) |
| 133 | 132 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2))) |
| 134 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑧↑2))) |
| 135 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐿‘(𝑧↑2)) ∈ V |
| 136 | 134, 128,
135 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2))) |
| 137 | 136 | ad2antll 729 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2))) |
| 138 | 133, 137 | eqeq12d 2753 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ (𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)))) |
| 139 | 47 | nnnn0d 12587 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
| 140 | 139 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈
ℕ0) |
| 141 | | elfzelz 13564 |
. . . . . . . 8
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ) |
| 142 | 141 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℤ) |
| 143 | | zsqcl 14169 |
. . . . . . 7
⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈
ℤ) |
| 144 | 142, 143 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥↑2) ∈
ℤ) |
| 145 | | elfzelz 13564 |
. . . . . . . 8
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℤ) |
| 146 | 145 | ad2antll 729 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℤ) |
| 147 | | zsqcl 14169 |
. . . . . . 7
⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈
ℤ) |
| 148 | 146, 147 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧↑2) ∈
ℤ) |
| 149 | 3, 13 | zndvds 21568 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ0
∧ (𝑥↑2) ∈
ℤ ∧ (𝑧↑2)
∈ ℤ) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2)))) |
| 150 | 140, 144,
148, 149 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2)))) |
| 151 | | elfznn 13593 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ) |
| 152 | 151 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℕ) |
| 153 | 152 | nncnd 12282 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℂ) |
| 154 | | elfznn 13593 |
. . . . . . . . 9
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℕ) |
| 155 | 154 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℕ) |
| 156 | 155 | nncnd 12282 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℂ) |
| 157 | | subsq 14249 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧))) |
| 158 | 153, 156,
157 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧))) |
| 159 | 158 | breq2d 5155 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥↑2) − (𝑧↑2)) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)))) |
| 160 | 138, 150,
159 | 3bitrd 305 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)))) |
| 161 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ) |
| 162 | 142, 146 | zaddcld 12726 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℤ) |
| 163 | 142, 146 | zsubcld 12727 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 − 𝑧) ∈ ℤ) |
| 164 | | euclemma 16750 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑥 + 𝑧) ∈ ℤ ∧ (𝑥 − 𝑧) ∈ ℤ) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)))) |
| 165 | 161, 162,
163, 164 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)))) |
| 166 | 161, 46 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ) |
| 167 | 166 | nnzd 12640 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ) |
| 168 | 152, 155 | nnaddcld 12318 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℕ) |
| 169 | | dvdsle 16347 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ (𝑥 + 𝑧) ∈ ℕ) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧))) |
| 170 | 167, 168,
169 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧))) |
| 171 | 168 | nnred 12281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℝ) |
| 172 | 166 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ) |
| 173 | 172, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈
ℝ) |
| 174 | 152 | nnred 12281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℝ) |
| 175 | 155 | nnred 12281 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℝ) |
| 176 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈
ℝ) |
| 177 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
| 178 | 177 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2)) |
| 179 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ≤ ((𝑃 − 1) / 2)) |
| 180 | 179 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ≤ ((𝑃 − 1) / 2)) |
| 181 | 174, 175,
176, 176, 178, 180 | le2addd 11882 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2))) |
| 182 | 51 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈
ℂ) |
| 183 | 182 | 2halvesd 12512 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1)) |
| 184 | 181, 183 | breqtrd 5169 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (𝑃 − 1)) |
| 185 | 172 | ltm1d 12200 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) < 𝑃) |
| 186 | 171, 173,
172, 184, 185 | lelttrd 11419 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) < 𝑃) |
| 187 | 171, 172 | ltnled 11408 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 + 𝑧) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑥 + 𝑧))) |
| 188 | 186, 187 | mpbid 232 |
. . . . . . . 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 16301 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧))) |
| 192 | 166, 142,
146, 191 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧))) |
| 193 | 166 | nnrpd 13075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈
ℝ+) |
| 194 | 152 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈
ℕ0) |
| 195 | 194 | nn0ge0d 12590 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑥) |
| 196 | 82 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) < 𝑃) |
| 197 | 174, 176,
172, 178, 196 | lelttrd 11419 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 < 𝑃) |
| 198 | | modid 13936 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑃)) → (𝑥 mod 𝑃) = 𝑥) |
| 199 | 174, 193,
195, 197, 198 | syl22anc 839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 mod 𝑃) = 𝑥) |
| 200 | 155 | nnnn0d 12587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈
ℕ0) |
| 201 | 200 | nn0ge0d 12590 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑧) |
| 202 | 175, 176,
172, 180, 196 | lelttrd 11419 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 < 𝑃) |
| 203 | | modid 13936 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ+)
∧ (0 ≤ 𝑧 ∧ 𝑧 < 𝑃)) → (𝑧 mod 𝑃) = 𝑧) |
| 204 | 175, 193,
201, 202, 203 | syl22anc 839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧 mod 𝑃) = 𝑧) |
| 205 | 199, 204 | eqeq12d 2753 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑥 = 𝑧)) |
| 206 | 192, 205 | bitr3d 281 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) ↔ 𝑥 = 𝑧)) |
| 207 | 206 | biimpd 229 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) → 𝑥 = 𝑧)) |
| 208 | 190, 207 | jaod 860 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)) → 𝑥 = 𝑧)) |
| 209 | 165, 208 | sylbid 240 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) → 𝑥 = 𝑧)) |
| 210 | 160, 209 | sylbid 240 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)) |
| 211 | 210 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)) |
| 212 | | dff13 7275 |
. 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‘𝑌)})) |