lgsqrlem2

	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}))$
Assertion	lgsqrlem2	$⊢ φ \to G : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} {O (T)}^{-1} [\{0_{Y}\}]$

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	12	eldifad	$⊢ φ \to P \in ℙ$
15	1	znfld	$⊢ P \in ℙ \to Y \in Field$
16	14 15	syl	$⊢ φ \to Y \in Field$
17		fldidom	$⊢ Y \in Field \to Y \in IDomn$
18	16 17	syl	$⊢ φ \to Y \in IDomn$
19		isidom	$⊢ Y \in IDomn \leftrightarrow (Y \in CRing \land Y \in Domn)$
20	19	simplbi	$⊢ Y \in IDomn \to Y \in CRing$
21	18 20	syl	$⊢ φ \to Y \in CRing$
22		crngring	$⊢ Y \in CRing \to Y \in Ring$
23	21 22	syl	$⊢ φ \to Y \in Ring$
24	11	zrhrhm	$⊢ Y \in Ring \to L \in (ℤ_{ring} RingHom Y)$
25	23 24	syl	$⊢ φ \to L \in (ℤ_{ring} RingHom Y)$
26		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
27		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
28	26 27	rhmf	$⊢ L \in (ℤ_{ring} RingHom Y) \to L : ℤ ⟶ {Base}_{Y}$
29	25 28	syl	$⊢ φ \to L : ℤ ⟶ {Base}_{Y}$
30	29	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to L : ℤ ⟶ {Base}_{Y}$
31		elfzelz	$⊢ y \in (1 \dots \frac{P - 1}{2}) \to y \in ℤ$
32	31	adantl	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \in ℤ$
33		zsqcl	$⊢ y \in ℤ \to y^{2} \in ℤ$
34	32 33	syl	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y^{2} \in ℤ$
35	30 34	ffvelcdmd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to L (y^{2}) \in {Base}_{Y}$
36	12	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to P \in (ℙ ∖ \{2\})$
37		elfznn	$⊢ y \in (1 \dots \frac{P - 1}{2}) \to y \in ℕ$
38	37	adantl	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \in ℕ$
39	38	nncnd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \in ℂ$
40		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
41	12 40	syl	$⊢ φ \to \frac{P - 1}{2} \in ℕ$
42	41	nnnn0d	$⊢ φ \to \frac{P - 1}{2} \in ℕ_{0}$
43	42	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} \in ℕ_{0}$
44		2nn0	$⊢ 2 \in ℕ_{0}$
45	44	a1i	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to 2 \in ℕ_{0}$
46	39 43 45	expmuld	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y^{2 (\frac{P - 1}{2})} = {(y^{2})}^{\frac{P - 1}{2}}$
47		prmnn	$⊢ P \in ℙ \to P \in ℕ$
48	14 47	syl	$⊢ φ \to P \in ℕ$
49	48	nnred	$⊢ φ \to P \in ℝ$
50		peano2rem	$⊢ P \in ℝ \to P - 1 \in ℝ$
51	49 50	syl	$⊢ φ \to P - 1 \in ℝ$
52	51	recnd	$⊢ φ \to P - 1 \in ℂ$
53		2cnd	$⊢ φ \to 2 \in ℂ$
54		2ne0	$⊢ 2 \neq 0$
55	54	a1i	$⊢ φ \to 2 \neq 0$
56	52 53 55	divcan2d	$⊢ φ \to 2 (\frac{P - 1}{2}) = P - 1$
57		phiprm	$⊢ P \in ℙ \to ϕ (P) = P - 1$
58	14 57	syl	$⊢ φ \to ϕ (P) = P - 1$
59	56 58	eqtr4d	$⊢ φ \to 2 (\frac{P - 1}{2}) = ϕ (P)$
60	59	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to 2 (\frac{P - 1}{2}) = ϕ (P)$
61	60	oveq2d	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y^{2 (\frac{P - 1}{2})} = y^{ϕ (P)}$
62	46 61	eqtr3d	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to {(y^{2})}^{\frac{P - 1}{2}} = y^{ϕ (P)}$
63	62	oveq1d	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to {(y^{2})}^{\frac{P - 1}{2}} \mod P = y^{ϕ (P)} \mod P$
64	14	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to P \in ℙ$
65	64 47	syl	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to P \in ℕ$
66	48	nnzd	$⊢ φ \to P \in ℤ$
67	66	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to P \in ℤ$
68	32 67	gcdcomd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \gcd P = P \gcd y$
69	38	nnred	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \in ℝ$
70	51	rehalfcld	$⊢ φ \to \frac{P - 1}{2} \in ℝ$
71	70	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} \in ℝ$
72	49	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to P \in ℝ$
73		elfzle2	$⊢ y \in (1 \dots \frac{P - 1}{2}) \to y \leq \frac{P - 1}{2}$
74	73	adantl	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \leq \frac{P - 1}{2}$
75		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
76	14 75	syl	$⊢ φ \to P \in ℤ_{\geq 2}$
77		uz2m1nn	$⊢ P \in ℤ_{\geq 2} \to P - 1 \in ℕ$
78	76 77	syl	$⊢ φ \to P - 1 \in ℕ$
79	78	nnrpd	$⊢ φ \to P - 1 \in ℝ^{+}$
80		rphalflt	$⊢ P - 1 \in ℝ^{+} \to \frac{P - 1}{2} < P - 1$
81	79 80	syl	$⊢ φ \to \frac{P - 1}{2} < P - 1$
82	49	ltm1d	$⊢ φ \to P - 1 < P$
83	70 51 49 81 82	lttrd	$⊢ φ \to \frac{P - 1}{2} < P$
84	83	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} < P$
85	69 71 72 74 84	lelttrd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y < P$
86	69 72	ltnled	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to (y < P \leftrightarrow \neg P \leq y)$
87	85 86	mpbid	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \neg P \leq y$
88		dvdsle	$⊢ (P \in ℤ \land y \in ℕ) \to (P ∥ y \to P \leq y)$
89	67 38 88	syl2anc	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to (P ∥ y \to P \leq y)$
90	87 89	mtod	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ y$
91		coprm	$⊢ (P \in ℙ \land y \in ℤ) \to (\neg P ∥ y \leftrightarrow P \gcd y = 1)$
92	64 32 91	syl2anc	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to (\neg P ∥ y \leftrightarrow P \gcd y = 1)$
93	90 92	mpbid	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to P \gcd y = 1$
94	68 93	eqtrd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \gcd P = 1$
95		eulerth	$⊢ (P \in ℕ \land y \in ℤ \land y \gcd P = 1) \to y^{ϕ (P)} \mod P = 1 \mod P$
96	65 32 94 95	syl3anc	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y^{ϕ (P)} \mod P = 1 \mod P$
97	63 96	eqtrd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to {(y^{2})}^{\frac{P - 1}{2}} \mod P = 1 \mod P$
98	1 2 3 4 5 6 7 8 9 10 11 36 34 97	lgsqrlem1	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to O (T) (L (y^{2})) = 0_{Y}$
99		eqid	$⊢ Y ↑_{𝑠} {Base}_{Y} = Y ↑_{𝑠} {Base}_{Y}$
100		eqid	$⊢ {Base}_{(Y ↑_{𝑠} {Base}_{Y})} = {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
101		fvexd	$⊢ φ \to {Base}_{Y} \in V$
102	5 2 99 27	evl1rhm	$⊢ Y \in CRing \to O \in (S RingHom (Y ↑_{𝑠} {Base}_{Y}))$
103	21 102	syl	$⊢ φ \to O \in (S RingHom (Y ↑_{𝑠} {Base}_{Y}))$
104	3 100	rhmf	$⊢ O \in (S RingHom (Y ↑_{𝑠} {Base}_{Y})) \to O : B ⟶ {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
105	103 104	syl	$⊢ φ \to O : B ⟶ {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
106	2	ply1ring	$⊢ Y \in Ring \to S \in Ring$
107	23 106	syl	$⊢ φ \to S \in Ring$
108		ringgrp	$⊢ S \in Ring \to S \in Grp$
109	107 108	syl	$⊢ φ \to S \in Grp$
110		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
111	110 3	mgpbas	$⊢ B = {Base}_{{mulGrp}_{S}}$
112	110	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
113	107 112	syl	$⊢ φ \to {mulGrp}_{S} \in Mnd$
114	7 2 3	vr1cl	$⊢ Y \in Ring \to X \in B$
115	23 114	syl	$⊢ φ \to X \in B$
116	111 6 113 42 115	mulgnn0cld	$⊢ φ \to (\frac{P - 1}{2}) \underset{˙}{\times} X \in B$
117	3 9	ringidcl	$⊢ S \in Ring \to \underset{˙}{1} \in B$
118	107 117	syl	$⊢ φ \to \underset{˙}{1} \in B$
119	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$
120	109 116 118 119	syl3anc	$⊢ φ \to ((\frac{P - 1}{2}) \underset{˙}{\times} X) \underset{˙}{-} \underset{˙}{1} \in B$
121	10 120	eqeltrid	$⊢ φ \to T \in B$
122	105 121	ffvelcdmd	$⊢ φ \to O (T) \in {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
123	99 27 100 16 101 122	pwselbas	$⊢ φ \to O (T) : {Base}_{Y} ⟶ {Base}_{Y}$
124	123	ffnd	$⊢ φ \to O (T) Fn {Base}_{Y}$
125	124	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to O (T) Fn {Base}_{Y}$
126		fniniseg	$⊢ O (T) Fn {Base}_{Y} \to (L (y^{2}) \in {O (T)}^{-1} [\{0_{Y}\}] \leftrightarrow (L (y^{2}) \in {Base}_{Y} \land O (T) (L (y^{2})) = 0_{Y}))$
127	125 126	syl	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to (L (y^{2}) \in {O (T)}^{-1} [\{0_{Y}\}] \leftrightarrow (L (y^{2}) \in {Base}_{Y} \land O (T) (L (y^{2})) = 0_{Y}))$
128	35 98 127	mpbir2and	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to L (y^{2}) \in {O (T)}^{-1} [\{0_{Y}\}]$
129	128 13	fmptd	$⊢ φ \to G : (1 \dots \frac{P - 1}{2}) ⟶ {O (T)}^{-1} [\{0_{Y}\}]$
130		fvoveq1	$⊢ y = x \to L (y^{2}) = L (x^{2})$
131		fvex	$⊢ L (x^{2}) \in V$
132	130 13 131	fvmpt	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to G (x) = L (x^{2})$
133	132	ad2antrl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to G (x) = L (x^{2})$
134		fvoveq1	$⊢ y = z \to L (y^{2}) = L (z^{2})$
135		fvex	$⊢ L (z^{2}) \in V$
136	134 13 135	fvmpt	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to G (z) = L (z^{2})$
137	136	ad2antll	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to G (z) = L (z^{2})$
138	133 137	eqeq12d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (G (x) = G (z) \leftrightarrow L (x^{2}) = L (z^{2}))$
139	48	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
140	139	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℕ_{0}$
141		elfzelz	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℤ$
142	141	ad2antrl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℤ$
143		zsqcl	$⊢ x \in ℤ \to x^{2} \in ℤ$
144	142 143	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x^{2} \in ℤ$
145		elfzelz	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \in ℤ$
146	145	ad2antll	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℤ$
147		zsqcl	$⊢ z \in ℤ \to z^{2} \in ℤ$
148	146 147	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z^{2} \in ℤ$
149	1 11	zndvds	$⊢ (P \in ℕ_{0} \land x^{2} \in ℤ \land z^{2} \in ℤ) \to (L (x^{2}) = L (z^{2}) \leftrightarrow P ∥ (x^{2} - z^{2}))$
150	140 144 148 149	syl3anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (L (x^{2}) = L (z^{2}) \leftrightarrow P ∥ (x^{2} - z^{2}))$
151		elfznn	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℕ$
152	151	ad2antrl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℕ$
153	152	nncnd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℂ$
154		elfznn	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \in ℕ$
155	154	ad2antll	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℕ$
156	155	nncnd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℂ$
157		subsq	$⊢ (x \in ℂ \land z \in ℂ) \to x^{2} - z^{2} = (x + z) (x - z)$
158	153 156 157	syl2anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x^{2} - z^{2} = (x + z) (x - z)$
159	158	breq2d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (x^{2} - z^{2}) \leftrightarrow P ∥ (x + z) (x - z))$
160	138 150 159	3bitrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (G (x) = G (z) \leftrightarrow P ∥ (x + z) (x - z))$
161	14	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℙ$
162	142 146	zaddcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℤ$
163	142 146	zsubcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x - z \in ℤ$
164		euclemma	$⊢ (P \in ℙ \land x + z \in ℤ \land x - z \in ℤ) \to (P ∥ (x + z) (x - z) \leftrightarrow (P ∥ (x + z) \lor P ∥ (x - z)))$
165	161 162 163 164	syl3anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (x + z) (x - z) \leftrightarrow (P ∥ (x + z) \lor P ∥ (x - z)))$
166	161 47	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℕ$
167	166	nnzd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℤ$
168	152 155	nnaddcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℕ$
169		dvdsle	$⊢ (P \in ℤ \land x + z \in ℕ) \to (P ∥ (x + z) \to P \leq x + z)$
170	167 168 169	syl2anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (x + z) \to P \leq x + z)$
171	168	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℝ$
172	166	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℝ$
173	172 50	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 \in ℝ$
174	152	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℝ$
175	155	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℝ$
176	70	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to \frac{P - 1}{2} \in ℝ$
177		elfzle2	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \leq \frac{P - 1}{2}$
178	177	ad2antrl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \leq \frac{P - 1}{2}$
179		elfzle2	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \leq \frac{P - 1}{2}$
180	179	ad2antll	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \leq \frac{P - 1}{2}$
181	174 175 176 176 178 180	le2addd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \leq (\frac{P - 1}{2}) + (\frac{P - 1}{2})$
182	52	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 \in ℂ$
183	182	2halvesd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (\frac{P - 1}{2}) + (\frac{P - 1}{2}) = P - 1$
184	181 183	breqtrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \leq P - 1$
185	172	ltm1d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 < P$
186	171 173 172 184 185	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z < P$
187	171 172	ltnled	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (x + z < P \leftrightarrow \neg P \leq x + z)$
188	186 187	mpbid	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to \neg P \leq x + z$
189	188	pm2.21d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (P \leq x + z \to x = z)$
190	170 189	syld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (x + z) \to x = z)$
191		moddvds	$⊢ (P \in ℕ \land x \in ℤ \land z \in ℤ) \to (x \mod P = z \mod P \leftrightarrow P ∥ (x - z))$
192	166 142 146 191	syl3anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (x \mod P = z \mod P \leftrightarrow P ∥ (x - z))$
193	166	nnrpd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℝ^{+}$
194	152	nnnn0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℕ_{0}$
195	194	nn0ge0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to 0 \leq x$
196	83	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to \frac{P - 1}{2} < P$
197	174 176 172 178 196	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x < P$
198		modid	$⊢ ((x \in ℝ \land P \in ℝ^{+}) \land (0 \leq x \land x < P)) \to x \mod P = x$
199	174 193 195 197 198	syl22anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \mod P = x$
200	155	nnnn0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℕ_{0}$
201	200	nn0ge0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to 0 \leq z$
202	175 176 172 180 196	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z < P$
203		modid	$⊢ ((z \in ℝ \land P \in ℝ^{+}) \land (0 \leq z \land z < P)) \to z \mod P = z$
204	175 193 201 202 203	syl22anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \mod P = z$
205	199 204	eqeq12d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (x \mod P = z \mod P \leftrightarrow x = z)$
206	192 205	bitr3d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (x - z) \leftrightarrow x = z)$
207	206	biimpd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (x - z) \to x = z)$
208	190 207	jaod	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to ((P ∥ (x + z) \lor P ∥ (x - z)) \to x = z)$
209	165 208	sylbid	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (P ∥ (x + z) (x - z) \to x = z)$
210	160 209	sylbid	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to (G (x) = G (z) \to x = z)$
211	210	ralrimivva	$⊢ φ \to \forall x \in (1 \dots \frac{P - 1}{2}) \forall z \in (1 \dots \frac{P - 1}{2}) (G (x) = G (z) \to x = z)$
212		dff13	$⊢ G : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} {O (T)}^{-1} [\{0_{Y}\}] \leftrightarrow (G : (1 \dots \frac{P - 1}{2}) ⟶ {O (T)}^{-1} [\{0_{Y}\}] \land \forall x \in (1 \dots \frac{P - 1}{2}) \forall z \in (1 \dots \frac{P - 1}{2}) (G (x) = G (z) \to x = z))$
213	129 211 212	sylanbrc	$⊢ φ \to G : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} {O (T)}^{-1} [\{0_{Y}\}]$

Metamath Proof Explorer

Theorem lgsqrlem2

Proof