lgsqrlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgsqrlem2		Structured version Visualization version GIF version

Theorem lgsqrlem2 27315

Description: Lemma for lgsqr 27319. (Contributed by Mario Carneiro, 15-Jun-2015.)

**Hypotheses**
Ref	Expression
lgsqr.y	⊢ 𝑌 = (ℤ/nℤ‘𝑃)
lgsqr.s	⊢ 𝑆 = (Poly₁‘𝑌)
lgsqr.b	⊢ 𝐵 = (Base‘𝑆)
lgsqr.d	⊢ 𝐷 = (deg₁‘𝑌)
lgsqr.o	⊢ 𝑂 = (eval₁‘𝑌)
lgsqr.e	⊢ ↑ = (._g‘(mulGrp‘𝑆))
lgsqr.x	⊢ 𝑋 = (var₁‘𝑌)
lgsqr.m	⊢ − = (-_g‘𝑆)
lgsqr.u	⊢ 1 = (1_r‘𝑆)
lgsqr.t	⊢ 𝑇 = ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 )
lgsqr.l	⊢ 𝐿 = (ℤRHom‘𝑌)
lgsqr.1	⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
lgsqr.g	⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2)))

**Assertion**
Ref	Expression
lgsqrlem2	⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))–1-1→(^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}))

Distinct variable groups: 𝑦,𝑂 𝑦,𝑃 𝜑,𝑦 𝑦,𝑇 𝑦,𝐿 𝑦,𝑌 Allowed substitution hints: 𝐵(𝑦) 𝐷(𝑦) 𝑆(𝑦) 1 (𝑦) ↑ (𝑦) 𝐺(𝑦) − (𝑦) 𝑋(𝑦)

