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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 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 ringmgp ⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
112 107 111 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
113 7 2 3 vr1cl ⊢ ( 𝑌 ∈ Ring → 𝑋 ∈ 𝐵 )
114 23 113 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
115 110 3 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
116 115 6 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑆 ) ∈ Mnd ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) ∈ 𝐵 )
117 112 42 114 116 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) ∈ 𝐵 )
118 3 9 ringidcl ⊢ ( 𝑆 ∈ Ring → 1 ∈ 𝐵 )
119 107 118 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )
120 3 8 grpsubcl ⊢ ( ( 𝑆 ∈ Grp ∧ ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) ∈ 𝐵 ∧ 1 ∈ 𝐵 ) → ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 ) ∈ 𝐵 )
121 109 117 119 120 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑃 − 1 ) / 2 ) ↑ 𝑋 ) − 1 ) ∈ 𝐵 )
122 10 121 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
123 105 122 ffvelrnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) ∈ ( Base ‘ ( 𝑌 ↑s ( Base ‘ 𝑌 ) ) ) )
124 99 27 100 16 101 123 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑌 ) )
125 124 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑇 ) Fn ( Base ‘ 𝑌 ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝑂 ‘ 𝑇 ) Fn ( Base ‘ 𝑌 ) )
127 fniniseg ⊢ ( ( 𝑂 ‘ 𝑇 ) Fn ( Base ‘ 𝑌 ) → ( ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ↔ ( ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑂 ‘ 𝑇 ) ‘ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ) = ( 0g ‘ 𝑌 ) ) ) )
128 126 127 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ↔ ( ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( Base ‘ 𝑌 ) ∧ ( ( 𝑂 ‘ 𝑇 ) ‘ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ) = ( 0g ‘ 𝑌 ) ) ) )
129 35 98 128 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ∈ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )
130 129 13 fmptd ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )
131 fvoveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
132 fvex ⊢ ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) ∈ V
133 131 13 132 fvmpt ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
134 133 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
135 fvoveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) )
136 fvex ⊢ ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) ∈ V
137 135 13 136 fvmpt ⊢ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) )
138 137 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) )
139 134 138 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) ) )
140 48 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
141 140 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℕ0 )
142 elfzelz ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℤ )
143 142 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℤ )
144 zsqcl ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ↑ 2 ) ∈ ℤ )
145 143 144 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℤ )
146 elfzelz ⊢ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑧 ∈ ℤ )
147 146 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℤ )
148 zsqcl ⊢ ( 𝑧 ∈ ℤ → ( 𝑧 ↑ 2 ) ∈ ℤ )
149 147 148 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑧 ↑ 2 ) ∈ ℤ )
150 1 11 zndvds ⊢ ( ( 𝑃 ∈ ℕ0 ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ ( 𝑧 ↑ 2 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) ) )
151 141 145 149 150 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑧 ↑ 2 ) ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) ) )
152 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ∈ ℕ )
153 152 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℕ )
154 153 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℂ )
155 elfznn ⊢ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑧 ∈ ℕ )
156 155 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℕ )
157 156 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℂ )
158 subsq ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) = ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) )
159 154 157 158 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) = ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) )
160 159 breq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − ( 𝑧 ↑ 2 ) ) ↔ 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) ) )
161 139 151 160 3bitrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) ↔ 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) ) )
162 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℙ )
163 143 147 zaddcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ∈ ℤ )
164 143 147 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 − 𝑧 ) ∈ ℤ )
165 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 + 𝑧 ) ∈ ℤ ∧ ( 𝑥 − 𝑧 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) ↔ ( 𝑃 ∥ ( 𝑥 + 𝑧 ) ∨ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) ) )
166 162 163 164 165 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) ↔ ( 𝑃 ∥ ( 𝑥 + 𝑧 ) ∨ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) ) )
167 162 47 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℕ )
168 167 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℤ )
169 153 156 nnaddcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ∈ ℕ )
170 dvdsle ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑥 + 𝑧 ) ∈ ℕ ) → ( 𝑃 ∥ ( 𝑥 + 𝑧 ) → 𝑃 ≤ ( 𝑥 + 𝑧 ) ) )
171 168 169 170 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑥 + 𝑧 ) → 𝑃 ≤ ( 𝑥 + 𝑧 ) ) )
172 169 nnred ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ∈ ℝ )
173 167 nnred ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℝ )
174 173 50 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 − 1 ) ∈ ℝ )
175 153 nnred ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℝ )
176 156 nnred ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℝ )
177 70 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
178 elfzle2 ⊢ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
179 178 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
180 elfzle2 ⊢ ( 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝑧 ≤ ( ( 𝑃 − 1 ) / 2 ) )
181 180 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ≤ ( ( 𝑃 − 1 ) / 2 ) )
182 175 176 177 177 179 181 le2addd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ≤ ( ( ( 𝑃 − 1 ) / 2 ) + ( ( 𝑃 − 1 ) / 2 ) ) )
183 52 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 − 1 ) ∈ ℂ )
184 183 2halvesd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( ( 𝑃 − 1 ) / 2 ) + ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑃 − 1 ) )
185 182 184 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) ≤ ( 𝑃 − 1 ) )
186 173 ltm1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 − 1 ) < 𝑃 )
187 172 174 173 185 186 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 + 𝑧 ) < 𝑃 )
188 172 173 ltnled ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 + 𝑧 ) < 𝑃 ↔ ¬ 𝑃 ≤ ( 𝑥 + 𝑧 ) ) )
189 187 188 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ¬ 𝑃 ≤ ( 𝑥 + 𝑧 ) )
190 189 pm2.21d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ≤ ( 𝑥 + 𝑧 ) → 𝑥 = 𝑧 ) )
191 171 190 syld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑥 + 𝑧 ) → 𝑥 = 𝑧 ) )
192 moddvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( ( 𝑥 mod 𝑃 ) = ( 𝑧 mod 𝑃 ) ↔ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) )
193 167 143 147 192 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 mod 𝑃 ) = ( 𝑧 mod 𝑃 ) ↔ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) )
194 167 nnrpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑃 ∈ ℝ+ )
195 153 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 ∈ ℕ0 )
196 195 nn0ge0d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 0 ≤ 𝑥 )
197 83 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 − 1 ) / 2 ) < 𝑃 )
198 175 177 173 179 197 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑥 < 𝑃 )
199 modid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < 𝑃 ) ) → ( 𝑥 mod 𝑃 ) = 𝑥 )
200 175 194 196 198 199 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑥 mod 𝑃 ) = 𝑥 )
201 156 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 ∈ ℕ0 )
202 201 nn0ge0d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 0 ≤ 𝑧 )
203 176 177 173 181 197 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → 𝑧 < 𝑃 )
204 modid ⊢ ( ( ( 𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑧 ∧ 𝑧 < 𝑃 ) ) → ( 𝑧 mod 𝑃 ) = 𝑧 )
205 176 194 202 203 204 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑧 mod 𝑃 ) = 𝑧 )
206 200 205 eqeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑥 mod 𝑃 ) = ( 𝑧 mod 𝑃 ) ↔ 𝑥 = 𝑧 ) )
207 193 206 bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑥 − 𝑧 ) ↔ 𝑥 = 𝑧 ) )
208 207 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( 𝑥 − 𝑧 ) → 𝑥 = 𝑧 ) )
209 191 208 jaod ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝑃 ∥ ( 𝑥 + 𝑧 ) ∨ 𝑃 ∥ ( 𝑥 − 𝑧 ) ) → 𝑥 = 𝑧 ) )
210 166 209 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( 𝑃 ∥ ( ( 𝑥 + 𝑧 ) · ( 𝑥 − 𝑧 ) ) → 𝑥 = 𝑧 ) )
211 161 210 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∧ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) → 𝑥 = 𝑧 ) )
212 211 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) → 𝑥 = 𝑧 ) )
213 dff13 ⊢ ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ↔ ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ⟶ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) ∧ ∀ 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∀ 𝑧 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) → 𝑥 = 𝑧 ) ) )
214 130 212 213 sylanbrc ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ◡ ( 𝑂 ‘ 𝑇 ) “ { ( 0g ‘ 𝑌 ) } ) )