Proof of Theorem lgsqrlem4
| Step | Hyp | Ref
| Expression |
| 1 | | lgsqr.y |
. . . . . . 7
⊢ 𝑌 =
(ℤ/nℤ‘𝑃) |
| 2 | | lgsqr.s |
. . . . . . 7
⊢ 𝑆 = (Poly1‘𝑌) |
| 3 | | lgsqr.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
| 4 | | lgsqr.d |
. . . . . . 7
⊢ 𝐷 = (deg1‘𝑌) |
| 5 | | lgsqr.o |
. . . . . . 7
⊢ 𝑂 = (eval1‘𝑌) |
| 6 | | lgsqr.e |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑆)) |
| 7 | | lgsqr.x |
. . . . . . 7
⊢ 𝑋 = (var1‘𝑌) |
| 8 | | lgsqr.m |
. . . . . . 7
⊢ − =
(-g‘𝑆) |
| 9 | | lgsqr.u |
. . . . . . 7
⊢ 1 =
(1r‘𝑆) |
| 10 | | lgsqr.t |
. . . . . . 7
⊢ 𝑇 = ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) |
| 11 | | lgsqr.l |
. . . . . . 7
⊢ 𝐿 = (ℤRHom‘𝑌) |
| 12 | | lgsqr.1 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ (ℙ ∖
{2})) |
| 13 | | lgsqr.g |
. . . . . . 7
⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2))) |
| 14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | lgsqrlem2 27391 |
. . . . . 6
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 15 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝑂‘𝑇) ∈ V |
| 16 | 15 | cnvex 7947 |
. . . . . . . . . . 11
⊢ ◡(𝑂‘𝑇) ∈ V |
| 17 | 16 | imaex 7936 |
. . . . . . . . . 10
⊢ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∈ V |
| 18 | 17 | f1dom 9014 |
. . . . . . . . 9
⊢ (𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) → (1...((𝑃 − 1) / 2)) ≼ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 19 | 14, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ≼ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 20 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑌) = (0g‘𝑌) |
| 21 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑆) = (0g‘𝑆) |
| 22 | 12 | eldifad 3963 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 23 | 1 | znfld 21579 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ Field) |
| 25 | | fldidom 20771 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ IDomn) |
| 27 | | isidom 20725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn)) |
| 28 | 27 | simplbi 497 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ CRing) |
| 29 | 26, 28 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 ∈ CRing) |
| 30 | | crngring 20242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ Ring) |
| 32 | 2 | ply1ring 22249 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ∈ Ring → 𝑆 ∈ Ring) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈ Ring) |
| 34 | | ringgrp 20235 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ Grp) |
| 36 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
| 37 | 36, 3 | mgpbas 20142 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 =
(Base‘(mulGrp‘𝑆)) |
| 38 | 36 | ringmgp 20236 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
| 39 | 33, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
| 40 | | oddprm 16848 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((𝑃 − 1) / 2)
∈ ℕ) |
| 41 | 12, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
| 42 | 41 | nnnn0d 12587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
| 43 | 7, 2, 3 | vr1cl 22219 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ∈ Ring → 𝑋 ∈ 𝐵) |
| 44 | 31, 43 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 45 | 37, 6, 39, 42, 44 | mulgnn0cld 19113 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵) |
| 46 | 3, 9 | ringidcl 20262 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ Ring → 1 ∈ 𝐵) |
| 47 | 33, 46 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈ 𝐵) |
| 48 | 3, 8 | grpsubcl 19038 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Grp ∧ (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
| 49 | 35, 45, 47, 48 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵) |
| 50 | 10, 49 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ 𝐵) |
| 51 | 10 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷‘𝑇) = (𝐷‘((((𝑃 − 1) / 2) ↑ 𝑋) − 1 )) |
| 52 | 41 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < ((𝑃 − 1) / 2)) |
| 53 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(algSc‘𝑆) =
(algSc‘𝑆) |
| 54 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1r‘𝑌) = (1r‘𝑌) |
| 55 | 2, 53, 54, 9 | ply1scl1 22296 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑌 ∈ Ring →
((algSc‘𝑆)‘(1r‘𝑌)) = 1 ) |
| 56 | 31, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((algSc‘𝑆)‘(1r‘𝑌)) = 1 ) |
| 57 | 56 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐷‘((algSc‘𝑆)‘(1r‘𝑌))) = (𝐷‘ 1 )) |
| 58 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 59 | 58, 54 | ringidcl 20262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑌 ∈ Ring →
(1r‘𝑌)
∈ (Base‘𝑌)) |
| 60 | 31, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1r‘𝑌) ∈ (Base‘𝑌)) |
| 61 | | domnnzr 20706 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑌 ∈ Domn → 𝑌 ∈ NzRing) |
| 62 | 27, 61 | simplbiim 504 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑌 ∈ IDomn → 𝑌 ∈ NzRing) |
| 63 | 26, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑌 ∈ NzRing) |
| 64 | 54, 20 | nzrnz 20515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑌 ∈ NzRing →
(1r‘𝑌)
≠ (0g‘𝑌)) |
| 65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1r‘𝑌) ≠
(0g‘𝑌)) |
| 66 | 4, 2, 58, 53, 20 | deg1scl 26152 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 ∈ Ring ∧
(1r‘𝑌)
∈ (Base‘𝑌) ∧
(1r‘𝑌)
≠ (0g‘𝑌)) → (𝐷‘((algSc‘𝑆)‘(1r‘𝑌))) = 0) |
| 67 | 31, 60, 65, 66 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐷‘((algSc‘𝑆)‘(1r‘𝑌))) = 0) |
| 68 | 57, 67 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐷‘ 1 ) = 0) |
| 69 | 4, 2, 7, 36, 6 | deg1pw 26160 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑌 ∈ NzRing ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝐷‘(((𝑃 − 1) / 2) ↑ 𝑋)) = ((𝑃 − 1) / 2)) |
| 70 | 63, 42, 69 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐷‘(((𝑃 − 1) / 2) ↑ 𝑋)) = ((𝑃 − 1) / 2)) |
| 71 | 52, 68, 70 | 3brtr4d 5175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘ 1 ) < (𝐷‘(((𝑃 − 1) / 2) ↑ 𝑋))) |
| 72 | 2, 4, 31, 3, 8, 45, 47, 71 | deg1sub 26147 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷‘((((𝑃 − 1) / 2) ↑ 𝑋) − 1 )) = (𝐷‘(((𝑃 − 1) / 2) ↑ 𝑋))) |
| 73 | 51, 72 | eqtrid 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷‘𝑇) = (𝐷‘(((𝑃 − 1) / 2) ↑ 𝑋))) |
| 74 | 73, 70 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷‘𝑇) = ((𝑃 − 1) / 2)) |
| 75 | 74, 42 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷‘𝑇) ∈
ℕ0) |
| 76 | 4, 2, 21, 3 | deg1nn0clb 26129 |
. . . . . . . . . . . . . 14
⊢ ((𝑌 ∈ Ring ∧ 𝑇 ∈ 𝐵) → (𝑇 ≠ (0g‘𝑆) ↔ (𝐷‘𝑇) ∈
ℕ0)) |
| 77 | 31, 50, 76 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ≠ (0g‘𝑆) ↔ (𝐷‘𝑇) ∈
ℕ0)) |
| 78 | 75, 77 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ≠ (0g‘𝑆)) |
| 79 | 2, 3, 4, 5, 20, 21, 26, 50, 78 | fta1g 26209 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) ≤ (𝐷‘𝑇)) |
| 80 | 79, 74 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) ≤ ((𝑃 − 1) / 2)) |
| 81 | | hashfz1 14385 |
. . . . . . . . . . 11
⊢ (((𝑃 − 1) / 2) ∈
ℕ0 → (♯‘(1...((𝑃 − 1) / 2))) = ((𝑃 − 1) / 2)) |
| 82 | 42, 81 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(♯‘(1...((𝑃
− 1) / 2))) = ((𝑃
− 1) / 2)) |
| 83 | 80, 82 | breqtrrd 5171 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) ≤
(♯‘(1...((𝑃
− 1) / 2)))) |
| 84 | | hashbnd 14375 |
. . . . . . . . . . 11
⊢ (((◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∈ V ∧ ((𝑃 − 1) / 2) ∈
ℕ0 ∧ (♯‘(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) ≤ ((𝑃 − 1) / 2)) → (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∈ Fin) |
| 85 | 17, 42, 80, 84 | mp3an2i 1468 |
. . . . . . . . . 10
⊢ (𝜑 → (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∈ Fin) |
| 86 | | fzfid 14014 |
. . . . . . . . . 10
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ∈
Fin) |
| 87 | | hashdom 14418 |
. . . . . . . . . 10
⊢ (((◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∈ Fin ∧
(1...((𝑃 − 1) / 2))
∈ Fin) → ((♯‘(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) ≤
(♯‘(1...((𝑃
− 1) / 2))) ↔ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ≼ (1...((𝑃 − 1) /
2)))) |
| 88 | 85, 86, 87 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) ≤
(♯‘(1...((𝑃
− 1) / 2))) ↔ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ≼ (1...((𝑃 − 1) /
2)))) |
| 89 | 83, 88 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ≼ (1...((𝑃 − 1) /
2))) |
| 90 | | sbth 9133 |
. . . . . . . 8
⊢
(((1...((𝑃 −
1) / 2)) ≼ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∧ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ≼ (1...((𝑃 − 1) / 2))) →
(1...((𝑃 − 1) / 2))
≈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 91 | 19, 89, 90 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (1...((𝑃 − 1) / 2)) ≈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 92 | | f1finf1o 9305 |
. . . . . . 7
⊢
(((1...((𝑃 −
1) / 2)) ≈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∧ (◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∈ Fin) → (𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ 𝐺:(1...((𝑃 − 1) / 2))–1-1-onto→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}))) |
| 93 | 91, 85, 92 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐺:(1...((𝑃 − 1) / 2))–1-1→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ↔ 𝐺:(1...((𝑃 − 1) / 2))–1-1-onto→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}))) |
| 94 | 14, 93 | mpbid 232 |
. . . . 5
⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))–1-1-onto→(◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 95 | | f1ocnv 6860 |
. . . . 5
⊢ (𝐺:(1...((𝑃 − 1) / 2))–1-1-onto→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) → ◡𝐺:(◡(𝑂‘𝑇) “ {(0g‘𝑌)})–1-1-onto→(1...((𝑃 − 1) / 2))) |
| 96 | | f1of 6848 |
. . . . 5
⊢ (◡𝐺:(◡(𝑂‘𝑇) “ {(0g‘𝑌)})–1-1-onto→(1...((𝑃 − 1) / 2)) → ◡𝐺:(◡(𝑂‘𝑇) “ {(0g‘𝑌)})⟶(1...((𝑃 − 1) /
2))) |
| 97 | 94, 95, 96 | 3syl 18 |
. . . 4
⊢ (𝜑 → ◡𝐺:(◡(𝑂‘𝑇) “ {(0g‘𝑌)})⟶(1...((𝑃 − 1) /
2))) |
| 98 | | lgsqr.3 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 99 | | lgsqr.4 |
. . . . 5
⊢ (𝜑 → (𝐴 /L 𝑃) = 1) |
| 100 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 98, 99 | lgsqrlem3 27392 |
. . . 4
⊢ (𝜑 → (𝐿‘𝐴) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) |
| 101 | 97, 100 | ffvelcdmd 7105 |
. . 3
⊢ (𝜑 → (◡𝐺‘(𝐿‘𝐴)) ∈ (1...((𝑃 − 1) / 2))) |
| 102 | 101 | elfzelzd 13565 |
. 2
⊢ (𝜑 → (◡𝐺‘(𝐿‘𝐴)) ∈ ℤ) |
| 103 | | fvoveq1 7454 |
. . . . . 6
⊢ (𝑥 = (◡𝐺‘(𝐿‘𝐴)) → (𝐿‘(𝑥↑2)) = (𝐿‘((◡𝐺‘(𝐿‘𝐴))↑2))) |
| 104 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑥↑2))) |
| 105 | 104 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2))) = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑥↑2))) |
| 106 | 13, 105 | eqtri 2765 |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑥↑2))) |
| 107 | | fvex 6919 |
. . . . . 6
⊢ (𝐿‘((◡𝐺‘(𝐿‘𝐴))↑2)) ∈ V |
| 108 | 103, 106,
107 | fvmpt 7016 |
. . . . 5
⊢ ((◡𝐺‘(𝐿‘𝐴)) ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘(◡𝐺‘(𝐿‘𝐴))) = (𝐿‘((◡𝐺‘(𝐿‘𝐴))↑2))) |
| 109 | 101, 108 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐺‘(◡𝐺‘(𝐿‘𝐴))) = (𝐿‘((◡𝐺‘(𝐿‘𝐴))↑2))) |
| 110 | | f1ocnvfv2 7297 |
. . . . 5
⊢ ((𝐺:(1...((𝑃 − 1) / 2))–1-1-onto→(◡(𝑂‘𝑇) “ {(0g‘𝑌)}) ∧ (𝐿‘𝐴) ∈ (◡(𝑂‘𝑇) “ {(0g‘𝑌)})) → (𝐺‘(◡𝐺‘(𝐿‘𝐴))) = (𝐿‘𝐴)) |
| 111 | 94, 100, 110 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐺‘(◡𝐺‘(𝐿‘𝐴))) = (𝐿‘𝐴)) |
| 112 | 109, 111 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → (𝐿‘((◡𝐺‘(𝐿‘𝐴))↑2)) = (𝐿‘𝐴)) |
| 113 | | prmnn 16711 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 114 | 22, 113 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 115 | 114 | nnnn0d 12587 |
. . . 4
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
| 116 | | zsqcl 14169 |
. . . . 5
⊢ ((◡𝐺‘(𝐿‘𝐴)) ∈ ℤ → ((◡𝐺‘(𝐿‘𝐴))↑2) ∈ ℤ) |
| 117 | 102, 116 | syl 17 |
. . . 4
⊢ (𝜑 → ((◡𝐺‘(𝐿‘𝐴))↑2) ∈ ℤ) |
| 118 | 1, 11 | zndvds 21568 |
. . . 4
⊢ ((𝑃 ∈ ℕ0
∧ ((◡𝐺‘(𝐿‘𝐴))↑2) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐿‘((◡𝐺‘(𝐿‘𝐴))↑2)) = (𝐿‘𝐴) ↔ 𝑃 ∥ (((◡𝐺‘(𝐿‘𝐴))↑2) − 𝐴))) |
| 119 | 115, 117,
98, 118 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝐿‘((◡𝐺‘(𝐿‘𝐴))↑2)) = (𝐿‘𝐴) ↔ 𝑃 ∥ (((◡𝐺‘(𝐿‘𝐴))↑2) − 𝐴))) |
| 120 | 112, 119 | mpbid 232 |
. 2
⊢ (𝜑 → 𝑃 ∥ (((◡𝐺‘(𝐿‘𝐴))↑2) − 𝐴)) |
| 121 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = (◡𝐺‘(𝐿‘𝐴)) → (𝑥↑2) = ((◡𝐺‘(𝐿‘𝐴))↑2)) |
| 122 | 121 | oveq1d 7446 |
. . . 4
⊢ (𝑥 = (◡𝐺‘(𝐿‘𝐴)) → ((𝑥↑2) − 𝐴) = (((◡𝐺‘(𝐿‘𝐴))↑2) − 𝐴)) |
| 123 | 122 | breq2d 5155 |
. . 3
⊢ (𝑥 = (◡𝐺‘(𝐿‘𝐴)) → (𝑃 ∥ ((𝑥↑2) − 𝐴) ↔ 𝑃 ∥ (((◡𝐺‘(𝐿‘𝐴))↑2) − 𝐴))) |
| 124 | 123 | rspcev 3622 |
. 2
⊢ (((◡𝐺‘(𝐿‘𝐴)) ∈ ℤ ∧ 𝑃 ∥ (((◡𝐺‘(𝐿‘𝐴))↑2) − 𝐴)) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)) |
| 125 | 102, 120,
124 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − 𝐴)) |