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 26695

Description: Lemma for lgsqr 26699. (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 3922	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℙ)
3		lgsqr.y	. . . . . . . . . . . . 13 ⊢ 𝑌 = (ℤ/nℤ‘𝑃)
4	3	znfld 20967	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑌 ∈ Field)
5	2, 4	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Field)
6		fldidom 20775	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Field → 𝑌 ∈ IDomn)
7	5, 6	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ IDomn)
8		isidom 20774	. . . . . . . . . . 11 ⊢ (𝑌 ∈ IDomn ↔ (𝑌 ∈ CRing ∧ 𝑌 ∈ Domn))
9	8	simplbi 498	. . . . . . . . . 10 ⊢ (𝑌 ∈ IDomn → 𝑌 ∈ CRing)
10	7, 9	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ CRing)
11		crngring 19976	. . . . . . . . 9 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
12	10, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ Ring)
13		lgsqr.l	. . . . . . . . 9 ⊢ 𝐿 = (ℤRHom‘𝑌)
14	13	zrhrhm 20912	. . . . . . . 8 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
15	12, 14	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ (ℤ_ring RingHom 𝑌))
16		zringbas 20875	. . . . . . . 8 ⊢ ℤ = (Base‘ℤ_ring)
17		eqid 2736	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
18	16, 17	rhmf 20158	. . . . . . 7 ⊢ (𝐿 ∈ (ℤ_ring RingHom 𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
19	15, 18	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑌))
20	19	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝐿:ℤ⟶(Base‘𝑌))
21		elfzelz 13441	. . . . . . 7 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℤ)
22	21	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℤ)
23		zsqcl 14034	. . . . . 6 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
24	22, 23	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑2) ∈ ℤ)
25	20, 24	ffvelcdmd 7036	. . . 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 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ (ℙ ∖ {2}))
36		elfznn 13470	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ∈ ℕ)
37	36	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℕ)
38	37	nncnd 12169	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℂ)
39		oddprm 16682	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑃 − 1) / 2) ∈ ℕ)
40	1, 39	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ)
41	40	nnnn0d 12473	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℕ₀)
42	41	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℕ₀)
43		2nn0 12430	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
44	43	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 2 ∈ ℕ₀)
45	38, 42, 44	expmuld 14054	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = ((𝑦↑2)↑((𝑃 − 1) / 2)))
46		prmnn 16550	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
47	2, 46	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℕ)
48	47	nnred 12168	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℝ)
49		peano2rem 11468	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
50	48, 49	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ)
51	50	recnd 11183	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 − 1) ∈ ℂ)
52		2cnd 12231	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
53		2ne0 12257	. . . . . . . . . . . . 13 ⊢ 2 ≠ 0
54	53	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≠ 0)
55	51, 52, 54	divcan2d 11933	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (𝑃 − 1))
56		phiprm 16649	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
57	2, 56	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1))
58	55, 57	eqtr4d 2779	. . . . . . . . . 10 ⊢ (𝜑 → (2 · ((𝑃 − 1) / 2)) = (ϕ‘𝑃))
59	58	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (2 · ((𝑃 − 1) / 2)) = (ϕ‘𝑃))
60	59	oveq2d 7373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦↑(2 · ((𝑃 − 1) / 2))) = (𝑦↑(ϕ‘𝑃)))
61	45, 60	eqtr3d 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑2)↑((𝑃 − 1) / 2)) = (𝑦↑(ϕ‘𝑃)))
62	61	oveq1d 7372	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (((𝑦↑2)↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑦↑(ϕ‘𝑃)) mod 𝑃))
63	2	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℙ)
64	63, 46	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℕ)
65	47	nnzd 12526	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ ℤ)
66	65	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℤ)
67	22, 66	gcdcomd 16394	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = (𝑃 gcd 𝑦))
68	37	nnred 12168	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ∈ ℝ)
69	50	rehalfcld 12400	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) / 2) ∈ ℝ)
70	69	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) ∈ ℝ)
71	48	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑃 ∈ ℝ)
72		elfzle2 13445	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (1...((𝑃 − 1) / 2)) → 𝑦 ≤ ((𝑃 − 1) / 2))
73	72	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 ≤ ((𝑃 − 1) / 2))
74		prmuz2 16572	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
75	2, 74	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘2))
76		uz2m1nn 12848	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ)
78	77	nnrpd 12955	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 − 1) ∈ ℝ⁺)
79		rphalflt 12944	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 − 1) ∈ ℝ⁺ → ((𝑃 − 1) / 2) < (𝑃 − 1))
80	78, 79	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑃 − 1) / 2) < (𝑃 − 1))
81	48	ltm1d 12087	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 − 1) < 𝑃)
82	69, 50, 48, 80, 81	lttrd 11316	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑃 − 1) / 2) < 𝑃)
83	82	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑃 − 1) / 2) < 𝑃)
84	68, 70, 71, 73, 83	lelttrd 11313	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → 𝑦 < 𝑃)
85	68, 71	ltnled 11302	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑦))
86	84, 85	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ≤ 𝑦)
87		dvdsle 16192	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦))
88	66, 37, 87	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦))
89	86, 88	mtod 197	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ¬ 𝑃 ∥ 𝑦)
90		coprm 16587	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ) → (¬ 𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1))
91	63, 22, 90	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (¬ 𝑃 ∥ 𝑦 ↔ (𝑃 gcd 𝑦) = 1))
92	89, 91	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑃 gcd 𝑦) = 1)
93	67, 92	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑦 gcd 𝑃) = 1)
94		eulerth 16655	. . . . . . 7 ⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ (𝑦 gcd 𝑃) = 1) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
95	64, 22, 93, 94	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → ((𝑦↑(ϕ‘𝑃)) mod 𝑃) = (1 mod 𝑃))
96	62, 95	eqtrd 2776	. . . . 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 26694	. . . 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 6857	. . . . . . . 8 ⊢ (𝜑 → (Base‘𝑌) ∈ V)
101	29, 26, 98, 17	evl1rhm 21698	. . . . . . . . . . 11 ⊢ (𝑌 ∈ CRing → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))))
102	10, 101	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))))
103	27, 99	rhmf 20158	. . . . . . . . . 10 ⊢ (𝑂 ∈ (𝑆 RingHom (𝑌 ↑_s (Base‘𝑌))) → 𝑂:𝐵⟶(Base‘(𝑌 ↑_s (Base‘𝑌))))
104	102, 103	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑂:𝐵⟶(Base‘(𝑌 ↑_s (Base‘𝑌))))
105	26	ply1ring 21619	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ Ring → 𝑆 ∈ Ring)
106	12, 105	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Ring)
107		ringgrp 19969	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp)
108	106, 107	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Grp)
109		eqid 2736	. . . . . . . . . . . . 13 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
110	109, 27	mgpbas 19902	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘(mulGrp‘𝑆))
111	109	ringmgp 19970	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
112	106, 111	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
113	31, 26, 27	vr1cl 21588	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ Ring → 𝑋 ∈ 𝐵)
114	12, 113	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
115	110, 30, 112, 41, 114	mulgnn0cld 18897	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵)
116	27, 33	ringidcl 19989	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Ring → 1 ∈ 𝐵)
117	106, 116	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ 𝐵)
118	27, 32	grpsubcl 18827	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Grp ∧ (((𝑃 − 1) / 2) ↑ 𝑋) ∈ 𝐵 ∧ 1 ∈ 𝐵) → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵)
119	108, 115, 117, 118	syl3anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑃 − 1) / 2) ↑ 𝑋) − 1 ) ∈ 𝐵)
120	34, 119	eqeltrid 2842	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ 𝐵)
121	104, 120	ffvelcdmd 7036	. . . . . . . 8 ⊢ (𝜑 → (𝑂‘𝑇) ∈ (Base‘(𝑌 ↑_s (Base‘𝑌))))
122	98, 17, 99, 5, 100, 121	pwselbas 17371	. . . . . . 7 ⊢ (𝜑 → (𝑂‘𝑇):(Base‘𝑌)⟶(Base‘𝑌))
123	122	ffnd 6669	. . . . . 6 ⊢ (𝜑 → (𝑂‘𝑇) Fn (Base‘𝑌))
124	123	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝑂‘𝑇) Fn (Base‘𝑌))
125		fniniseg 7010	. . . . 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 711	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...((𝑃 − 1) / 2))) → (𝐿‘(𝑦↑2)) ∈ (^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}))
128		lgsqr.g	. . 3 ⊢ 𝐺 = (𝑦 ∈ (1...((𝑃 − 1) / 2)) ↦ (𝐿‘(𝑦↑2)))
129	127, 128	fmptd 7062	. 2 ⊢ (𝜑 → 𝐺:(1...((𝑃 − 1) / 2))⟶(^◡(𝑂‘𝑇) “ {(0_g‘𝑌)}))
130		fvoveq1 7380	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑥↑2)))
131		fvex 6855	. . . . . . . 8 ⊢ (𝐿‘(𝑥↑2)) ∈ V
132	130, 128, 131	fvmpt 6948	. . . . . . 7 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2)))
133	132	ad2antrl 726	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝐺‘𝑥) = (𝐿‘(𝑥↑2)))
134		fvoveq1 7380	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝐿‘(𝑦↑2)) = (𝐿‘(𝑧↑2)))
135		fvex 6855	. . . . . . . 8 ⊢ (𝐿‘(𝑧↑2)) ∈ V
136	134, 128, 135	fvmpt 6948	. . . . . . 7 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → (𝐺‘𝑧) = (𝐿‘(𝑧↑2)))
137	136	ad2antll 727	. . . . . 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 12473	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
140	139	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ₀)
141		elfzelz 13441	. . . . . . . 8 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℤ)
142	141	ad2antrl 726	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℤ)
143		zsqcl 14034	. . . . . . 7 ⊢ (𝑥 ∈ ℤ → (𝑥↑2) ∈ ℤ)
144	142, 143	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥↑2) ∈ ℤ)
145		elfzelz 13441	. . . . . . . 8 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℤ)
146	145	ad2antll 727	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℤ)
147		zsqcl 14034	. . . . . . 7 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℤ)
148	146, 147	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑧↑2) ∈ ℤ)
149	3, 13	zndvds 20956	. . . . . 6 ⊢ ((𝑃 ∈ ℕ₀ ∧ (𝑥↑2) ∈ ℤ ∧ (𝑧↑2) ∈ ℤ) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2))))
150	140, 144, 148, 149	syl3anc 1371	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐿‘(𝑥↑2)) = (𝐿‘(𝑧↑2)) ↔ 𝑃 ∥ ((𝑥↑2) − (𝑧↑2))))
151		elfznn 13470	. . . . . . . . 9 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ∈ ℕ)
152	151	ad2antrl 726	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ)
153	152	nncnd 12169	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℂ)
154		elfznn 13470	. . . . . . . . 9 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ∈ ℕ)
155	154	ad2antll 727	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℕ)
156	155	nncnd 12169	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℂ)
157		subsq 14114	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧)))
158	153, 156, 157	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥↑2) − (𝑧↑2)) = ((𝑥 + 𝑧) · (𝑥 − 𝑧)))
159	158	breq2d 5117	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥↑2) − (𝑧↑2)) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧))))
160	138, 150, 159	3bitrd 304	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) ↔ 𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧))))
161	2	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℙ)
162	142, 146	zaddcld 12611	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℤ)
163	142, 146	zsubcld 12612	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 − 𝑧) ∈ ℤ)
164		euclemma 16589	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝑥 + 𝑧) ∈ ℤ ∧ (𝑥 − 𝑧) ∈ ℤ) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧))))
165	161, 162, 163, 164	syl3anc 1371	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) ↔ (𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧))))
166	161, 46	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℕ)
167	166	nnzd 12526	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℤ)
168	152, 155	nnaddcld 12205	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℕ)
169		dvdsle 16192	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ (𝑥 + 𝑧) ∈ ℕ) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧)))
170	167, 168, 169	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 + 𝑧) → 𝑃 ≤ (𝑥 + 𝑧)))
171	168	nnred 12168	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ∈ ℝ)
172	166	nnred 12168	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ)
173	172, 49	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℝ)
174	152	nnred 12168	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℝ)
175	155	nnred 12168	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℝ)
176	69	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) ∈ ℝ)
177		elfzle2 13445	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1...((𝑃 − 1) / 2)) → 𝑥 ≤ ((𝑃 − 1) / 2))
178	177	ad2antrl 726	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ≤ ((𝑃 − 1) / 2))
179		elfzle2 13445	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (1...((𝑃 − 1) / 2)) → 𝑧 ≤ ((𝑃 − 1) / 2))
180	179	ad2antll 727	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ≤ ((𝑃 − 1) / 2))
181	174, 175, 176, 176, 178, 180	le2addd 11774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)))
182	51	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) ∈ ℂ)
183	182	2halvesd 12399	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (((𝑃 − 1) / 2) + ((𝑃 − 1) / 2)) = (𝑃 − 1))
184	181, 183	breqtrd 5131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) ≤ (𝑃 − 1))
185	172	ltm1d 12087	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 − 1) < 𝑃)
186	171, 173, 172, 184, 185	lelttrd 11313	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 + 𝑧) < 𝑃)
187	171, 172	ltnled 11302	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 + 𝑧) < 𝑃 ↔ ¬ 𝑃 ≤ (𝑥 + 𝑧)))
188	186, 187	mpbid 231	. . . . . . . 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 16147	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧)))
192	166, 142, 146, 191	syl3anc 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑥 mod 𝑃) = (𝑧 mod 𝑃) ↔ 𝑃 ∥ (𝑥 − 𝑧)))
193	166	nnrpd 12955	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑃 ∈ ℝ⁺)
194	152	nnnn0d 12473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 ∈ ℕ₀)
195	194	nn0ge0d 12476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑥)
196	82	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 − 1) / 2) < 𝑃)
197	174, 176, 172, 178, 196	lelttrd 11313	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑥 < 𝑃)
198		modid 13801	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑃)) → (𝑥 mod 𝑃) = 𝑥)
199	174, 193, 195, 197, 198	syl22anc 837	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑥 mod 𝑃) = 𝑥)
200	155	nnnn0d 12473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 ∈ ℕ₀)
201	200	nn0ge0d 12476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 0 ≤ 𝑧)
202	175, 176, 172, 180, 196	lelttrd 11313	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → 𝑧 < 𝑃)
203		modid 13801	. . . . . . . . . 10 ⊢ (((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ⁺) ∧ (0 ≤ 𝑧 ∧ 𝑧 < 𝑃)) → (𝑧 mod 𝑃) = 𝑧)
204	175, 193, 201, 202, 203	syl22anc 837	. . . . . . . . 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 280	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) ↔ 𝑥 = 𝑧))
207	206	biimpd 228	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ (𝑥 − 𝑧) → 𝑥 = 𝑧))
208	190, 207	jaod 857	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝑃 ∥ (𝑥 + 𝑧) ∨ 𝑃 ∥ (𝑥 − 𝑧)) → 𝑥 = 𝑧))
209	165, 208	sylbid 239	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → (𝑃 ∥ ((𝑥 + 𝑧) · (𝑥 − 𝑧)) → 𝑥 = 𝑧))
210	160, 209	sylbid 239	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((𝑃 − 1) / 2)) ∧ 𝑧 ∈ (1...((𝑃 − 1) / 2)))) → ((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧))
211	210	ralrimivva 3197	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (1...((𝑃 − 1) / 2))∀𝑧 ∈ (1...((𝑃 − 1) / 2))((𝐺‘𝑥) = (𝐺‘𝑧) → 𝑥 = 𝑧))
212		dff13 7202	. 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 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 Vcvv 3445 ∖ cdif 3907 {csn 4586 class class class wbr 5105 ↦ cmpt 5188 ^◡ccnv 5632 “ cima 5636 Fn wfn 6491 ⟶wf 6492 –1-1→wf1 6493 ‘cfv 6496 (class class class)co 7357 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 < clt 11189 ≤ cle 11190 − cmin 11385 / cdiv 11812 ℕcn 12153 2c2 12208 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 ℝ⁺crp 12915 ...cfz 13424 mod cmo 13774 ↑cexp 13967 ∥ cdvds 16136 gcd cgcd 16374 ℙcprime 16547 ϕcphi 16636 Basecbs 17083 0_gc0g 17321 ↑_s cpws 17328 Mndcmnd 18556 Grpcgrp 18748 -_gcsg 18750 ._gcmg 18872 mulGrpcmgp 19896 1_rcur 19913 Ringcrg 19964 CRingccrg 19965 RingHom crh 20143 Fieldcfield 20186 Domncdomn 20750 IDomncidom 20751 ℤ_ringczring 20869 ℤRHomczrh 20900 ℤ/nℤczn 20903 var₁cv1 21547 Poly₁cpl1 21548 eval₁ce1 21680 deg₁ cdg1 25416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129 ax-addf 11130 ax-mulf 11131

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-ofr 7618 df-om 7803 df-1st 7921 df-2nd 7922 df-supp 8093 df-tpos 8157 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-oadd 8416 df-er 8648 df-ec 8650 df-qs 8654 df-map 8767 df-pm 8768 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9306 df-sup 9378 df-inf 9379 df-oi 9446 df-dju 9837 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-xnn0 12486 df-z 12500 df-dec 12619 df-uz 12764 df-rp 12916 df-fz 13425 df-fzo 13568 df-fl 13697 df-mod 13775 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-dvds 16137 df-gcd 16375 df-prm 16548 df-phi 16638 df-struct 17019 df-sets 17036 df-slot 17054 df-ndx 17066 df-base 17084 df-ress 17113 df-plusg 17146 df-mulr 17147 df-starv 17148 df-sca 17149 df-vsca 17150 df-ip 17151 df-tset 17152 df-ple 17153 df-ds 17155 df-unif 17156 df-hom 17157 df-cco 17158 df-0g 17323 df-gsum 17324 df-prds 17329 df-pws 17331 df-imas 17390 df-qus 17391 df-mre 17466 df-mrc 17467 df-acs 17469 df-mgm 18497 df-sgrp 18546 df-mnd 18557 df-mhm 18601 df-submnd 18602 df-grp 18751 df-minusg 18752 df-sbg 18753 df-mulg 18873 df-subg 18925 df-nsg 18926 df-eqg 18927 df-ghm 19006 df-cntz 19097 df-cmn 19564 df-abl 19565 df-mgp 19897 df-ur 19914 df-srg 19918 df-ring 19966 df-cring 19967 df-oppr 20049 df-dvdsr 20070 df-unit 20071 df-invr 20101 df-dvr 20112 df-rnghom 20146 df-drng 20187 df-field 20188 df-subrg 20220 df-lmod 20324 df-lss 20393 df-lsp 20433 df-sra 20633 df-rgmod 20634 df-lidl 20635 df-rsp 20636 df-2idl 20702 df-nzr 20728 df-rlreg 20753 df-domn 20754 df-idom 20755 df-cnfld 20797 df-zring 20870 df-zrh 20904 df-zn 20907 df-assa 21259 df-asp 21260 df-ascl 21261 df-psr 21311 df-mvr 21312 df-mpl 21313 df-opsr 21315 df-evls 21482 df-evl 21483 df-psr1 21551 df-vr1 21552 df-ply1 21553 df-evl1 21682

This theorem is referenced by: lgsqrlem4 26697

W3C validator