lgsqrlem4

	Ref	Expression
Hypotheses	lgsqr.y	$⊢ Y = ℤ / P ℤ$
	lgsqr.s	$⊢ S = {Poly}_{1} (Y)$
	lgsqr.b	$⊢ B = {Base}_{S}$
	lgsqr.d	$⊢ D = \deg_{1} (Y)$
	lgsqr.o	$⊢ O = {eval}_{1} (Y)$
	lgsqr.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{S}}$
	lgsqr.x	$⊢ X = {var}_{1} (Y)$
	lgsqr.m	$⊢ \underset{˙}{-} = -_{S}$
	lgsqr.u	$⊢ \underset{˙}{1} = 1_{S}$
	lgsqr.t	$⊢ T = ((\frac{P - 1}{2}) \underset{˙}{\times} X) \underset{˙}{-} \underset{˙}{1}$
	lgsqr.l	$⊢ L = ℤRHom (Y)$
	lgsqr.1	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	lgsqr.g	$⊢ G = (y \in (1 \dots \frac{P - 1}{2}) ⟼ L (y^{2}))$
	lgsqr.3	$⊢ φ \to A \in ℤ$
	lgsqr.4	$⊢ φ \to A /_{L} P = 1$
Assertion	lgsqrlem4	$⊢ φ \to \exists x \in ℤ P ∥ (x^{2} - A)$

Proof

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

Metamath Proof Explorer

Theorem lgsqrlem4

Proof