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 27285

Description: Lemma for lgsqr 27289. (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 3909	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
3		lgsqr.y	. . . . . . . . . . . . 13 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
4	3	znfld 21497	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field)
5	2, 4	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Field)
6		fldidom 20686	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn)
7	5, 6	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ IDomn)
8		isidom 20640	. . . . . . . . . . 11 ⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn))
9	8	simplbi 497	. . . . . . . . . 10 ⊢ (𝑌 ∈ IDomn → 𝑌 ∈ CRing)
10	7, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ CRing)
11		crngring 20163	. . . . . . . . 9 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
12	10, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ Ring)
13		lgsqr.l	. . . . . . . . 9 ⊢ 𝐿 = (ℤRHom‘𝑌)
14	13	zrhrhm 21448	. . . . . . . 8 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
15	12, 14	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
16		zringbas 21390	. . . . . . . 8 ⊢ ℤ = (Base‘ℤ_ring)
17		eqid 2731	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
18	16, 17	rhmf 20402	. . . . . . 7 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
19	15, 18	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
20	19	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
21		elfzelz 13424	. . . . . . 7 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ)
22	21	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℤ)
23		zsqcl 14036	. . . . . 6 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
24	22, 23	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑2) ∈ ℤ)
25	20, 24	ffvelcdmd 7018	. . . 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 13453	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ)
37	36	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℕ)
38	37	nncnd 12141	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℂ)
39		oddprm 16722	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
40	1, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
41	40	nnnn0d 12442	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
42	41	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℕ₀)
43		2nn0 12398	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
44	43	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℕ₀)
45	38, 42, 44	expmuld 14056	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = ((𝑦↑2)↑((𝑃 − 1) / 2)))
46		prmnn 16585	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
47	2, 46	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℕ)
48	47	nnred 12140	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℝ)
49		peano2rem 11428	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
50	48, 49	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ)
51	50	recnd 11140	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
52		2cnd 12203	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
53		2ne0 12229	. . . . . . . . . . . . 13 ⊢ 2 ≠ 0
54	53	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 0)
55	51, 52, 54	divcan2d 11899	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
56		phiprm 16688	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
57	2, 56	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
58	55, 57	eqtr4d 2769	. . . . . . . . . 10 ⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (ϕ‘𝑃))
59	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((𝑃 − 1) / 2)) = (ϕ‘𝑃))
60	59	oveq2d 7362	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = (𝑦↑(ϕ‘𝑃)))
61	45, 60	eqtr3d 2768	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑2)↑((𝑃 − 1) / 2)) = (𝑦↑(ϕ‘𝑃)))
62	61	oveq1d 7361	. . . . . 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 12495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
66	65	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
67	22, 66	gcdcomd 16425	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦))
68	37	nnred 12140	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℝ)
69	50	rehalfcld 12368	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℝ)
70	69	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℝ)
71	48	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ)
72		elfzle2 13428	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2))
73	72	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ≤ ((𝑃 − 1) / 2))
74		prmuz2 16607	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
75	2, 74	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘2))
76		uz2m1nn 12821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ)
78	77	nnrpd 12932	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ⁺)
79		rphalflt 12921	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 − 1) ∈ ℝ⁺ → ((𝑃 − 1) / 2) < (𝑃 − 1))
80	78, 79	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑃 − 1) / 2) < (𝑃 − 1))
81	48	ltm1d 12054	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 − 1) < 𝑃)
82	69, 50, 48, 80, 81	lttrd 11274	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) / 2) < 𝑃)
83	82	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) < 𝑃)
84	68, 70, 71, 73, 83	lelttrd 11271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 < 𝑃)
85	68, 71	ltnled 11260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑦))
86	84, 85	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ≤ 𝑦)
87		dvdsle 16221	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦))
88	66, 37, 87	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦))
89	86, 88	mtod 198	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ 𝑦)
90		coprm 16622	. . . . . . . . . 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 2766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = 1)
94		eulerth 16694	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ (𝑦 gcd 𝑃) = 1) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
95	64, 22, 93, 94	syl3anc 1373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
96	62, 95	eqtrd 2766	. . . . 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 27284	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑂‘𝑇)‘(𝐿‘(𝑦↑2))) = (0_g‘𝑌))
98		eqid 2731	. . . . . . . 8 ⊢ (𝑌 ↑_s (Base‘𝑌)) = (𝑌 ↑_s (Base‘𝑌))
99		eqid 2731	. . . . . . . 8 ⊢ (Base‘(𝑌 ↑_s (Base‘𝑌))) = (Base‘(𝑌 ↑_s (Base‘𝑌)))
100		fvexd 6837	. . . . . . . 8 ⊢ (𝜑 → (Base‘𝑌) ∈ V)
101	29, 26, 98, 17	evl1rhm 22247	. . . . . . . . . . 11 ⊢ (𝑌 ∈ CRing → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))))
102	10, 101	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))))
103	27, 99	rhmf 20402	. . . . . . . . . 10 ⊢ (𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))) → 𝑂:𝐵⟶(Base‘(𝑌 ↑_s (Base‘𝑌))))
104	102, 103	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑌 ↑_s (Base‘𝑌))))
105	26	ply1ring 22160	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ Ring → 𝑆 ∈ Ring)
106	12, 105	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Ring)
107		ringgrp 20156	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp)
108	106, 107	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Grp)
109		eqid 2731	. . . . . . . . . . . . 13 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
110	109, 27	mgpbas 20063	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘(mulGrp‘𝑆))
111	109	ringmgp 20157	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
112	106, 111	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
113	31, 26, 27	vr1cl 22130	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ Ring → 𝑋 ∈ 𝐵)
114	12, 113	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
115	110, 30, 112, 41, 114	mulgnn0cld 19008	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵)
116	27, 33	ringidcl 20183	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Ring → 1 ∈ 𝐵)
117	106, 116	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ 𝐵)
118	27, 32	grpsubcl 18933	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Grp ∧ (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵)
119	108, 115, 117, 118	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵)
120	34, 119	eqeltrid 2835	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ 𝐵)
121	104, 120	ffvelcdmd 7018	. . . . . . . 8 ⊢ (𝜑 → (𝑂‘𝑇) ∈ (Base‘(𝑌 ↑_s (Base‘𝑌))))
122	98, 17, 99, 5, 100, 121	pwselbas 17393	. . . . . . 7 ⊢ (𝜑 → (𝑂‘𝑇):(Base‘𝑌)⟶(Base‘𝑌))
123	122	ffnd 6652	. . . . . 6 ⊢ (𝜑 → (𝑂‘𝑇) Fn (Base‘𝑌))
124	123	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑂‘𝑇) Fn (Base‘𝑌))
125		fniniseg 6993	. . . . 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 7047	. 2 ⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))⟶(^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}))
130		fvoveq1 7369	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑥↑2)))
131		fvex 6835	. . . . . . . 8 ⊢ (𝐿‘(𝑥↑2)) ∈ V
132	130, 128, 131	fvmpt 6929	. . . . . . 7 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2)))
133	132	ad2antrl 728	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2)))
134		fvoveq1 7369	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑧↑2)))
135		fvex 6835	. . . . . . . 8 ⊢ (𝐿‘(𝑧↑2)) ∈ V
136	134, 128, 135	fvmpt 6929	. . . . . . 7 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2)))
137	136	ad2antll 729	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2)))
138	133, 137	eqeq12d 2747	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ (𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2))))
139	47	nnnn0d 12442	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
140	139	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ₀)
141		elfzelz 13424	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
142	141	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℤ)
143		zsqcl 14036	. . . . . . 7 ⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈ ℤ)
144	142, 143	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥↑2) ∈ ℤ)
145		elfzelz 13424	. . . . . . . 8 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℤ)
146	145	ad2antll 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℤ)
147		zsqcl 14036	. . . . . . 7 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℤ)
148	146, 147	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧↑2) ∈ ℤ)
149	3, 13	zndvds 21486	. . . . . 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 13453	. . . . . . . . 9 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
152	151	ad2antrl 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ)
153	152	nncnd 12141	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℂ)
154		elfznn 13453	. . . . . . . . 9 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℕ)
155	154	ad2antll 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℕ)
156	155	nncnd 12141	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℂ)
157		subsq 14117	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧)))
158	153, 156, 157	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧)))
159	158	breq2d 5101	. . . . 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 12581	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℤ)
163	142, 146	zsubcld 12582	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 − 𝑧) ∈ ℤ)
164		euclemma 16624	. . . . . 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 12495	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ)
168	152, 155	nnaddcld 12177	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℕ)
169		dvdsle 16221	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ (𝑥 + 𝑧) ∈ ℕ) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧)))
170	167, 168, 169	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧)))
171	168	nnred 12140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℝ)
172	166	nnred 12140	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ)
173	172, 49	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℝ)
174	152	nnred 12140	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℝ)
175	155	nnred 12140	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℝ)
176	69	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℝ)
177		elfzle2 13428	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
178	177	ad2antrl 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2))
179		elfzle2 13428	. . . . . . . . . . . . 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 11736	. . . . . . . . . . 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 12367	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
184	181, 183	breqtrd 5115	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (𝑃 − 1))
185	172	ltm1d 12054	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) < 𝑃)
186	171, 173, 172, 184, 185	lelttrd 11271	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) < 𝑃)
187	171, 172	ltnled 11260	. . . . . . . . 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 16174	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧)))
192	166, 142, 146, 191	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧)))
193	166	nnrpd 12932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ⁺)
194	152	nnnn0d 12442	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ₀)
195	194	nn0ge0d 12445	. . . . . . . . . 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 11271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 < 𝑃)
198		modid 13800	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑃)) → (𝑥 mod 𝑃) = 𝑥)
199	174, 193, 195, 197, 198	syl22anc 838	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 mod 𝑃) = 𝑥)
200	155	nnnn0d 12442	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℕ₀)
201	200	nn0ge0d 12445	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑧)
202	175, 176, 172, 180, 196	lelttrd 11271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 < 𝑃)
203		modid 13800	. . . . . . . . . 10 ⊢ (((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 𝑧 ∧ 𝑧 < 𝑃)) → (𝑧 mod 𝑃) = 𝑧)
204	175, 193, 201, 202, 203	syl22anc 838	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧 mod 𝑃) = 𝑧)
205	199, 204	eqeq12d 2747	. . . . . . . 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 3175	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧))
212		dff13 7188	. 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 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 Vcvv 3436 ∖ cdif 3894 {csn 4573 class class class wbr 5089 ↦ cmpt 5170 ^◡ccnv 5613 “ cima 5617 Fn wfn 6476 ⟶wf 6477 –1-1→wf1 6478 ‘cfv 6481 (class class class)co 7346 ℂcc 11004 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 < clt 11146 ≤ cle 11147 − cmin 11344 / cdiv 11774 ℕcn 12125 2c2 12180 ℕ₀cn0 12381 ℤcz 12468 ℤ_≥cuz 12732 ℝ⁺crp 12890 ...cfz 13407 mod cmo 13773 ↑cexp 13968 ∥ cdvds 16163 gcd cgcd 16405 ℙcprime 16582 ϕcphi 16675 Basecbs 17120 0_gc0g 17343 ↑_s cpws 17350 Mndcmnd 18642 Grpcgrp 18846 -_gcsg 18848 ._gcmg 18980 mulGrpcmgp 20058 1_rcur 20099 Ringcrg 20151 CRingccrg 20152 RingHom crh 20387 Domncdomn 20607 IDomncidom 20608 Fieldcfield 20645 ℤ_ringczring 21383 ℤRHomczrh 21436 ℤ/nℤczn 21439 var₁cv1 22088 Poly₁cpl1 22089 eval₁ce1 22229 deg₁cdg1 25986

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084 ax-addf 11085 ax-mulf 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-iin 4942 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-ofr 7611 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-tpos 8156 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-oadd 8389 df-er 8622 df-ec 8624 df-qs 8628 df-map 8752 df-pm 8753 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fsupp 9246 df-sup 9326 df-inf 9327 df-oi 9396 df-dju 9794 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-5 12191 df-6 12192 df-7 12193 df-8 12194 df-9 12195 df-n0 12382 df-xnn0 12455 df-z 12469 df-dec 12589 df-uz 12733 df-rp 12891 df-fz 13408 df-fzo 13555 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-dvds 16164 df-gcd 16406 df-prm 16583 df-phi 16677 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-0g 17345 df-gsum 17346 df-prds 17351 df-pws 17353 df-imas 17412 df-qus 17413 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18548 df-sgrp 18627 df-mnd 18643 df-mhm 18691 df-submnd 18692 df-grp 18849 df-minusg 18850 df-sbg 18851 df-mulg 18981 df-subg 19036 df-nsg 19037 df-eqg 19038 df-ghm 19125 df-cntz 19229 df-cmn 19694 df-abl 19695 df-mgp 20059 df-rng 20071 df-ur 20100 df-srg 20105 df-ring 20153 df-cring 20154 df-oppr 20255 df-dvdsr 20275 df-unit 20276 df-invr 20306 df-dvr 20319 df-rhm 20390 df-nzr 20428 df-subrng 20461 df-subrg 20485 df-rlreg 20609 df-domn 20610 df-idom 20611 df-drng 20646 df-field 20647 df-lmod 20795 df-lss 20865 df-lsp 20905 df-sra 21107 df-rgmod 21108 df-lidl 21145 df-rsp 21146 df-2idl 21187 df-cnfld 21292 df-zring 21384 df-zrh 21440 df-zn 21443 df-assa 21790 df-asp 21791 df-ascl 21792 df-psr 21846 df-mvr 21847 df-mpl 21848 df-opsr 21850 df-evls 22009 df-evl 22010 df-psr1 22092 df-vr1 22093 df-ply1 22094 df-evl1 22231

This theorem is referenced by: lgsqrlem4 27287

W3C validator