# Metamath Proof Explorer

## Theorem lgsqrlem4

Description: Lemma for lgsqr . (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses lgsqr.y ${⊢}{Y}=ℤ/{P}ℤ$
lgsqr.s ${⊢}{S}={\mathrm{Poly}}_{1}\left({Y}\right)$
lgsqr.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
lgsqr.d ${⊢}{D}={\mathrm{deg}}_{1}\left({Y}\right)$
lgsqr.o ${⊢}{O}={\mathrm{eval}}_{1}\left({Y}\right)$
lgsqr.e
lgsqr.x ${⊢}{X}={\mathrm{var}}_{1}\left({Y}\right)$
lgsqr.m
lgsqr.u
lgsqr.t
lgsqr.l ${⊢}{L}=\mathrm{ℤRHom}\left({Y}\right)$
lgsqr.1 ${⊢}{\phi }\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
lgsqr.g ${⊢}{G}=\left({y}\in \left(1\dots \frac{{P}-1}{2}\right)⟼{L}\left({{y}}^{2}\right)\right)$
lgsqr.3 ${⊢}{\phi }\to {A}\in ℤ$
lgsqr.4 ${⊢}{\phi }\to {A}{/}_{L}{P}=1$
Assertion lgsqrlem4 ${⊢}{\phi }\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\parallel \left({{x}}^{2}-{A}\right)$

### Proof

Step Hyp Ref Expression
1 lgsqr.y ${⊢}{Y}=ℤ/{P}ℤ$
2 lgsqr.s ${⊢}{S}={\mathrm{Poly}}_{1}\left({Y}\right)$
3 lgsqr.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
4 lgsqr.d ${⊢}{D}={\mathrm{deg}}_{1}\left({Y}\right)$
5 lgsqr.o ${⊢}{O}={\mathrm{eval}}_{1}\left({Y}\right)$
6 lgsqr.e
7 lgsqr.x ${⊢}{X}={\mathrm{var}}_{1}\left({Y}\right)$
8 lgsqr.m
9 lgsqr.u
10 lgsqr.t
11 lgsqr.l ${⊢}{L}=\mathrm{ℤRHom}\left({Y}\right)$
12 lgsqr.1 ${⊢}{\phi }\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
13 lgsqr.g ${⊢}{G}=\left({y}\in \left(1\dots \frac{{P}-1}{2}\right)⟼{L}\left({{y}}^{2}\right)\right)$
14 lgsqr.3 ${⊢}{\phi }\to {A}\in ℤ$
15 lgsqr.4 ${⊢}{\phi }\to {A}{/}_{L}{P}=1$
16 1 2 3 4 5 6 7 8 9 10 11 12 13 lgsqrlem2 ${⊢}{\phi }\to {G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]$
17 fvex ${⊢}{O}\left({T}\right)\in \mathrm{V}$
18 17 cnvex ${⊢}{{O}\left({T}\right)}^{-1}\in \mathrm{V}$
19 18 imaex ${⊢}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\in \mathrm{V}$
20 19 f1dom ${⊢}{G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\to \left(1\dots \frac{{P}-1}{2}\right)\preccurlyeq {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]$
21 16 20 syl ${⊢}{\phi }\to \left(1\dots \frac{{P}-1}{2}\right)\preccurlyeq {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]$
22 eqid ${⊢}{0}_{{Y}}={0}_{{Y}}$
23 eqid ${⊢}{0}_{{S}}={0}_{{S}}$
24 12 eldifad ${⊢}{\phi }\to {P}\in ℙ$
25 1 znfld ${⊢}{P}\in ℙ\to {Y}\in \mathrm{Field}$
26 24 25 syl ${⊢}{\phi }\to {Y}\in \mathrm{Field}$
27 fldidom ${⊢}{Y}\in \mathrm{Field}\to {Y}\in \mathrm{IDomn}$
28 26 27 syl ${⊢}{\phi }\to {Y}\in \mathrm{IDomn}$
29 isidom ${⊢}{Y}\in \mathrm{IDomn}↔\left({Y}\in \mathrm{CRing}\wedge {Y}\in \mathrm{Domn}\right)$
30 29 simplbi ${⊢}{Y}\in \mathrm{IDomn}\to {Y}\in \mathrm{CRing}$
31 28 30 syl ${⊢}{\phi }\to {Y}\in \mathrm{CRing}$
32 crngring ${⊢}{Y}\in \mathrm{CRing}\to {Y}\in \mathrm{Ring}$
33 31 32 syl ${⊢}{\phi }\to {Y}\in \mathrm{Ring}$
34 2 ply1ring ${⊢}{Y}\in \mathrm{Ring}\to {S}\in \mathrm{Ring}$
35 33 34 syl ${⊢}{\phi }\to {S}\in \mathrm{Ring}$
36 ringgrp ${⊢}{S}\in \mathrm{Ring}\to {S}\in \mathrm{Grp}$
37 35 36 syl ${⊢}{\phi }\to {S}\in \mathrm{Grp}$
38 eqid ${⊢}{\mathrm{mulGrp}}_{{S}}={\mathrm{mulGrp}}_{{S}}$
39 38 ringmgp ${⊢}{S}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{S}}\in \mathrm{Mnd}$
40 35 39 syl ${⊢}{\phi }\to {\mathrm{mulGrp}}_{{S}}\in \mathrm{Mnd}$
41 oddprm ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)\to \frac{{P}-1}{2}\in ℕ$
42 12 41 syl ${⊢}{\phi }\to \frac{{P}-1}{2}\in ℕ$
43 42 nnnn0d ${⊢}{\phi }\to \frac{{P}-1}{2}\in {ℕ}_{0}$
44 7 2 3 vr1cl ${⊢}{Y}\in \mathrm{Ring}\to {X}\in {B}$
45 33 44 syl ${⊢}{\phi }\to {X}\in {B}$
46 38 3 mgpbas ${⊢}{B}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{S}}}$
47 46 6 mulgnn0cl
48 40 43 45 47 syl3anc
49 3 9 ringidcl
50 35 49 syl
51 3 8 grpsubcl
52 37 48 50 51 syl3anc
53 10 52 eqeltrid ${⊢}{\phi }\to {T}\in {B}$
54 10 fveq2i
55 42 nngt0d ${⊢}{\phi }\to 0<\frac{{P}-1}{2}$
56 eqid ${⊢}\mathrm{algSc}\left({S}\right)=\mathrm{algSc}\left({S}\right)$
57 eqid ${⊢}{1}_{{Y}}={1}_{{Y}}$
58 2 56 57 9 ply1scl1
59 33 58 syl
60 59 fveq2d
61 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
62 61 57 ringidcl ${⊢}{Y}\in \mathrm{Ring}\to {1}_{{Y}}\in {\mathrm{Base}}_{{Y}}$
63 33 62 syl ${⊢}{\phi }\to {1}_{{Y}}\in {\mathrm{Base}}_{{Y}}$
64 domnnzr ${⊢}{Y}\in \mathrm{Domn}\to {Y}\in \mathrm{NzRing}$
65 29 64 simplbiim ${⊢}{Y}\in \mathrm{IDomn}\to {Y}\in \mathrm{NzRing}$
66 28 65 syl ${⊢}{\phi }\to {Y}\in \mathrm{NzRing}$
67 57 22 nzrnz ${⊢}{Y}\in \mathrm{NzRing}\to {1}_{{Y}}\ne {0}_{{Y}}$
68 66 67 syl ${⊢}{\phi }\to {1}_{{Y}}\ne {0}_{{Y}}$
69 4 2 61 56 22 deg1scl ${⊢}\left({Y}\in \mathrm{Ring}\wedge {1}_{{Y}}\in {\mathrm{Base}}_{{Y}}\wedge {1}_{{Y}}\ne {0}_{{Y}}\right)\to {D}\left(\mathrm{algSc}\left({S}\right)\left({1}_{{Y}}\right)\right)=0$
70 33 63 68 69 syl3anc ${⊢}{\phi }\to {D}\left(\mathrm{algSc}\left({S}\right)\left({1}_{{Y}}\right)\right)=0$
71 60 70 eqtr3d
72 4 2 7 38 6 deg1pw
73 66 43 72 syl2anc
74 55 71 73 3brtr4d
75 2 4 33 3 8 48 50 74 deg1sub
76 54 75 syl5eq
77 76 73 eqtrd ${⊢}{\phi }\to {D}\left({T}\right)=\frac{{P}-1}{2}$
78 77 43 eqeltrd ${⊢}{\phi }\to {D}\left({T}\right)\in {ℕ}_{0}$
79 4 2 23 3 deg1nn0clb ${⊢}\left({Y}\in \mathrm{Ring}\wedge {T}\in {B}\right)\to \left({T}\ne {0}_{{S}}↔{D}\left({T}\right)\in {ℕ}_{0}\right)$
80 33 53 79 syl2anc ${⊢}{\phi }\to \left({T}\ne {0}_{{S}}↔{D}\left({T}\right)\in {ℕ}_{0}\right)$
81 78 80 mpbird ${⊢}{\phi }\to {T}\ne {0}_{{S}}$
82 2 3 4 5 22 23 28 53 81 fta1g ${⊢}{\phi }\to \left|{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right|\le {D}\left({T}\right)$
83 82 77 breqtrd ${⊢}{\phi }\to \left|{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right|\le \frac{{P}-1}{2}$
84 hashfz1 ${⊢}\frac{{P}-1}{2}\in {ℕ}_{0}\to \left|\left(1\dots \frac{{P}-1}{2}\right)\right|=\frac{{P}-1}{2}$
85 43 84 syl ${⊢}{\phi }\to \left|\left(1\dots \frac{{P}-1}{2}\right)\right|=\frac{{P}-1}{2}$
86 83 85 breqtrrd ${⊢}{\phi }\to \left|{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right|\le \left|\left(1\dots \frac{{P}-1}{2}\right)\right|$
87 hashbnd ${⊢}\left({{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\in \mathrm{V}\wedge \frac{{P}-1}{2}\in {ℕ}_{0}\wedge \left|{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right|\le \frac{{P}-1}{2}\right)\to {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\in \mathrm{Fin}$
88 19 43 83 87 mp3an2i ${⊢}{\phi }\to {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\in \mathrm{Fin}$
89 fzfid ${⊢}{\phi }\to \left(1\dots \frac{{P}-1}{2}\right)\in \mathrm{Fin}$
90 hashdom ${⊢}\left({{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\in \mathrm{Fin}\wedge \left(1\dots \frac{{P}-1}{2}\right)\in \mathrm{Fin}\right)\to \left(\left|{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right|\le \left|\left(1\dots \frac{{P}-1}{2}\right)\right|↔{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\preccurlyeq \left(1\dots \frac{{P}-1}{2}\right)\right)$
91 88 89 90 syl2anc ${⊢}{\phi }\to \left(\left|{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right|\le \left|\left(1\dots \frac{{P}-1}{2}\right)\right|↔{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\preccurlyeq \left(1\dots \frac{{P}-1}{2}\right)\right)$
92 86 91 mpbid ${⊢}{\phi }\to {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\preccurlyeq \left(1\dots \frac{{P}-1}{2}\right)$
93 sbth ${⊢}\left(\left(1\dots \frac{{P}-1}{2}\right)\preccurlyeq {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\wedge {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\preccurlyeq \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(1\dots \frac{{P}-1}{2}\right)\approx {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]$
94 21 92 93 syl2anc ${⊢}{\phi }\to \left(1\dots \frac{{P}-1}{2}\right)\approx {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]$
95 f1finf1o ${⊢}\left(\left(1\dots \frac{{P}-1}{2}\right)\approx {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\wedge {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\in \mathrm{Fin}\right)\to \left({G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]↔{G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right)$
96 94 88 95 syl2anc ${⊢}{\phi }\to \left({G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]↔{G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right)$
97 16 96 mpbid ${⊢}{\phi }\to {G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]$
98 f1ocnv ${⊢}{G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\to {{G}}^{-1}:{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\underset{1-1 onto}{⟶}\left(1\dots \frac{{P}-1}{2}\right)$
99 f1of ${⊢}{{G}}^{-1}:{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\underset{1-1 onto}{⟶}\left(1\dots \frac{{P}-1}{2}\right)\to {{G}}^{-1}:{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]⟶\left(1\dots \frac{{P}-1}{2}\right)$
100 97 98 99 3syl ${⊢}{\phi }\to {{G}}^{-1}:{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]⟶\left(1\dots \frac{{P}-1}{2}\right)$
101 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 lgsqrlem3 ${⊢}{\phi }\to {L}\left({A}\right)\in {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]$
102 100 101 ffvelrnd ${⊢}{\phi }\to {{G}}^{-1}\left({L}\left({A}\right)\right)\in \left(1\dots \frac{{P}-1}{2}\right)$
103 elfzelz ${⊢}{{G}}^{-1}\left({L}\left({A}\right)\right)\in \left(1\dots \frac{{P}-1}{2}\right)\to {{G}}^{-1}\left({L}\left({A}\right)\right)\in ℤ$
104 102 103 syl ${⊢}{\phi }\to {{G}}^{-1}\left({L}\left({A}\right)\right)\in ℤ$
105 fvoveq1 ${⊢}{x}={{G}}^{-1}\left({L}\left({A}\right)\right)\to {L}\left({{x}}^{2}\right)={L}\left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\right)$
106 fvoveq1 ${⊢}{y}={x}\to {L}\left({{y}}^{2}\right)={L}\left({{x}}^{2}\right)$
107 106 cbvmptv ${⊢}\left({y}\in \left(1\dots \frac{{P}-1}{2}\right)⟼{L}\left({{y}}^{2}\right)\right)=\left({x}\in \left(1\dots \frac{{P}-1}{2}\right)⟼{L}\left({{x}}^{2}\right)\right)$
108 13 107 eqtri ${⊢}{G}=\left({x}\in \left(1\dots \frac{{P}-1}{2}\right)⟼{L}\left({{x}}^{2}\right)\right)$
109 fvex ${⊢}{L}\left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\right)\in \mathrm{V}$
110 105 108 109 fvmpt ${⊢}{{G}}^{-1}\left({L}\left({A}\right)\right)\in \left(1\dots \frac{{P}-1}{2}\right)\to {G}\left({{G}}^{-1}\left({L}\left({A}\right)\right)\right)={L}\left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\right)$
111 102 110 syl ${⊢}{\phi }\to {G}\left({{G}}^{-1}\left({L}\left({A}\right)\right)\right)={L}\left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\right)$
112 f1ocnvfv2 ${⊢}\left({G}:\left(1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}{{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\wedge {L}\left({A}\right)\in {{O}\left({T}\right)}^{-1}\left[\left\{{0}_{{Y}}\right\}\right]\right)\to {G}\left({{G}}^{-1}\left({L}\left({A}\right)\right)\right)={L}\left({A}\right)$
113 97 101 112 syl2anc ${⊢}{\phi }\to {G}\left({{G}}^{-1}\left({L}\left({A}\right)\right)\right)={L}\left({A}\right)$
114 111 113 eqtr3d ${⊢}{\phi }\to {L}\left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\right)={L}\left({A}\right)$
115 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
116 24 115 syl ${⊢}{\phi }\to {P}\in ℕ$
117 116 nnnn0d ${⊢}{\phi }\to {P}\in {ℕ}_{0}$
118 zsqcl ${⊢}{{G}}^{-1}\left({L}\left({A}\right)\right)\in ℤ\to {{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\in ℤ$
119 104 118 syl ${⊢}{\phi }\to {{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\in ℤ$
120 1 11 zndvds ${⊢}\left({P}\in {ℕ}_{0}\wedge {{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\in ℤ\wedge {A}\in ℤ\right)\to \left({L}\left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\right)={L}\left({A}\right)↔{P}\parallel \left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}-{A}\right)\right)$
121 117 119 14 120 syl3anc ${⊢}{\phi }\to \left({L}\left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}\right)={L}\left({A}\right)↔{P}\parallel \left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}-{A}\right)\right)$
122 114 121 mpbid ${⊢}{\phi }\to {P}\parallel \left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}-{A}\right)$
123 oveq1 ${⊢}{x}={{G}}^{-1}\left({L}\left({A}\right)\right)\to {{x}}^{2}={{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}$
124 123 oveq1d ${⊢}{x}={{G}}^{-1}\left({L}\left({A}\right)\right)\to {{x}}^{2}-{A}={{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}-{A}$
125 124 breq2d ${⊢}{x}={{G}}^{-1}\left({L}\left({A}\right)\right)\to \left({P}\parallel \left({{x}}^{2}-{A}\right)↔{P}\parallel \left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}-{A}\right)\right)$
126 125 rspcev ${⊢}\left({{G}}^{-1}\left({L}\left({A}\right)\right)\in ℤ\wedge {P}\parallel \left({{{G}}^{-1}\left({L}\left({A}\right)\right)}^{2}-{A}\right)\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\parallel \left({{x}}^{2}-{A}\right)$
127 104 122 126 syl2anc ${⊢}{\phi }\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\parallel \left({{x}}^{2}-{A}\right)$