Metamath Proof Explorer

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 ‘ 𝑌 ) } ) )