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	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
40	35 39	syl	$⊢ φ \to {mulGrp}_{S} \in Mnd$
41		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
42	12 41	syl	$⊢ φ \to \frac{P - 1}{2} \in ℕ$
43	42	nnnn0d	$⊢ φ \to \frac{P - 1}{2} \in ℕ_{0}$
44	7 2 3	vr1cl	$⊢ Y \in Ring \to X \in B$
45	33 44	syl	$⊢ φ \to X \in B$
46	38 3	mgpbas	$⊢ B = {Base}_{{mulGrp}_{S}}$
47	46 6	mulgnn0cl	$⊢ ({mulGrp}_{S} \in Mnd \land \frac{P - 1}{2} \in ℕ_{0} \land X \in B) \to (\frac{P - 1}{2}) \underset{˙}{\times} X \in B$
48	40 43 45 47	syl3anc	$⊢ φ \to (\frac{P - 1}{2}) \underset{˙}{\times} X \in B$
49	3 9	ringidcl	$⊢ S \in Ring \to \underset{˙}{1} \in B$
50	35 49	syl	$⊢ φ \to \underset{˙}{1} \in B$
51	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$
52	37 48 50 51	syl3anc	$⊢ φ \to ((\frac{P - 1}{2}) \underset{˙}{\times} X) \underset{˙}{-} \underset{˙}{1} \in B$
53	10 52	eqeltrid	$⊢ φ \to T \in B$
54	10	fveq2i	$⊢ D (T) = D (((\frac{P - 1}{2}) \underset{˙}{\times} X) \underset{˙}{-} \underset{˙}{1})$
55	42	nngt0d	$⊢ φ \to 0 < \frac{P - 1}{2}$
56		eqid	$⊢ algSc (S) = algSc (S)$
57		eqid	$⊢ 1_{Y} = 1_{Y}$
58	2 56 57 9	ply1scl1	$⊢ Y \in Ring \to algSc (S) (1_{Y}) = \underset{˙}{1}$
59	33 58	syl	$⊢ φ \to algSc (S) (1_{Y}) = \underset{˙}{1}$
60	59	fveq2d	$⊢ φ \to D (algSc (S) (1_{Y})) = D (\underset{˙}{1})$
61		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
62	61 57	ringidcl	$⊢ Y \in Ring \to 1_{Y} \in {Base}_{Y}$
63	33 62	syl	$⊢ φ \to 1_{Y} \in {Base}_{Y}$
64		domnnzr	$⊢ Y \in Domn \to Y \in NzRing$
65	29 64	simplbiim	$⊢ Y \in IDomn \to Y \in NzRing$
66	28 65	syl	$⊢ φ \to Y \in NzRing$
67	57 22	nzrnz	$⊢ Y \in NzRing \to 1_{Y} \neq 0_{Y}$
68	66 67	syl	$⊢ φ \to 1_{Y} \neq 0_{Y}$
69	4 2 61 56 22	deg1scl	$⊢ (Y \in Ring \land 1_{Y} \in {Base}_{Y} \land 1_{Y} \neq 0_{Y}) \to D (algSc (S) (1_{Y})) = 0$
70	33 63 68 69	syl3anc	$⊢ φ \to D (algSc (S) (1_{Y})) = 0$
71	60 70	eqtr3d	$⊢ φ \to D (\underset{˙}{1}) = 0$
72	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}$
73	66 43 72	syl2anc	$⊢ φ \to D ((\frac{P - 1}{2}) \underset{˙}{\times} X) = \frac{P - 1}{2}$
74	55 71 73	3brtr4d	$⊢ φ \to D (\underset{˙}{1}) < D ((\frac{P - 1}{2}) \underset{˙}{\times} X)$
75	2 4 33 3 8 48 50 74	deg1sub	$⊢ φ \to D (((\frac{P - 1}{2}) \underset{˙}{\times} X) \underset{˙}{-} \underset{˙}{1}) = D ((\frac{P - 1}{2}) \underset{˙}{\times} X)$
76	54 75	syl5eq	$⊢ φ \to D (T) = D ((\frac{P - 1}{2}) \underset{˙}{\times} X)$
77	76 73	eqtrd	$⊢ φ \to D (T) = \frac{P - 1}{2}$
78	77 43	eqeltrd	$⊢ φ \to D (T) \in ℕ_{0}$
79	4 2 23 3	deg1nn0clb	$⊢ (Y \in Ring \land T \in B) \to (T \neq 0_{S} \leftrightarrow D (T) \in ℕ_{0})$
80	33 53 79	syl2anc	$⊢ φ \to (T \neq 0_{S} \leftrightarrow D (T) \in ℕ_{0})$
81	78 80	mpbird	$⊢ φ \to T \neq 0_{S}$
82	2 3 4 5 22 23 28 53 81	fta1g	$⊢ φ \to \|{O (T)}^{-1} [\{0_{Y}\}]\| \leq D (T)$
83	82 77	breqtrd	$⊢ φ \to \|{O (T)}^{-1} [\{0_{Y}\}]\| \leq \frac{P - 1}{2}$
84		hashfz1	$⊢ \frac{P - 1}{2} \in ℕ_{0} \to \|(1 \dots \frac{P - 1}{2})\| = \frac{P - 1}{2}$
85	43 84	syl	$⊢ φ \to \|(1 \dots \frac{P - 1}{2})\| = \frac{P - 1}{2}$
86	83 85	breqtrrd	$⊢ φ \to \|{O (T)}^{-1} [\{0_{Y}\}]\| \leq \|(1 \dots \frac{P - 1}{2})\|$
87		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$
88	19 43 83 87	mp3an2i	$⊢ φ \to {O (T)}^{-1} [\{0_{Y}\}] \in Fin$
89		fzfid	$⊢ φ \to (1 \dots \frac{P - 1}{2}) \in Fin$
90		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}))$
91	88 89 90	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}))$
92	86 91	mpbid	$⊢ φ \to {O (T)}^{-1} [\{0_{Y}\}] ≼ (1 \dots \frac{P - 1}{2})$
93		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}\}]$
94	21 92 93	syl2anc	$⊢ φ \to (1 \dots \frac{P - 1}{2}) \approx {O (T)}^{-1} [\{0_{Y}\}]$
95		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}\}])$
96	94 88 95	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}\}])$
97	16 96	mpbid	$⊢ φ \to G : (1 \dots \frac{P - 1}{2}) \underset{1-1 onto}{⟶} {O (T)}^{-1} [\{0_{Y}\}]$
98		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})$
99		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})$
100	97 98 99	3syl	$⊢ φ \to G^{-1} : {O (T)}^{-1} [\{0_{Y}\}] ⟶ (1 \dots \frac{P - 1}{2})$
101	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}\}]$
102	100 101	ffvelrnd	$⊢ φ \to G^{-1} (L (A)) \in (1 \dots \frac{P - 1}{2})$
103		elfzelz	$⊢ G^{-1} (L (A)) \in (1 \dots \frac{P - 1}{2}) \to G^{-1} (L (A)) \in ℤ$
104	102 103	syl	$⊢ φ \to G^{-1} (L (A)) \in ℤ$
105		fvoveq1	$⊢ x = G^{-1} (L (A)) \to L (x^{2}) = L ({G^{-1} (L (A))}^{2})$
106		fvoveq1	$⊢ y = x \to L (y^{2}) = L (x^{2})$
107	106	cbvmptv	$⊢ (y \in (1 \dots \frac{P - 1}{2}) ⟼ L (y^{2})) = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (x^{2}))$
108	13 107	eqtri	$⊢ G = (x \in (1 \dots \frac{P - 1}{2}) ⟼ L (x^{2}))$
109		fvex	$⊢ L ({G^{-1} (L (A))}^{2}) \in V$
110	105 108 109	fvmpt	$⊢ G^{-1} (L (A)) \in (1 \dots \frac{P - 1}{2}) \to G (G^{-1} (L (A))) = L ({G^{-1} (L (A))}^{2})$
111	102 110	syl	$⊢ φ \to G (G^{-1} (L (A))) = L ({G^{-1} (L (A))}^{2})$
112		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)$
113	97 101 112	syl2anc	$⊢ φ \to G (G^{-1} (L (A))) = L (A)$
114	111 113	eqtr3d	$⊢ φ \to L ({G^{-1} (L (A))}^{2}) = L (A)$
115		prmnn	$⊢ P \in ℙ \to P \in ℕ$
116	24 115	syl	$⊢ φ \to P \in ℕ$
117	116	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
118		zsqcl	$⊢ G^{-1} (L (A)) \in ℤ \to {G^{-1} (L (A))}^{2} \in ℤ$
119	104 118	syl	$⊢ φ \to {G^{-1} (L (A))}^{2} \in ℤ$
120	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))$
121	117 119 14 120	syl3anc	$⊢ φ \to (L ({G^{-1} (L (A))}^{2}) = L (A) \leftrightarrow P ∥ ({G^{-1} (L (A))}^{2} - A))$
122	114 121	mpbid	$⊢ φ \to P ∥ ({G^{-1} (L (A))}^{2} - A)$
123		oveq1	$⊢ x = G^{-1} (L (A)) \to x^{2} = {G^{-1} (L (A))}^{2}$
124	123	oveq1d	$⊢ x = G^{-1} (L (A)) \to x^{2} - A = {G^{-1} (L (A))}^{2} - A$
125	124	breq2d	$⊢ x = G^{-1} (L (A)) \to (P ∥ (x^{2} - A) \leftrightarrow P ∥ ({G^{-1} (L (A))}^{2} - A))$
126	125	rspcev	$⊢ (G^{-1} (L (A)) \in ℤ \land P ∥ ({G^{-1} (L (A))}^{2} - A)) \to \exists x \in ℤ P ∥ (x^{2} - A)$
127	104 122 126	syl2anc	$⊢ φ \to \exists x \in ℤ P ∥ (x^{2} - A)$

Metamath Proof Explorer

Theorem lgsqrlem4

Proof