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