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		gcdcom	$⊢ (y \in ℤ \land P \in ℤ) \to y \gcd P = P \gcd y$
69	32 67 68	syl2anc	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \gcd P = P \gcd y$
70	38	nnred	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \in ℝ$
71	51	rehalfcld	$⊢ φ \to \frac{P - 1}{2} \in ℝ$
72	71	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} \in ℝ$
73	49	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to P \in ℝ$
74		elfzle2	$⊢ y \in (1 \dots \frac{P - 1}{2}) \to y \leq \frac{P - 1}{2}$
75	74	adantl	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \leq \frac{P - 1}{2}$
76		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
77	14 76	syl	$⊢ φ \to P \in ℤ_{\geq 2}$
78		uz2m1nn	$⊢ P \in ℤ_{\geq 2} \to P - 1 \in ℕ$
79	77 78	syl	$⊢ φ \to P - 1 \in ℕ$
80	79	nnrpd	$⊢ φ \to P - 1 \in ℝ^{+}$
81		rphalflt	$⊢ P - 1 \in ℝ^{+} \to \frac{P - 1}{2} < P - 1$
82	80 81	syl	$⊢ φ \to \frac{P - 1}{2} < P - 1$
83	49	ltm1d	$⊢ φ \to P - 1 < P$
84	71 51 49 82 83	lttrd	$⊢ φ \to \frac{P - 1}{2} < P$
85	84	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \frac{P - 1}{2} < P$
86	70 72 73 75 85	lelttrd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y < P$
87	70 73	ltnled	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to (y < P \leftrightarrow \neg P \leq y)$
88	86 87	mpbid	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \neg P \leq y$
89		dvdsle	$⊢ (P \in ℤ \land y \in ℕ) \to (P ∥ y \to P \leq y)$
90	67 38 89	syl2anc	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to (P ∥ y \to P \leq y)$
91	88 90	mtod	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to \neg P ∥ y$
92		coprm	$⊢ (P \in ℙ \land y \in ℤ) \to (\neg P ∥ y \leftrightarrow P \gcd y = 1)$
93	64 32 92	syl2anc	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to (\neg P ∥ y \leftrightarrow P \gcd y = 1)$
94	91 93	mpbid	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to P \gcd y = 1$
95	69 94	eqtrd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y \gcd P = 1$
96		eulerth	$⊢ (P \in ℕ \land y \in ℤ \land y \gcd P = 1) \to y^{ϕ (P)} \mod P = 1 \mod P$
97	65 32 95 96	syl3anc	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to y^{ϕ (P)} \mod P = 1 \mod P$
98	63 97	eqtrd	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to {(y^{2})}^{\frac{P - 1}{2}} \mod P = 1 \mod P$
99	1 2 3 4 5 6 7 8 9 10 11 36 34 98	lgsqrlem1	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to O (T) (L (y^{2})) = 0_{Y}$
100		eqid	$⊢ Y ↑_{𝑠} {Base}_{Y} = Y ↑_{𝑠} {Base}_{Y}$
101		eqid	$⊢ {Base}_{(Y ↑_{𝑠} {Base}_{Y})} = {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
102		fvexd	$⊢ φ \to {Base}_{Y} \in V$
103	5 2 100 27	evl1rhm	$⊢ Y \in CRing \to O \in (S RingHom (Y ↑_{𝑠} {Base}_{Y}))$
104	21 103	syl	$⊢ φ \to O \in (S RingHom (Y ↑_{𝑠} {Base}_{Y}))$
105	3 101	rhmf	$⊢ O \in (S RingHom (Y ↑_{𝑠} {Base}_{Y})) \to O : B ⟶ {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
106	104 105	syl	$⊢ φ \to O : B ⟶ {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
107	2	ply1ring	$⊢ Y \in Ring \to S \in Ring$
108	23 107	syl	$⊢ φ \to S \in Ring$
109		ringgrp	$⊢ S \in Ring \to S \in Grp$
110	108 109	syl	$⊢ φ \to S \in Grp$
111		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
112	111	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
113	108 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 3	mgpbas	$⊢ B = {Base}_{{mulGrp}_{S}}$
117	116 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$
118	113 42 115 117	syl3anc	$⊢ φ \to (\frac{P - 1}{2}) \underset{˙}{\times} X \in B$
119	3 9	ringidcl	$⊢ S \in Ring \to \underset{˙}{1} \in B$
120	108 119	syl	$⊢ φ \to \underset{˙}{1} \in B$
121	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$
122	110 118 120 121	syl3anc	$⊢ φ \to ((\frac{P - 1}{2}) \underset{˙}{\times} X) \underset{˙}{-} \underset{˙}{1} \in B$
123	10 122	eqeltrid	$⊢ φ \to T \in B$
124	106 123	ffvelrnd	$⊢ φ \to O (T) \in {Base}_{(Y ↑_{𝑠} {Base}_{Y})}$
125	100 27 101 16 102 124	pwselbas	$⊢ φ \to O (T) : {Base}_{Y} ⟶ {Base}_{Y}$
126	125	ffnd	$⊢ φ \to O (T) Fn {Base}_{Y}$
127	126	adantr	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to O (T) Fn {Base}_{Y}$
128		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}))$
129	127 128	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}))$
130	35 99 129	mpbir2and	$⊢ (φ \land y \in (1 \dots \frac{P - 1}{2})) \to L (y^{2}) \in {O (T)}^{-1} [\{0_{Y}\}]$
131	130 13	fmptd	$⊢ φ \to G : (1 \dots \frac{P - 1}{2}) ⟶ {O (T)}^{-1} [\{0_{Y}\}]$
132		fvoveq1	$⊢ y = x \to L (y^{2}) = L (x^{2})$
133		fvex	$⊢ L (x^{2}) \in V$
134	132 13 133	fvmpt	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to G (x) = L (x^{2})$
135	134	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})$
136		fvoveq1	$⊢ y = z \to L (y^{2}) = L (z^{2})$
137		fvex	$⊢ L (z^{2}) \in V$
138	136 13 137	fvmpt	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to G (z) = L (z^{2})$
139	138	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})$
140	135 139	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}))$
141	48	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
142	141	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℕ_{0}$
143		elfzelz	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℤ$
144	143	ad2antrl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℤ$
145		zsqcl	$⊢ x \in ℤ \to x^{2} \in ℤ$
146	144 145	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x^{2} \in ℤ$
147		elfzelz	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \in ℤ$
148	147	ad2antll	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℤ$
149		zsqcl	$⊢ z \in ℤ \to z^{2} \in ℤ$
150	148 149	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z^{2} \in ℤ$
151	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}))$
152	142 146 150 151	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}))$
153		elfznn	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \in ℕ$
154	153	ad2antrl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℕ$
155	154	nncnd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℂ$
156		elfznn	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \in ℕ$
157	156	ad2antll	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℕ$
158	157	nncnd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℂ$
159		subsq	$⊢ (x \in ℂ \land z \in ℂ) \to x^{2} - z^{2} = (x + z) (x - z)$
160	155 158 159	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)$
161	160	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))$
162	140 152 161	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))$
163	14	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℙ$
164	144 148	zaddcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℤ$
165	144 148	zsubcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x - z \in ℤ$
166		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)))$
167	163 164 165 166	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)))$
168	163 47	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℕ$
169	168	nnzd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℤ$
170	154 157	nnaddcld	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℕ$
171		dvdsle	$⊢ (P \in ℤ \land x + z \in ℕ) \to (P ∥ (x + z) \to P \leq x + z)$
172	169 170 171	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)$
173	170	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z \in ℝ$
174	168	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℝ$
175	174 50	syl	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 \in ℝ$
176	154	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℝ$
177	157	nnred	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℝ$
178	71	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 ℝ$
179		elfzle2	$⊢ x \in (1 \dots \frac{P - 1}{2}) \to x \leq \frac{P - 1}{2}$
180	179	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}$
181		elfzle2	$⊢ z \in (1 \dots \frac{P - 1}{2}) \to z \leq \frac{P - 1}{2}$
182	181	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}$
183	176 177 178 178 180 182	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})$
184	52	adantr	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 \in ℂ$
185	184	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$
186	183 185	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$
187	174	ltm1d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P - 1 < P$
188	173 175 174 186 187	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x + z < P$
189	173 174	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)$
190	188 189	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$
191	190	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)$
192	172 191	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)$
193		moddvds	$⊢ (P \in ℕ \land x \in ℤ \land z \in ℤ) \to (x \mod P = z \mod P \leftrightarrow P ∥ (x - z))$
194	168 144 148 193	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))$
195	168	nnrpd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to P \in ℝ^{+}$
196	154	nnnn0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \in ℕ_{0}$
197	196	nn0ge0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to 0 \leq x$
198	84	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$
199	176 178 174 180 198	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x < P$
200		modid	$⊢ ((x \in ℝ \land P \in ℝ^{+}) \land (0 \leq x \land x < P)) \to x \mod P = x$
201	176 195 197 199 200	syl22anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to x \mod P = x$
202	157	nnnn0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \in ℕ_{0}$
203	202	nn0ge0d	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to 0 \leq z$
204	177 178 174 182 198	lelttrd	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z < P$
205		modid	$⊢ ((z \in ℝ \land P \in ℝ^{+}) \land (0 \leq z \land z < P)) \to z \mod P = z$
206	177 195 203 204 205	syl22anc	$⊢ (φ \land (x \in (1 \dots \frac{P - 1}{2}) \land z \in (1 \dots \frac{P - 1}{2}))) \to z \mod P = z$
207	201 206	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)$
208	194 207	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)$
209	208	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)$
210	192 209	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)$
211	167 210	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)$
212	162 211	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)$
213	212	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)$
214		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))$
215	131 213 214	sylanbrc	$⊢ φ \to G : (1 \dots \frac{P - 1}{2}) \underset{1-1}{⟶} {O (T)}^{-1} [\{0_{Y}\}]$

Metamath Proof Explorer

Theorem lgsqrlem2

Proof