Proof of Theorem lgsqrlem2 Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgsqr.1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
2	1	eldifad 3943	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
3		lgsqr.y	. . . . . . . . . . . . 13 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
4	3	znfld 21526	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field)
5	2, 4	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Field)
6		fldidom 20736	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn)
7	5, 6	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ IDomn)
8		isidom 20690	. . . . . . . . . . 11 ⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn))
9	8	simplbi 497	. . . . . . . . . 10 ⊢ (𝑌 ∈ IDomn → 𝑌 ∈ CRing)
10	7, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ CRing)
11		crngring 20210	. . . . . . . . 9 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
12	10, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ Ring)
13		lgsqr.l	. . . . . . . . 9 ⊢ 𝐿 = (ℤRHom‘𝑌)
14	13	zrhrhm 21477	. . . . . . . 8 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
15	12, 14	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
16		zringbas 21419	. . . . . . . 8 ⊢ ℤ = (Base‘ℤ_ring)
17		eqid 2736	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
18	16, 17	rhmf 20450	. . . . . . 7 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
19	15, 18	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
20	19	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
21		elfzelz 13546	. . . . . . 7 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ)
22	21	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℤ)
23		zsqcl 14152	. . . . . 6 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
24	22, 23	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑2) ∈ ℤ)
25	20, 24	ffvelcdmd 7080	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(𝑦↑2)) ∈ (Base‘𝑌))
26		lgsqr.s	. . . . 5 ⊢ 𝑆 = (Poly₁‘𝑌)
27		lgsqr.b	. . . . 5 ⊢ 𝐵 = (Base‘𝑆)
28		lgsqr.d	. . . . 5 ⊢ 𝐷 = (deg₁‘𝑌)
29		lgsqr.o	. . . . 5 ⊢ 𝑂 = (eval₁‘𝑌)
30		lgsqr.e	. . . . 5 ⊢ ↑ = (._g‘(mulGrp‘𝑆))
31		lgsqr.x	. . . . 5 ⊢ 𝑋 = (var₁‘𝑌)
32		lgsqr.m	. . . . 5 ⊢ − = (-_g‘𝑆)
33		lgsqr.u	. . . . 5 ⊢ 1 = (1_r‘𝑆)
34		lgsqr.t	. . . . 5 ⊢ 𝑇 = ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 )
35	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖ {2}))
36		elfznn 13575	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ)
37	36	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℕ)
38	37	nncnd 12261	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℂ)
39		oddprm 16835	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
40	1, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
41	40	nnnn0d 12567	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
42	41	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℕ₀)
43		2nn0 12523	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
44	43	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℕ₀)
45	38, 42, 44	expmuld 14172	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = ((𝑦↑2)↑((𝑃 − 1) / 2)))
46		prmnn 16698	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
47	2, 46	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℕ)
48	47	nnred 12260	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℝ)
49		peano2rem 11555	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
50	48, 49	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ)
51	50	recnd 11268	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
52		2cnd 12323	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
53		2ne0 12349	. . . . . . . . . . . . 13 ⊢ 2 ≠ 0
54	53	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 0)
55	51, 52, 54	divcan2d 12024	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
56		phiprm 16801	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
57	2, 56	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
58	55, 57	eqtr4d 2774	. . . . . . . . . 10 ⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (ϕ‘𝑃))
59	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((𝑃 − 1) / 2)) = (ϕ‘𝑃))
60	59	oveq2d 7426	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = (𝑦↑(ϕ‘𝑃)))
61	45, 60	eqtr3d 2773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑2)↑((𝑃 − 1) / 2)) = (𝑦↑(ϕ‘𝑃)))
62	61	oveq1d 7425	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (((𝑦↑2)↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑦↑(ϕ‘𝑃)) mod 𝑃))
63	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
64	63, 46	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
65	47	nnzd 12620	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
66	65	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
67	22, 66	gcdcomd 16538	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦))
68	37	nnred 12260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℝ)
69	50	rehalfcld 12493	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℝ)
70	69	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℝ)
71	48	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ)
72		elfzle2 13550	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2))
73	72	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ≤ ((𝑃 − 1) / 2))
74		prmuz2 16720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
75	2, 74	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘2))
76		uz2m1nn 12944	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ)
78	77	nnrpd 13054	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ⁺)
79		rphalflt 13043	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 − 1) ∈ ℝ⁺ → ((𝑃 − 1) / 2) < (𝑃 − 1))
80	78, 79	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑃 − 1) / 2) < (𝑃 − 1))
81	48	ltm1d 12179	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 − 1) < 𝑃)
82	69, 50, 48, 80, 81	lttrd 11401	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) / 2) < 𝑃)
83	82	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) < 𝑃)
84	68, 70, 71, 73, 83	lelttrd 11398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 < 𝑃)
85	68, 71	ltnled 11387	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑦))
86	84, 85	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ≤ 𝑦)
87		dvdsle 16334	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦))
88	66, 37, 87	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦))
89	86, 88	mtod 198	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ 𝑦)
90		coprm 16735	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ) → (¬ 𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1))
91	63, 22, 90	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1))
92	89, 91	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑦) = 1)
93	67, 92	eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = 1)
94		eulerth 16807	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ (𝑦 gcd 𝑃) = 1) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
95	64, 22, 93, 94	syl3anc 1373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
96	62, 95	eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (((𝑦↑2)↑((𝑃 − 1) / 2)) mod 𝑃) = (1 mod 𝑃))
97	3, 26, 27, 28, 29, 30, 31, 32, 33, 34, 13, 35, 24, 96	lgsqrlem1 27314	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0_g‘𝑌))
98		eqid 2736	. . . . . . . 8 ⊢ (𝑌 ↑_s (Base‘𝑌)) = (𝑌 ↑_s (Base‘𝑌))
99		eqid 2736	. . . . . . . 8 ⊢ (Base‘(𝑌 ↑_s (Base‘𝑌))) = (Base‘(𝑌 ↑_s (Base‘𝑌)))
100		fvexd 6896	. . . . . . . 8 ⊢ (𝜑 → (Base‘𝑌) ∈ V)
101	29, 26, 98, 17	evl1rhm 22275	. . . . . . . . . . 11 ⊢ (𝑌 ∈ CRing → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))))
102	10, 101	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))))
103	27, 99	rhmf 20450	. . . . . . . . . 10 ⊢ (𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))) → 𝑂:𝐵⟶(Base‘(𝑌 ↑_s (Base‘𝑌))))
104	102, 103	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑌 ↑_s (Base‘𝑌))))
105	26	ply1ring 22188	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ Ring → 𝑆 ∈ Ring)
106	12, 105	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Ring)
107		ringgrp 20203	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp)
108	106, 107	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Grp)
109		eqid 2736	. . . . . . . . . . . . 13 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
110	109, 27	mgpbas 20110	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘(mulGrp‘𝑆))
111	109	ringmgp 20204	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
112	106, 111	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
113	31, 26, 27	vr1cl 22158	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ Ring → 𝑋 ∈ 𝐵)
114	12, 113	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
115	110, 30, 112, 41, 114	mulgnn0cld 19083	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵)
116	27, 33	ringidcl 20230	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Ring → 1 ∈ 𝐵)
117	106, 116	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ 𝐵)
118	27, 32	grpsubcl 19008	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Grp ∧ (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵)
119	108, 115, 117, 118	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵)
120	34, 119	eqeltrid 2839	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ 𝐵)
121	104, 120	ffvelcdmd 7080	. . . . . . . 8 ⊢ (𝜑 → (𝑂‘𝑇) ∈ (Base‘(𝑌 ↑_s (Base‘𝑌))))
122	98, 17, 99, 5, 100, 121	pwselbas 17508	. . . . . . 7 ⊢ (𝜑 → (𝑂‘𝑇):(Base‘𝑌)⟶(Base‘𝑌))
123	122	ffnd 6712	. . . . . 6 ⊢ (𝜑 → (𝑂‘𝑇) Fn (Base‘𝑌))
124	123	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑂‘𝑇) Fn (Base‘𝑌))
125		fniniseg 7055	. . . . 5 ⊢ ((𝑂‘𝑇) Fn (Base‘𝑌) → ((𝐿‘(𝑦↑2)) ∈ (^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}) ↔ ((𝐿‘(𝑦↑2)) ∈ (Base‘𝑌) ∧ ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0_g‘𝑌))))
126	124, 125	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝐿‘(𝑦↑2)) ∈ (^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}) ↔ ((𝐿‘(𝑦↑2)) ∈ (Base‘𝑌) ∧ ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0_g‘𝑌))))
127	25, 97, 126	mpbir2and 713	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(𝑦↑2)) ∈ (^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}))
128		lgsqr.g	. . 3 ⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2)))
129	127, 128	fmptd 7109	. 2 ⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))⟶(^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}))
130		fvoveq1 7433	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑥↑2)))
131		fvex 6894	. . . . . . . 8 ⊢ (𝐿‘(𝑥↑2)) ∈ V
132	130, 128, 131	fvmpt 6991	. . . . . . 7 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2)))
133	132	ad2antrl 728	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2)))
134		fvoveq1 7433	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑧↑2)))
135		fvex 6894	. . . . . . . 8 ⊢ (𝐿‘(𝑧↑2)) ∈ V
136	134, 128, 135	fvmpt 6991	. . . . . . 7 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2)))
137	136	ad2antll 729	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2)))
138	133, 137	eqeq12d 2752	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ (𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2))))
139	47	nnnn0d 12567	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
140	139	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ₀)
141		elfzelz 13546	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
142	141	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℤ)
143		zsqcl 14152	. . . . . . 7 ⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈ ℤ)
144	142, 143	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥↑2) ∈ ℤ)
145		elfzelz 13546	. . . . . . . 8 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℤ)
146	145	ad2antll 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℤ)
147		zsqcl 14152	. . . . . . 7 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℤ)
148	146, 147	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧↑2) ∈ ℤ)
149	3, 13	zndvds 21515	. . . . . 6 ⊢ ((𝑃 ∈ ℕ₀ ∧ (𝑥↑2) ∈ ℤ ∧ (𝑧↑2) ∈ ℤ) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2))))
150	140, 144, 148, 149	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2))))
151		elfznn 13575	. . . . . . . . 9 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
152	151	ad2antrl 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ)
153	152	nncnd 12261	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℂ)
154		elfznn 13575	. . . . . . . . 9 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℕ)
155	154	ad2antll 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℕ)
156	155	nncnd 12261	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℂ)
157		subsq 14233	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧)))
158	153, 156, 157	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧)))
159	158	breq2d 5136	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥↑2) − (𝑧↑2)) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧))))
160	138, 150, 159	3bitrd 305	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧))))
161	2	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ)
162	142, 146	zaddcld 12706	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℤ)
163	142, 146	zsubcld 12707	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 − 𝑧) ∈ ℤ)
164		euclemma 16737	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 + 𝑧) ∈ ℤ ∧ (𝑥 − 𝑧) ∈ ℤ) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧))))
165	161, 162, 163, 164	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧))))
166	161, 46	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ)
167	166	nnzd 12620	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ)
168	152, 155	nnaddcld 12297	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℕ)
169		dvdsle 16334	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ (𝑥 + 𝑧) ∈ ℕ) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧)))
170	167, 168, 169	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧)))
171	168	nnred 12260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℝ)
172	166	nnred 12260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ)
173	172, 49	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℝ)
174	152	nnred 12260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℝ)
175	155	nnred 12260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℝ)
176	69	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℝ)
177		elfzle2 13550	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
178	177	ad2antrl 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2))
179		elfzle2 13550	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ≤ ((𝑃 − 1) / 2))
180	179	ad2antll 729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ≤ ((𝑃 − 1) / 2))
181	174, 175, 176, 176, 178, 180	le2addd 11861	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)))
182	51	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℂ)
183	182	2halvesd 12492	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
184	181, 183	breqtrd 5150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (𝑃 − 1))
185	172	ltm1d 12179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) < 𝑃)
186	171, 173, 172, 184, 185	lelttrd 11398	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) < 𝑃)
187	171, 172	ltnled 11387	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 + 𝑧) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑥 + 𝑧)))
188	186, 187	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ¬ 𝑃 ≤ (𝑥 + 𝑧))
189	188	pm2.21d 121	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ≤ (𝑥 + 𝑧) → 𝑥 = 𝑧))
190	170, 189	syld 47	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑥 = 𝑧))
191		moddvds 16288	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧)))
192	166, 142, 146, 191	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧)))
193	166	nnrpd 13054	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ⁺)
194	152	nnnn0d 12567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ₀)
195	194	nn0ge0d 12570	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑥)
196	82	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) < 𝑃)
197	174, 176, 172, 178, 196	lelttrd 11398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 < 𝑃)
198		modid 13918	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑃)) → (𝑥 mod 𝑃) = 𝑥)
199	174, 193, 195, 197, 198	syl22anc 838	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 mod 𝑃) = 𝑥)
200	155	nnnn0d 12567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℕ₀)
201	200	nn0ge0d 12570	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑧)
202	175, 176, 172, 180, 196	lelttrd 11398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 < 𝑃)
203		modid 13918	. . . . . . . . . 10 ⊢ (((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 𝑧 ∧ 𝑧 < 𝑃)) → (𝑧 mod 𝑃) = 𝑧)
204	175, 193, 201, 202, 203	syl22anc 838	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧 mod 𝑃) = 𝑧)
205	199, 204	eqeq12d 2752	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑥 = 𝑧))
206	192, 205	bitr3d 281	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) ↔ 𝑥 = 𝑧))
207	206	biimpd 229	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) → 𝑥 = 𝑧))
208	190, 207	jaod 859	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)) → 𝑥 = 𝑧))
209	165, 208	sylbid 240	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) → 𝑥 = 𝑧))
210	160, 209	sylbid 240	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧))
211	210	ralrimivva 3188	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧))
212		dff13 7252	. 2 ⊢ (𝐺:(1...((𝑃 − 1) / 2))–1-1→(^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}) ↔ (𝐺:(1...((𝑃 − 1) / 2))⟶(^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}) ∧ ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧)))
213	129, 211, 212	sylanbrc 583	1 ⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))–1-1→(^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 Vcvv 3464 ∖ cdif 3928 {csn 4606 class class class wbr 5124 ↦ cmpt 5206 ^◡ccnv 5658 “ cima 5662 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 · cmul 11139 < clt 11274 ≤ cle 11275 − cmin 11471 / cdiv 11899 ℕcn 12245 2c2 12300 ℕ₀cn0 12506 ℤcz 12593 ℤ_≥cuz 12857 ℝ⁺crp 13013 ...cfz 13529 mod cmo 13891 ↑cexp 14084 ∥ cdvds 16277 gcd cgcd 16518 ℙcprime 16695 ϕcphi 16788 Basecbs 17233 0_gc0g 17458 ↑_s cpws 17465 Mndcmnd 18717 Grpcgrp 18921 -_gcsg 18923 ._gcmg 19055 mulGrpcmgp 20105 1_rcur 20146 Ringcrg 20198 CRingccrg 20199 RingHom crh 20434 Domncdomn 20657 IDomncidom 20658 Fieldcfield 20695 ℤ_ringczring 21412 ℤRHomczrh 21465 ℤ/nℤczn 21468 var₁cv1 22116 Poly₁cpl1 22117 eval₁ce1 22257 deg₁cdg1 26016

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212 ax-addf 11213 ax-mulf 11214

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-ofr 7677 df-om 7867 df-1st 7993 df-2nd 7994 df-supp 8165 df-tpos 8230 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-oadd 8489 df-er 8724 df-ec 8726 df-qs 8730 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9379 df-sup 9459 df-inf 9460 df-oi 9529 df-dju 9920 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-xnn0 12580 df-z 12594 df-dec 12714 df-uz 12858 df-rp 13014 df-fz 13530 df-fzo 13677 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-hash 14354 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-dvds 16278 df-gcd 16519 df-prm 16696 df-phi 16790 df-struct 17171 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-mulr 17290 df-starv 17291 df-sca 17292 df-vsca 17293 df-ip 17294 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-hom 17300 df-cco 17301 df-0g 17460 df-gsum 17461 df-prds 17466 df-pws 17468 df-imas 17527 df-qus 17528 df-mre 17603 df-mrc 17604 df-acs 17606 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-mhm 18766 df-submnd 18767 df-grp 18924 df-minusg 18925 df-sbg 18926 df-mulg 19056 df-subg 19111 df-nsg 19112 df-eqg 19113 df-ghm 19201 df-cntz 19305 df-cmn 19768 df-abl 19769 df-mgp 20106 df-rng 20118 df-ur 20147 df-srg 20152 df-ring 20200 df-cring 20201 df-oppr 20302 df-dvdsr 20322 df-unit 20323 df-invr 20353 df-dvr 20366 df-rhm 20437 df-nzr 20478 df-subrng 20511 df-subrg 20535 df-rlreg 20659 df-domn 20660 df-idom 20661 df-drng 20696 df-field 20697 df-lmod 20824 df-lss 20894 df-lsp 20934 df-sra 21136 df-rgmod 21137 df-lidl 21174 df-rsp 21175 df-2idl 21216 df-cnfld 21321 df-zring 21413 df-zrh 21469 df-zn 21472 df-assa 21818 df-asp 21819 df-ascl 21820 df-psr 21874 df-mvr 21875 df-mpl 21876 df-opsr 21878 df-evls 22037 df-evl 22038 df-psr1 22120 df-vr1 22121 df-ply1 22122 df-evl1 22259

This theorem is referenced by: lgsqrlem4 27317

W3C validator