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	ffvelrnd	$⊢ (φ \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	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
112	107 111	syl	$⊢ φ \to {mulGrp}_{S} \in Mnd$
113	7 2 3	vr1cl	$⊢ Y \in Ring \to X \in B$
114	23 113	syl	$⊢ φ \to X \in B$
115	110 3	mgpbas	$⊢ B = {Base}_{{mulGrp}_{S}}$
116	115 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$
117	112 42 114 116	syl3anc	$⊢ φ \to (\frac{P - 1}{2}) \underset{˙}{\times} X \in B$
118	3 9	ringidcl	$⊢ S \in Ring \to \underset{˙}{1} \in B$
119	107 118	syl	$⊢ φ \to \underset{˙}{1} \in B$
120	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$
121	109 117 119 120	syl3anc	$⊢ φ \to ((\frac{P - 1}{2}) \underset{˙}{\times} X) \underset{˙}{-} \underset{˙}{1} \in B$
122	10 121	eqeltrid	$⊢ φ \to T \in B$
123	105 122	ffvelrnd	$⊢ φ \to O (T) \in {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
124	99 27 100 16 101 123	pwselbas	$⊢ φ \to O (T) : {Base}_{Y} ⟶ {Base}_{Y}$
125	124	ffnd	$⊢ φ \to O (T) Fn {Base}_{Y}$
126	125	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to O (T) Fn {Base}_{Y}$
127		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}))$
128	126 127	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}))$
129	35 98 128	mpbir2and	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to L (y^{2}) \in {O (T)}^{-1} [\{0_{Y}\}]$
130	129 13	fmptd	$⊢ φ \to G : (1 \dots \frac{P - 1}{2}) ⟶ {O (T)}^{-1} [\{0_{Y}\}]$
131		fvoveq1	$⊢ y = x \to L (y^{2}) = L (x^{2})$
132		fvex	$⊢ L (x^{2}) \in V$
133	131 13 132	fvmpt	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to G (x) = L (x^{2})$
134	133	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})$
135		fvoveq1	$⊢ y = z \to L (y^{2}) = L (z^{2})$
136		fvex	$⊢ L (z^{2}) \in V$
137	135 13 136	fvmpt	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to G (z) = L (z^{2})$
138	137	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})$
139	134 138	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}))$
140	48	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
141	140	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℕ_{0}$
142		elfzelz	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℤ$
143	142	ad2antrl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℤ$
144		zsqcl	$⊢ x \in ℤ \to x^{2} \in ℤ$
145	143 144	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x^{2} \in ℤ$
146		elfzelz	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \in ℤ$
147	146	ad2antll	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℤ$
148		zsqcl	$⊢ z \in ℤ \to z^{2} \in ℤ$
149	147 148	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z^{2} \in ℤ$
150	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}))$
151	141 145 149 150	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}))$
152		elfznn	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℕ$
153	152	ad2antrl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℕ$
154	153	nncnd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℂ$
155		elfznn	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \in ℕ$
156	155	ad2antll	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℕ$
157	156	nncnd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℂ$
158		subsq	$⊢ (x \in ℂ \land z \in ℂ) \to x^{2} - z^{2} = (x + z) (x - z)$
159	154 157 158	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)$
160	159	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))$
161	139 151 160	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))$
162	14	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℙ$
163	143 147	zaddcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℤ$
164	143 147	zsubcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x - z \in ℤ$
165		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)))$
166	162 163 164 165	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)))$
167	162 47	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℕ$
168	167	nnzd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℤ$
169	153 156	nnaddcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℕ$
170		dvdsle	$⊢ (P \in ℤ \land x + z \in ℕ) \to (P ∥ (x + z) \to P \leq x + z)$
171	168 169 170	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)$
172	169	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℝ$
173	167	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℝ$
174	173 50	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 \in ℝ$
175	153	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℝ$
176	156	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℝ$
177	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 ℝ$
178		elfzle2	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \leq \frac{P - 1}{2}$
179	178	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}$
180		elfzle2	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \leq \frac{P - 1}{2}$
181	180	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}$
182	175 176 177 177 179 181	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})$
183	52	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 \in ℂ$
184	183	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$
185	182 184	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$
186	173	ltm1d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 < P$
187	172 174 173 185 186	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z < P$
188	172 173	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)$
189	187 188	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$
190	189	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)$
191	171 190	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)$
192		moddvds	$⊢ (P \in ℕ \land x \in ℤ \land z \in ℤ) \to (x \mod P = z \mod P \leftrightarrow P ∥ (x - z))$
193	167 143 147 192	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))$
194	167	nnrpd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℝ^{+}$
195	153	nnnn0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℕ_{0}$
196	195	nn0ge0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to 0 \leq x$
197	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$
198	175 177 173 179 197	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x < P$
199		modid	$⊢ ((x \in ℝ \land P \in ℝ^{+}) \land (0 \leq x \land x < P)) \to x \mod P = x$
200	175 194 196 198 199	syl22anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \mod P = x$
201	156	nnnn0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℕ_{0}$
202	201	nn0ge0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to 0 \leq z$
203	176 177 173 181 197	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z < P$
204		modid	$⊢ ((z \in ℝ \land P \in ℝ^{+}) \land (0 \leq z \land z < P)) \to z \mod P = z$
205	176 194 202 203 204	syl22anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \mod P = z$
206	200 205	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)$
207	193 206	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)$
208	207	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)$
209	191 208	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)$
210	166 209	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)$
211	161 210	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)$
212	211	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)$
213		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))$
214	130 212 213	sylanbrc	$⊢ φ \to G : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} {O (T)}^{-1} [\{0_{Y}\}]$

Metamath Proof Explorer

Theorem lgsqrlem2

Proof