Theorem lgsqrlem2

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

	Ref	Expression
Hypotheses	lgsqr.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑃 )
	lgsqr.s	⊢ 𝑆 = ( Poly1 ‘ 𝑌 )
	lgsqr.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	lgsqr.d	⊢ 𝐷 = ( deg1 ‘ 𝑌 )
	lgsqr.o	⊢ 𝑂 = ( eval1 ‘ 𝑌 )
	lgsqr.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
	lgsqr.x	⊢ 𝑋 = ( var1 ‘ 𝑌 )
	lgsqr.m	⊢ − = ( -g ‘ 𝑆 )
	lgsqr.u	⊢ 1 = ( 1r ‘ 𝑆 )
	lgsqr.t	⊢ 𝑇 = ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 )
	lgsqr.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
	lgsqr.1	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
	lgsqr.g	⊢ 𝐺 = ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) )
Assertion	lgsqrlem2	⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		lgsqr.y	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑃 )
2		lgsqr.s	⊢ 𝑆 = ( Poly1 ‘ 𝑌 )
3		lgsqr.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		lgsqr.d	⊢ 𝐷 = ( deg1 ‘ 𝑌 )
5		lgsqr.o	⊢ 𝑂 = ( eval1 ‘ 𝑌 )
6		lgsqr.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
7		lgsqr.x	⊢ 𝑋 = ( var1 ‘ 𝑌 )
8		lgsqr.m	⊢ − = ( -g ‘ 𝑆 )
9		lgsqr.u	⊢ 1 = ( 1r ‘ 𝑆 )
10		lgsqr.t	⊢ 𝑇 = ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 )
11		lgsqr.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
12		lgsqr.1	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
13		lgsqr.g	⊢ 𝐺 = ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) )
14	12	eldifad	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
15	1	znfld	⊢ ( 𝑃 ∈ ℙ → 𝑌 ∈ Field )
16	14 15	syl	⊢ ( 𝜑 → 𝑌 ∈ Field )
17		fldidom	⊢ ( 𝑌 ∈ Field → 𝑌 ∈ IDomn )
18	16 17	syl	⊢ ( 𝜑 → 𝑌 ∈ IDomn )
19		isidom	⊢ ( 𝑌 ∈ IDomn ↔ ( 𝑌 ∈ CRing ∧ 𝑌 ∈ Domn ) )
20	19	simplbi	⊢ ( 𝑌 ∈ IDomn → 𝑌 ∈ CRing )
21	18 20	syl	⊢ ( 𝜑 → 𝑌 ∈ CRing )
22		crngring	⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
23	21 22	syl	⊢ ( 𝜑 → 𝑌 ∈ Ring )
24	11	zrhrhm	⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
25	23 24	syl	⊢ ( 𝜑 → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
26		zringbas	⊢ ℤ = ( Base ‘ ℤring )
27		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
28	26 27	rhmf	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
29	25 28	syl	⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
31		elfzelz	⊢ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑦 ∈ ℤ )
32	31	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑦 ∈ ℤ )
33		zsqcl	⊢ ( 𝑦 ∈ ℤ → ( 𝑦 ↑ 2 ) ∈ ℤ )
34	32 33	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑦 ↑ 2 ) ∈ ℤ )
35	30 34	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( Base ‘ 𝑌 ) )
36	12	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
37		elfznn	⊢ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑦 ∈ ℕ )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑦 ∈ ℕ )
39	38	nncnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑦 ∈ ℂ )
40		oddprm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
41	12 40	syl	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
42	41	nnnn0d	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
44		2nn0	⊢ 2 ∈ ℕ0
45	44	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 2 ∈ ℕ0 )
46	39 43 45	expmuld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑦 ↑ ( 2 · ( ( 𝑃 − 1 ) / 2 ) ) ) = ( ( 𝑦 ↑ 2 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
47		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
48	14 47	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
49	48	nnred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
50		peano2rem	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
51	49 50	syl	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
52	51	recnd	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℂ )
53		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
54		2ne0	⊢ 2 ≠ 0
55	54	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
56	52 53 55	divcan2d	⊢ ( 𝜑 → ( 2 · ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑃 − 1 ) )
57		phiprm	⊢ ( 𝑃 ∈ ℙ → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
58	14 57	syl	⊢ ( 𝜑 → ( ϕ ‘ 𝑃 ) = ( 𝑃 − 1 ) )
59	56 58	eqtr4d	⊢ ( 𝜑 → ( 2 · ( ( 𝑃 − 1 ) / 2 ) ) = ( ϕ ‘ 𝑃 ) )
60	59	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 2 · ( ( 𝑃 − 1 ) / 2 ) ) = ( ϕ ‘ 𝑃 ) )
61	60	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑦 ↑ ( 2 · ( ( 𝑃 − 1 ) / 2 ) ) ) = ( 𝑦 ↑ ( ϕ ‘ 𝑃 ) ) )
62	46 61	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑦 ↑ 2 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑦 ↑ ( ϕ ‘ 𝑃 ) ) )
63	62	oveq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( 𝑦 ↑ 2 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( 𝑦 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) )
64	14	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℙ )
65	64 47	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℕ )
66	48	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
67	66	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℤ )
68	32 67	gcdcomd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑦 gcd 𝑃 ) = ( 𝑃 gcd 𝑦 ) )
69	38	nnred	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑦 ∈ ℝ )
70	51	rehalfcld	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
71	70	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
72	49	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑃 ∈ ℝ )
73		elfzle2	⊢ ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) )
74	73	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) )
75		prmuz2	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
76	14 75	syl	⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
77		uz2m1nn	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ )
78	76 77	syl	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ )
79	78	nnrpd	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ+ )
80		rphalflt	⊢ ( ( 𝑃 − 1 ) ∈ ℝ+ → ( ( 𝑃 − 1 ) / 2 ) < ( 𝑃 − 1 ) )
81	79 80	syl	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) < ( 𝑃 − 1 ) )
82	49	ltm1d	⊢ ( 𝜑 → ( 𝑃 − 1 ) < 𝑃 )
83	70 51 49 81 82	lttrd	⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) < 𝑃 )
84	83	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑃 − 1 ) / 2 ) < 𝑃 )
85	69 71 72 74 84	lelttrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → 𝑦 < 𝑃 )
86	69 72	ltnled	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑦 < 𝑃 ↔ ¬ 𝑃 ≤ 𝑦 ) )
87	85 86	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ≤ 𝑦 )
88		dvdsle	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦 ) )
89	67 38 88	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 ∥ 𝑦 → 𝑃 ≤ 𝑦 ) )
90	87 89	mtod	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ¬ 𝑃 ∥ 𝑦 )
91		coprm	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑦 ↔ ( 𝑃 gcd 𝑦 ) = 1 ) )
92	64 32 91	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ¬ 𝑃 ∥ 𝑦 ↔ ( 𝑃 gcd 𝑦 ) = 1 ) )
93	90 92	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑃 gcd 𝑦 ) = 1 )
94	68 93	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑦 gcd 𝑃 ) = 1 )
95		eulerth	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑦 ∈ ℤ ∧ ( 𝑦 gcd 𝑃 ) = 1 ) → ( ( 𝑦 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
96	65 32 94 95	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑦 ↑ ( ϕ ‘ 𝑃 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
97	63 96	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( ( 𝑦 ↑ 2 ) ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( 1 mod 𝑃 ) )
98	1 2 3 4 5 6 7 8 9 10 11 36 34 97	lgsqrlem1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝑂 ‘ 𝑇 ) ‘ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ) = ( 0g ‘ 𝑌 ) )
99		eqid	⊢ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) = ( 𝑌 ↑s ( Base ‘ 𝑌 ) )
100		eqid	⊢ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) = ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) )
101		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑌 ) ∈ V )
102	5 2 99 27	evl1rhm	⊢ ( 𝑌 ∈ CRing → 𝑂 ∈ ( 𝑆 RingHom ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
103	21 102	syl	⊢ ( 𝜑 → 𝑂 ∈ ( 𝑆 RingHom ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
104	3 100	rhmf	⊢ ( 𝑂 ∈ ( 𝑆 RingHom ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
105	103 104	syl	⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
106	2	ply1ring	⊢ ( 𝑌 ∈ Ring → 𝑆 ∈ Ring )
107	23 106	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
108		ringgrp	⊢ ( 𝑆 ∈ Ring → 𝑆 ∈ Grp )
109	107 108	syl	⊢ ( 𝜑 → 𝑆 ∈ Grp )
110		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
111	110 3	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
112	110	ringmgp	⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
113	107 112	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
114	7 2 3	vr1cl	⊢ ( 𝑌 ∈ Ring → 𝑋 ∈ 𝐵 )
115	23 114	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
116	111 6 113 42 115	mulgnn0cld	⊢ ( 𝜑 → ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) ∈ 𝐵 )
117	3 9	ringidcl	⊢ ( 𝑆 ∈ Ring → 1 ∈ 𝐵 )
118	107 117	syl	⊢ ( 𝜑 → 1 ∈ 𝐵 )
119	3 8	grpsubcl	⊢ ( ( 𝑆 ∈ Grp ∧ ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) ∈ 𝐵 ∧ 1 ∈ 𝐵 ) → ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 ) ∈ 𝐵 )
120	109 116 118 119	syl3anc	⊢ ( 𝜑 → ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 ) ∈ 𝐵 )
121	10 120	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
122	105 121	ffvelcdmd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) ∈ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
123	99 27 100 16 101 122	pwselbas	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑌 ) )
124	123	ffnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) Fn ( Base ‘ 𝑌 ) )
125	124	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑂 ‘ 𝑇 ) Fn ( Base ‘ 𝑌 ) )
126		fniniseg	⊢ ( ( 𝑂 ‘ 𝑇 ) Fn ( Base ‘ 𝑌 ) → ( ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ↔ ( ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑂 ‘ 𝑇 ) ‘ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ) = ( 0g ‘ 𝑌 ) ) ) )
127	125 126	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ↔ ( ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑂 ‘ 𝑇 ) ‘ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ) = ( 0g ‘ 𝑌 ) ) ) )
128	35 98 127	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )
129	128 13	fmptd	⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )
130		fvoveq1	⊢ ( 𝑦 = 𝑥 → ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
131		fvex	⊢ ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) ∈ V
132	130 13 131	fvmpt	⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
133	132	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
134		fvoveq1	⊢ ( 𝑦 = 𝑧 → ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) )
135		fvex	⊢ ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) ∈ V
136	134 13 135	fvmpt	⊢ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) )
137	136	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) )
138	133 137	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) ) )
139	48	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
140	139	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℕ0 )
141		elfzelz	⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℤ )
142	141	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℤ )
143		zsqcl	⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ↑ 2 ) ∈ ℤ )
144	142 143	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℤ )
145		elfzelz	⊢ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑧 ∈ ℤ )
146	145	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℤ )
147		zsqcl	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 ↑ 2 ) ∈ ℤ )
148	146 147	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑧 ↑ 2 ) ∈ ℤ )
149	1 11	zndvds	⊢ ( ( 𝑃 ∈ ℕ0 ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ ( 𝑧 ↑ 2 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) ) )
150	140 144 148 149	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) ) )
151		elfznn	⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℕ )
152	151	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℕ )
153	152	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℂ )
154		elfznn	⊢ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑧 ∈ ℕ )
155	154	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℕ )
156	155	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℂ )
157		subsq	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) = ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) )
158	153 156 157	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) = ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) )
159	158	breq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) ↔ 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) ) )
160	138 150 159	3bitrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) ↔ 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) ) )
161	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℙ )
162	142 146	zaddcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ∈ ℤ )
163	142 146	zsubcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 − 𝑧 ) ∈ ℤ )
164		euclemma	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 + 𝑧 ) ∈ ℤ ∧ ( 𝑥 − 𝑧 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) ↔ ( 𝑃 ∥ ( 𝑥 + 𝑧 ) ∨ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) ) )
165	161 162 163 164	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) ↔ ( 𝑃 ∥ ( 𝑥 + 𝑧 ) ∨ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) ) )
166	161 47	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℕ )
167	166	nnzd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℤ )
168	152 155	nnaddcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ∈ ℕ )
169		dvdsle	⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑥 + 𝑧 ) ∈ ℕ ) → ( 𝑃 ∥ ( 𝑥 + 𝑧 ) → 𝑃 ≤ ( 𝑥 + 𝑧 ) ) )
170	167 168 169	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑥 + 𝑧 ) → 𝑃 ≤ ( 𝑥 + 𝑧 ) ) )
171	168	nnred	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ∈ ℝ )
172	166	nnred	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℝ )
173	172 50	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 − 1 ) ∈ ℝ )
174	152	nnred	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℝ )
175	155	nnred	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℝ )
176	70	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
177		elfzle2	⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
178	177	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
179		elfzle2	⊢ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑧 ≤ ( ( 𝑃 − 1 ) / 2 ) )
180	179	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ≤ ( ( 𝑃 − 1 ) / 2 ) )
181	174 175 176 176 178 180	le2addd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) + ( ( 𝑃 − 1 ) / 2 ) ) )
182	52	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 − 1 ) ∈ ℂ )
183	182	2halvesd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 𝑃 − 1 ) / 2 ) + ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑃 − 1 ) )
184	181 183	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ≤ ( 𝑃 − 1 ) )
185	172	ltm1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 − 1 ) < 𝑃 )
186	171 173 172 184 185	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) < 𝑃 )
187	171 172	ltnled	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 + 𝑧 ) < 𝑃 ↔ ¬ 𝑃 ≤ ( 𝑥 + 𝑧 ) ) )
188	186 187	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ¬ 𝑃 ≤ ( 𝑥 + 𝑧 ) )
189	188	pm2.21d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ≤ ( 𝑥 + 𝑧 ) → 𝑥 = 𝑧 ) )
190	170 189	syld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑥 + 𝑧 ) → 𝑥 = 𝑧 ) )
191		moddvds	⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑥 mod 𝑃 ) = ( 𝑧 mod 𝑃 ) ↔ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) )
192	166 142 146 191	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 mod 𝑃 ) = ( 𝑧 mod 𝑃 ) ↔ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) )
193	166	nnrpd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℝ+ )
194	152	nnnn0d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℕ0 )
195	194	nn0ge0d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 0 ≤ 𝑥 )
196	83	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 − 1 ) / 2 ) < 𝑃 )
197	174 176 172 178 196	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 < 𝑃 )
198		modid	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < 𝑃 ) ) → ( 𝑥 mod 𝑃 ) = 𝑥 )
199	174 193 195 197 198	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 mod 𝑃 ) = 𝑥 )
200	155	nnnn0d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℕ0 )
201	200	nn0ge0d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 0 ≤ 𝑧 )
202	175 176 172 180 196	lelttrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 < 𝑃 )
203		modid	⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑧 ∧ 𝑧 < 𝑃 ) ) → ( 𝑧 mod 𝑃 ) = 𝑧 )
204	175 193 201 202 203	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑧 mod 𝑃 ) = 𝑧 )
205	199 204	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 mod 𝑃 ) = ( 𝑧 mod 𝑃 ) ↔ 𝑥 = 𝑧 ) )
206	192 205	bitr3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑥 − 𝑧 ) ↔ 𝑥 = 𝑧 ) )
207	206	biimpd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑥 − 𝑧 ) → 𝑥 = 𝑧 ) )
208	190 207	jaod	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 ∥ ( 𝑥 + 𝑧 ) ∨ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) → 𝑥 = 𝑧 ) )
209	165 208	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) → 𝑥 = 𝑧 ) )
210	160 209	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) → 𝑥 = 𝑧 ) )
211	210	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) → 𝑥 = 𝑧 ) )
212		dff13	⊢ ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ↔ ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ∧ ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) → 𝑥 = 𝑧 ) ) )
213	129 211 212	sylanbrc	⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )