MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgsqrlem4 Structured version   Visualization version   GIF version

Theorem lgsqrlem4 27088
Description: Lemma for lgsqr 27090. (Contributed by Mario Carneiro, 15-Jun-2015.)
Hypotheses
Ref Expression
lgsqr.y π‘Œ = (β„€/nβ„€β€˜π‘ƒ)
lgsqr.s 𝑆 = (Poly1β€˜π‘Œ)
lgsqr.b 𝐡 = (Baseβ€˜π‘†)
lgsqr.d 𝐷 = ( deg1 β€˜π‘Œ)
lgsqr.o 𝑂 = (eval1β€˜π‘Œ)
lgsqr.e ↑ = (.gβ€˜(mulGrpβ€˜π‘†))
lgsqr.x 𝑋 = (var1β€˜π‘Œ)
lgsqr.m βˆ’ = (-gβ€˜π‘†)
lgsqr.u 1 = (1rβ€˜π‘†)
lgsqr.t 𝑇 = ((((𝑃 βˆ’ 1) / 2) ↑ 𝑋) βˆ’ 1 )
lgsqr.l 𝐿 = (β„€RHomβ€˜π‘Œ)
lgsqr.1 (πœ‘ β†’ 𝑃 ∈ (β„™ βˆ– {2}))
lgsqr.g 𝐺 = (𝑦 ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(𝑦↑2)))
lgsqr.3 (πœ‘ β†’ 𝐴 ∈ β„€)
lgsqr.4 (πœ‘ β†’ (𝐴 /L 𝑃) = 1)
Assertion
Ref Expression
lgsqrlem4 (πœ‘ β†’ βˆƒπ‘₯ ∈ β„€ 𝑃 βˆ₯ ((π‘₯↑2) βˆ’ 𝐴))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐺   𝑦,𝑂   π‘₯,𝑦,𝑃   πœ‘,π‘₯,𝑦   𝑦,𝑇   π‘₯,𝐿,𝑦   π‘₯,π‘Œ,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝐡(π‘₯,𝑦)   𝐷(π‘₯,𝑦)   𝑆(π‘₯,𝑦)   𝑇(π‘₯)   1 (π‘₯,𝑦)   ↑ (π‘₯,𝑦)   𝐺(𝑦)   βˆ’ (π‘₯,𝑦)   𝑂(π‘₯)   𝑋(π‘₯,𝑦)

Proof of Theorem lgsqrlem4
StepHypRef 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)))
141, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13lgsqrlem2 27086 . . . . . 6 (πœ‘ β†’ 𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1β†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}))
15 fvex 6903 . . . . . . . . . . . 12 (π‘‚β€˜π‘‡) ∈ V
1615cnvex 7918 . . . . . . . . . . 11 β—‘(π‘‚β€˜π‘‡) ∈ V
1716imaex 7909 . . . . . . . . . 10 (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∈ V
1817f1dom 8972 . . . . . . . . 9 (𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1β†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) β†’ (1...((𝑃 βˆ’ 1) / 2)) β‰Ό (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}))
1914, 18syl 17 . . . . . . . 8 (πœ‘ β†’ (1...((𝑃 βˆ’ 1) / 2)) β‰Ό (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}))
20 eqid 2730 . . . . . . . . . . . 12 (0gβ€˜π‘Œ) = (0gβ€˜π‘Œ)
21 eqid 2730 . . . . . . . . . . . 12 (0gβ€˜π‘†) = (0gβ€˜π‘†)
2212eldifad 3959 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ β„™)
231znfld 21335 . . . . . . . . . . . . . 14 (𝑃 ∈ β„™ β†’ π‘Œ ∈ Field)
2422, 23syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ π‘Œ ∈ Field)
25 fldidom 21123 . . . . . . . . . . . . 13 (π‘Œ ∈ Field β†’ π‘Œ ∈ IDomn)
2624, 25syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ ∈ IDomn)
27 isidom 21122 . . . . . . . . . . . . . . . . . . 19 (π‘Œ ∈ IDomn ↔ (π‘Œ ∈ CRing ∧ π‘Œ ∈ Domn))
2827simplbi 496 . . . . . . . . . . . . . . . . . 18 (π‘Œ ∈ IDomn β†’ π‘Œ ∈ CRing)
2926, 28syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Œ ∈ CRing)
30 crngring 20139 . . . . . . . . . . . . . . . . 17 (π‘Œ ∈ CRing β†’ π‘Œ ∈ Ring)
3129, 30syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ π‘Œ ∈ Ring)
322ply1ring 21990 . . . . . . . . . . . . . . . 16 (π‘Œ ∈ Ring β†’ 𝑆 ∈ Ring)
3331, 32syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑆 ∈ Ring)
34 ringgrp 20132 . . . . . . . . . . . . . . 15 (𝑆 ∈ Ring β†’ 𝑆 ∈ Grp)
3533, 34syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 ∈ Grp)
36 eqid 2730 . . . . . . . . . . . . . . . 16 (mulGrpβ€˜π‘†) = (mulGrpβ€˜π‘†)
3736, 3mgpbas 20034 . . . . . . . . . . . . . . 15 𝐡 = (Baseβ€˜(mulGrpβ€˜π‘†))
3836ringmgp 20133 . . . . . . . . . . . . . . . 16 (𝑆 ∈ Ring β†’ (mulGrpβ€˜π‘†) ∈ Mnd)
3933, 38syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (mulGrpβ€˜π‘†) ∈ Mnd)
40 oddprm 16747 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (β„™ βˆ– {2}) β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•)
4112, 40syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•)
4241nnnn0d 12536 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑃 βˆ’ 1) / 2) ∈ β„•0)
437, 2, 3vr1cl 21960 . . . . . . . . . . . . . . . 16 (π‘Œ ∈ Ring β†’ 𝑋 ∈ 𝐡)
4431, 43syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 ∈ 𝐡)
4537, 6, 39, 42, 44mulgnn0cld 19011 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((𝑃 βˆ’ 1) / 2) ↑ 𝑋) ∈ 𝐡)
463, 9ringidcl 20154 . . . . . . . . . . . . . . 15 (𝑆 ∈ Ring β†’ 1 ∈ 𝐡)
4733, 46syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 1 ∈ 𝐡)
483, 8grpsubcl 18939 . . . . . . . . . . . . . 14 ((𝑆 ∈ Grp ∧ (((𝑃 βˆ’ 1) / 2) ↑ 𝑋) ∈ 𝐡 ∧ 1 ∈ 𝐡) β†’ ((((𝑃 βˆ’ 1) / 2) ↑ 𝑋) βˆ’ 1 ) ∈ 𝐡)
4935, 45, 47, 48syl3anc 1369 . . . . . . . . . . . . 13 (πœ‘ β†’ ((((𝑃 βˆ’ 1) / 2) ↑ 𝑋) βˆ’ 1 ) ∈ 𝐡)
5010, 49eqeltrid 2835 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 ∈ 𝐡)
5110fveq2i 6893 . . . . . . . . . . . . . . . 16 (π·β€˜π‘‡) = (π·β€˜((((𝑃 βˆ’ 1) / 2) ↑ 𝑋) βˆ’ 1 ))
5241nngt0d 12265 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 0 < ((𝑃 βˆ’ 1) / 2))
53 eqid 2730 . . . . . . . . . . . . . . . . . . . . . 22 (algScβ€˜π‘†) = (algScβ€˜π‘†)
54 eqid 2730 . . . . . . . . . . . . . . . . . . . . . 22 (1rβ€˜π‘Œ) = (1rβ€˜π‘Œ)
552, 53, 54, 9ply1scl1 22035 . . . . . . . . . . . . . . . . . . . . 21 (π‘Œ ∈ Ring β†’ ((algScβ€˜π‘†)β€˜(1rβ€˜π‘Œ)) = 1 )
5631, 55syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((algScβ€˜π‘†)β€˜(1rβ€˜π‘Œ)) = 1 )
5756fveq2d 6894 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π·β€˜((algScβ€˜π‘†)β€˜(1rβ€˜π‘Œ))) = (π·β€˜ 1 ))
58 eqid 2730 . . . . . . . . . . . . . . . . . . . . . 22 (Baseβ€˜π‘Œ) = (Baseβ€˜π‘Œ)
5958, 54ringidcl 20154 . . . . . . . . . . . . . . . . . . . . 21 (π‘Œ ∈ Ring β†’ (1rβ€˜π‘Œ) ∈ (Baseβ€˜π‘Œ))
6031, 59syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1rβ€˜π‘Œ) ∈ (Baseβ€˜π‘Œ))
61 domnnzr 21111 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Œ ∈ Domn β†’ π‘Œ ∈ NzRing)
6227, 61simplbiim 503 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Œ ∈ IDomn β†’ π‘Œ ∈ NzRing)
6326, 62syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ π‘Œ ∈ NzRing)
6454, 20nzrnz 20406 . . . . . . . . . . . . . . . . . . . . 21 (π‘Œ ∈ NzRing β†’ (1rβ€˜π‘Œ) β‰  (0gβ€˜π‘Œ))
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1rβ€˜π‘Œ) β‰  (0gβ€˜π‘Œ))
664, 2, 58, 53, 20deg1scl 25866 . . . . . . . . . . . . . . . . . . . 20 ((π‘Œ ∈ Ring ∧ (1rβ€˜π‘Œ) ∈ (Baseβ€˜π‘Œ) ∧ (1rβ€˜π‘Œ) β‰  (0gβ€˜π‘Œ)) β†’ (π·β€˜((algScβ€˜π‘†)β€˜(1rβ€˜π‘Œ))) = 0)
6731, 60, 65, 66syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π·β€˜((algScβ€˜π‘†)β€˜(1rβ€˜π‘Œ))) = 0)
6857, 67eqtr3d 2772 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π·β€˜ 1 ) = 0)
694, 2, 7, 36, 6deg1pw 25873 . . . . . . . . . . . . . . . . . . 19 ((π‘Œ ∈ NzRing ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0) β†’ (π·β€˜(((𝑃 βˆ’ 1) / 2) ↑ 𝑋)) = ((𝑃 βˆ’ 1) / 2))
7063, 42, 69syl2anc 582 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π·β€˜(((𝑃 βˆ’ 1) / 2) ↑ 𝑋)) = ((𝑃 βˆ’ 1) / 2))
7152, 68, 703brtr4d 5179 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π·β€˜ 1 ) < (π·β€˜(((𝑃 βˆ’ 1) / 2) ↑ 𝑋)))
722, 4, 31, 3, 8, 45, 47, 71deg1sub 25861 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π·β€˜((((𝑃 βˆ’ 1) / 2) ↑ 𝑋) βˆ’ 1 )) = (π·β€˜(((𝑃 βˆ’ 1) / 2) ↑ 𝑋)))
7351, 72eqtrid 2782 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π·β€˜π‘‡) = (π·β€˜(((𝑃 βˆ’ 1) / 2) ↑ 𝑋)))
7473, 70eqtrd 2770 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π·β€˜π‘‡) = ((𝑃 βˆ’ 1) / 2))
7574, 42eqeltrd 2831 . . . . . . . . . . . . 13 (πœ‘ β†’ (π·β€˜π‘‡) ∈ β„•0)
764, 2, 21, 3deg1nn0clb 25843 . . . . . . . . . . . . . 14 ((π‘Œ ∈ Ring ∧ 𝑇 ∈ 𝐡) β†’ (𝑇 β‰  (0gβ€˜π‘†) ↔ (π·β€˜π‘‡) ∈ β„•0))
7731, 50, 76syl2anc 582 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑇 β‰  (0gβ€˜π‘†) ↔ (π·β€˜π‘‡) ∈ β„•0))
7875, 77mpbird 256 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 β‰  (0gβ€˜π‘†))
792, 3, 4, 5, 20, 21, 26, 50, 78fta1g 25920 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})) ≀ (π·β€˜π‘‡))
8079, 74breqtrd 5173 . . . . . . . . . 10 (πœ‘ β†’ (β™―β€˜(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})) ≀ ((𝑃 βˆ’ 1) / 2))
81 hashfz1 14310 . . . . . . . . . . 11 (((𝑃 βˆ’ 1) / 2) ∈ β„•0 β†’ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))) = ((𝑃 βˆ’ 1) / 2))
8242, 81syl 17 . . . . . . . . . 10 (πœ‘ β†’ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))) = ((𝑃 βˆ’ 1) / 2))
8380, 82breqtrrd 5175 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})) ≀ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))))
84 hashbnd 14300 . . . . . . . . . . 11 (((β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∈ V ∧ ((𝑃 βˆ’ 1) / 2) ∈ β„•0 ∧ (β™―β€˜(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})) ≀ ((𝑃 βˆ’ 1) / 2)) β†’ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∈ Fin)
8517, 42, 80, 84mp3an2i 1464 . . . . . . . . . 10 (πœ‘ β†’ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∈ Fin)
86 fzfid 13942 . . . . . . . . . 10 (πœ‘ β†’ (1...((𝑃 βˆ’ 1) / 2)) ∈ Fin)
87 hashdom 14343 . . . . . . . . . 10 (((β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∈ Fin ∧ (1...((𝑃 βˆ’ 1) / 2)) ∈ Fin) β†’ ((β™―β€˜(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})) ≀ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))) ↔ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) β‰Ό (1...((𝑃 βˆ’ 1) / 2))))
8885, 86, 87syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ ((β™―β€˜(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})) ≀ (β™―β€˜(1...((𝑃 βˆ’ 1) / 2))) ↔ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) β‰Ό (1...((𝑃 βˆ’ 1) / 2))))
8983, 88mpbid 231 . . . . . . . 8 (πœ‘ β†’ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) β‰Ό (1...((𝑃 βˆ’ 1) / 2)))
90 sbth 9095 . . . . . . . 8 (((1...((𝑃 βˆ’ 1) / 2)) β‰Ό (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∧ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) β‰Ό (1...((𝑃 βˆ’ 1) / 2))) β†’ (1...((𝑃 βˆ’ 1) / 2)) β‰ˆ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}))
9119, 89, 90syl2anc 582 . . . . . . 7 (πœ‘ β†’ (1...((𝑃 βˆ’ 1) / 2)) β‰ˆ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}))
92 f1finf1o 9273 . . . . . . 7 (((1...((𝑃 βˆ’ 1) / 2)) β‰ˆ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∧ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∈ Fin) β†’ (𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1β†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ↔ 𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1-ontoβ†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})))
9391, 85, 92syl2anc 582 . . . . . 6 (πœ‘ β†’ (𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1β†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ↔ 𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1-ontoβ†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})))
9414, 93mpbid 231 . . . . 5 (πœ‘ β†’ 𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1-ontoβ†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}))
95 f1ocnv 6844 . . . . 5 (𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1-ontoβ†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) β†’ ◑𝐺:(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})–1-1-ontoβ†’(1...((𝑃 βˆ’ 1) / 2)))
96 f1of 6832 . . . . 5 (◑𝐺:(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})–1-1-ontoβ†’(1...((𝑃 βˆ’ 1) / 2)) β†’ ◑𝐺:(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})⟢(1...((𝑃 βˆ’ 1) / 2)))
9794, 95, 963syl 18 . . . 4 (πœ‘ β†’ ◑𝐺:(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})⟢(1...((𝑃 βˆ’ 1) / 2)))
98 lgsqr.3 . . . . 5 (πœ‘ β†’ 𝐴 ∈ β„€)
99 lgsqr.4 . . . . 5 (πœ‘ β†’ (𝐴 /L 𝑃) = 1)
1001, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 98, 99lgsqrlem3 27087 . . . 4 (πœ‘ β†’ (πΏβ€˜π΄) ∈ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}))
10197, 100ffvelcdmd 7086 . . 3 (πœ‘ β†’ (β—‘πΊβ€˜(πΏβ€˜π΄)) ∈ (1...((𝑃 βˆ’ 1) / 2)))
102101elfzelzd 13506 . 2 (πœ‘ β†’ (β—‘πΊβ€˜(πΏβ€˜π΄)) ∈ β„€)
103 fvoveq1 7434 . . . . . 6 (π‘₯ = (β—‘πΊβ€˜(πΏβ€˜π΄)) β†’ (πΏβ€˜(π‘₯↑2)) = (πΏβ€˜((β—‘πΊβ€˜(πΏβ€˜π΄))↑2)))
104 fvoveq1 7434 . . . . . . . 8 (𝑦 = π‘₯ β†’ (πΏβ€˜(𝑦↑2)) = (πΏβ€˜(π‘₯↑2)))
105104cbvmptv 5260 . . . . . . 7 (𝑦 ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(𝑦↑2))) = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(π‘₯↑2)))
10613, 105eqtri 2758 . . . . . 6 𝐺 = (π‘₯ ∈ (1...((𝑃 βˆ’ 1) / 2)) ↦ (πΏβ€˜(π‘₯↑2)))
107 fvex 6903 . . . . . 6 (πΏβ€˜((β—‘πΊβ€˜(πΏβ€˜π΄))↑2)) ∈ V
108103, 106, 107fvmpt 6997 . . . . 5 ((β—‘πΊβ€˜(πΏβ€˜π΄)) ∈ (1...((𝑃 βˆ’ 1) / 2)) β†’ (πΊβ€˜(β—‘πΊβ€˜(πΏβ€˜π΄))) = (πΏβ€˜((β—‘πΊβ€˜(πΏβ€˜π΄))↑2)))
109101, 108syl 17 . . . 4 (πœ‘ β†’ (πΊβ€˜(β—‘πΊβ€˜(πΏβ€˜π΄))) = (πΏβ€˜((β—‘πΊβ€˜(πΏβ€˜π΄))↑2)))
110 f1ocnvfv2 7277 . . . . 5 ((𝐺:(1...((𝑃 βˆ’ 1) / 2))–1-1-ontoβ†’(β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)}) ∧ (πΏβ€˜π΄) ∈ (β—‘(π‘‚β€˜π‘‡) β€œ {(0gβ€˜π‘Œ)})) β†’ (πΊβ€˜(β—‘πΊβ€˜(πΏβ€˜π΄))) = (πΏβ€˜π΄))
11194, 100, 110syl2anc 582 . . . 4 (πœ‘ β†’ (πΊβ€˜(β—‘πΊβ€˜(πΏβ€˜π΄))) = (πΏβ€˜π΄))
112109, 111eqtr3d 2772 . . 3 (πœ‘ β†’ (πΏβ€˜((β—‘πΊβ€˜(πΏβ€˜π΄))↑2)) = (πΏβ€˜π΄))
113 prmnn 16615 . . . . . 6 (𝑃 ∈ β„™ β†’ 𝑃 ∈ β„•)
11422, 113syl 17 . . . . 5 (πœ‘ β†’ 𝑃 ∈ β„•)
115114nnnn0d 12536 . . . 4 (πœ‘ β†’ 𝑃 ∈ β„•0)
116 zsqcl 14098 . . . . 5 ((β—‘πΊβ€˜(πΏβ€˜π΄)) ∈ β„€ β†’ ((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) ∈ β„€)
117102, 116syl 17 . . . 4 (πœ‘ β†’ ((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) ∈ β„€)
1181, 11zndvds 21324 . . . 4 ((𝑃 ∈ β„•0 ∧ ((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) ∈ β„€ ∧ 𝐴 ∈ β„€) β†’ ((πΏβ€˜((β—‘πΊβ€˜(πΏβ€˜π΄))↑2)) = (πΏβ€˜π΄) ↔ 𝑃 βˆ₯ (((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) βˆ’ 𝐴)))
119115, 117, 98, 118syl3anc 1369 . . 3 (πœ‘ β†’ ((πΏβ€˜((β—‘πΊβ€˜(πΏβ€˜π΄))↑2)) = (πΏβ€˜π΄) ↔ 𝑃 βˆ₯ (((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) βˆ’ 𝐴)))
120112, 119mpbid 231 . 2 (πœ‘ β†’ 𝑃 βˆ₯ (((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) βˆ’ 𝐴))
121 oveq1 7418 . . . . 5 (π‘₯ = (β—‘πΊβ€˜(πΏβ€˜π΄)) β†’ (π‘₯↑2) = ((β—‘πΊβ€˜(πΏβ€˜π΄))↑2))
122121oveq1d 7426 . . . 4 (π‘₯ = (β—‘πΊβ€˜(πΏβ€˜π΄)) β†’ ((π‘₯↑2) βˆ’ 𝐴) = (((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) βˆ’ 𝐴))
123122breq2d 5159 . . 3 (π‘₯ = (β—‘πΊβ€˜(πΏβ€˜π΄)) β†’ (𝑃 βˆ₯ ((π‘₯↑2) βˆ’ 𝐴) ↔ 𝑃 βˆ₯ (((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) βˆ’ 𝐴)))
124123rspcev 3611 . 2 (((β—‘πΊβ€˜(πΏβ€˜π΄)) ∈ β„€ ∧ 𝑃 βˆ₯ (((β—‘πΊβ€˜(πΏβ€˜π΄))↑2) βˆ’ 𝐴)) β†’ βˆƒπ‘₯ ∈ β„€ 𝑃 βˆ₯ ((π‘₯↑2) βˆ’ 𝐴))
125102, 120, 124syl2anc 582 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ β„€ 𝑃 βˆ₯ ((π‘₯↑2) βˆ’ 𝐴))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆƒwrex 3068  Vcvv 3472   βˆ– cdif 3944  {csn 4627   class class class wbr 5147   ↦ cmpt 5230  β—‘ccnv 5674   β€œ cima 5678  βŸΆwf 6538  β€“1-1β†’wf1 6539  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  (class class class)co 7411   β‰ˆ cen 8938   β‰Ό cdom 8939  Fincfn 8941  0cc0 11112  1c1 11113   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448   / cdiv 11875  β„•cn 12216  2c2 12271  β„•0cn0 12476  β„€cz 12562  ...cfz 13488  β†‘cexp 14031  β™―chash 14294   βˆ₯ cdvds 16201  β„™cprime 16612  Basecbs 17148  0gc0g 17389  Mndcmnd 18659  Grpcgrp 18855  -gcsg 18857  .gcmg 18986  mulGrpcmgp 20028  1rcur 20075  Ringcrg 20127  CRingccrg 20128  NzRingcnzr 20403  Fieldcfield 20501  Domncdomn 21096  IDomncidom 21097  β„€RHomczrh 21268  β„€/nβ„€czn 21271  algSccascl 21626  var1cv1 21919  Poly1cpl1 21920  eval1ce1 22053   deg1 cdg1 25804   /L clgs 27033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-ofr 7673  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-er 8705  df-ec 8707  df-qs 8711  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-xnn0 12549  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-hash 14295  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-dvds 16202  df-gcd 16440  df-prm 16613  df-phi 16703  df-pc 16774  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-hom 17225  df-cco 17226  df-0g 17391  df-gsum 17392  df-prds 17397  df-pws 17399  df-imas 17458  df-qus 17459  df-mre 17534  df-mrc 17535  df-acs 17537  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-mhm 18705  df-submnd 18706  df-grp 18858  df-minusg 18859  df-sbg 18860  df-mulg 18987  df-subg 19039  df-nsg 19040  df-eqg 19041  df-ghm 19128  df-cntz 19222  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-srg 20081  df-ring 20129  df-cring 20130  df-oppr 20225  df-dvdsr 20248  df-unit 20249  df-invr 20279  df-dvr 20292  df-rhm 20363  df-nzr 20404  df-subrng 20434  df-subrg 20459  df-drng 20502  df-field 20503  df-lmod 20616  df-lss 20687  df-lsp 20727  df-sra 20930  df-rgmod 20931  df-lidl 20932  df-rsp 20933  df-2idl 21006  df-rlreg 21099  df-domn 21100  df-idom 21101  df-cnfld 21145  df-zring 21218  df-zrh 21272  df-zn 21275  df-assa 21627  df-asp 21628  df-ascl 21629  df-psr 21681  df-mvr 21682  df-mpl 21683  df-opsr 21685  df-evls 21854  df-evl 21855  df-psr1 21923  df-vr1 21924  df-ply1 21925  df-coe1 21926  df-evl1 22055  df-mdeg 25805  df-deg1 25806  df-mon1 25883  df-uc1p 25884  df-q1p 25885  df-r1p 25886  df-lgs 27034
This theorem is referenced by:  lgsqrlem5  27089
  Copyright terms: Public domain W3C validator