Metamath Proof Explorer


Theorem lgsqrlem4

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 ) ) )
lgsqr.3 ( 𝜑𝐴 ∈ ℤ )
lgsqr.4 ( 𝜑 → ( 𝐴 /L 𝑃 ) = 1 )
Assertion lgsqrlem4 ( 𝜑 → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) )

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 lgsqr.3 ( 𝜑𝐴 ∈ ℤ )
15 lgsqr.4 ( 𝜑 → ( 𝐴 /L 𝑃 ) = 1 )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 lgsqrlem2 ( 𝜑𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) )
17 fvex ( 𝑂𝑇 ) ∈ V
18 17 cnvex ( 𝑂𝑇 ) ∈ V
19 18 imaex ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∈ V
20 19 f1dom ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) → ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ≼ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) )
21 16 20 syl ( 𝜑 → ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ≼ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) )
22 eqid ( 0g𝑌 ) = ( 0g𝑌 )
23 eqid ( 0g𝑆 ) = ( 0g𝑆 )
24 12 eldifad ( 𝜑𝑃 ∈ ℙ )
25 1 znfld ( 𝑃 ∈ ℙ → 𝑌 ∈ Field )
26 24 25 syl ( 𝜑𝑌 ∈ Field )
27 fldidom ( 𝑌 ∈ Field → 𝑌 ∈ IDomn )
28 26 27 syl ( 𝜑𝑌 ∈ IDomn )
29 isidom ( 𝑌 ∈ IDomn ↔ ( 𝑌 ∈ CRing ∧ 𝑌 ∈ Domn ) )
30 29 simplbi ( 𝑌 ∈ IDomn → 𝑌 ∈ CRing )
31 28 30 syl ( 𝜑𝑌 ∈ CRing )
32 crngring ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
33 31 32 syl ( 𝜑𝑌 ∈ Ring )
34 2 ply1ring ( 𝑌 ∈ Ring → 𝑆 ∈ Ring )
35 33 34 syl ( 𝜑𝑆 ∈ Ring )
36 ringgrp ( 𝑆 ∈ Ring → 𝑆 ∈ Grp )
37 35 36 syl ( 𝜑𝑆 ∈ Grp )
38 eqid ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
39 38 3 mgpbas 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
40 38 ringmgp ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
41 35 40 syl ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
42 oddprm ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
43 12 42 syl ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
44 43 nnnn0d ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
45 7 2 3 vr1cl ( 𝑌 ∈ Ring → 𝑋𝐵 )
46 33 45 syl ( 𝜑𝑋𝐵 )
47 39 6 41 44 46 mulgnn0cld ( 𝜑 → ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) ∈ 𝐵 )
48 3 9 ringidcl ( 𝑆 ∈ Ring → 1𝐵 )
49 35 48 syl ( 𝜑1𝐵 )
50 3 8 grpsubcl ( ( 𝑆 ∈ Grp ∧ ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) ∈ 𝐵1𝐵 ) → ( ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) 1 ) ∈ 𝐵 )
51 37 47 49 50 syl3anc ( 𝜑 → ( ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) 1 ) ∈ 𝐵 )
52 10 51 eqeltrid ( 𝜑𝑇𝐵 )
53 10 fveq2i ( 𝐷𝑇 ) = ( 𝐷 ‘ ( ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) 1 ) )
54 43 nngt0d ( 𝜑 → 0 < ( ( 𝑃 − 1 ) / 2 ) )
55 eqid ( algSc ‘ 𝑆 ) = ( algSc ‘ 𝑆 )
56 eqid ( 1r𝑌 ) = ( 1r𝑌 )
57 2 55 56 9 ply1scl1 ( 𝑌 ∈ Ring → ( ( algSc ‘ 𝑆 ) ‘ ( 1r𝑌 ) ) = 1 )
58 33 57 syl ( 𝜑 → ( ( algSc ‘ 𝑆 ) ‘ ( 1r𝑌 ) ) = 1 )
59 58 fveq2d ( 𝜑 → ( 𝐷 ‘ ( ( algSc ‘ 𝑆 ) ‘ ( 1r𝑌 ) ) ) = ( 𝐷1 ) )
60 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
61 60 56 ringidcl ( 𝑌 ∈ Ring → ( 1r𝑌 ) ∈ ( Base ‘ 𝑌 ) )
62 33 61 syl ( 𝜑 → ( 1r𝑌 ) ∈ ( Base ‘ 𝑌 ) )
63 domnnzr ( 𝑌 ∈ Domn → 𝑌 ∈ NzRing )
64 29 63 simplbiim ( 𝑌 ∈ IDomn → 𝑌 ∈ NzRing )
65 28 64 syl ( 𝜑𝑌 ∈ NzRing )
66 56 22 nzrnz ( 𝑌 ∈ NzRing → ( 1r𝑌 ) ≠ ( 0g𝑌 ) )
67 65 66 syl ( 𝜑 → ( 1r𝑌 ) ≠ ( 0g𝑌 ) )
68 4 2 60 55 22 deg1scl ( ( 𝑌 ∈ Ring ∧ ( 1r𝑌 ) ∈ ( Base ‘ 𝑌 ) ∧ ( 1r𝑌 ) ≠ ( 0g𝑌 ) ) → ( 𝐷 ‘ ( ( algSc ‘ 𝑆 ) ‘ ( 1r𝑌 ) ) ) = 0 )
69 33 62 67 68 syl3anc ( 𝜑 → ( 𝐷 ‘ ( ( algSc ‘ 𝑆 ) ‘ ( 1r𝑌 ) ) ) = 0 )
70 59 69 eqtr3d ( 𝜑 → ( 𝐷1 ) = 0 )
71 4 2 7 38 6 deg1pw ( ( 𝑌 ∈ NzRing ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) → ( 𝐷 ‘ ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) ) = ( ( 𝑃 − 1 ) / 2 ) )
72 65 44 71 syl2anc ( 𝜑 → ( 𝐷 ‘ ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) ) = ( ( 𝑃 − 1 ) / 2 ) )
73 54 70 72 3brtr4d ( 𝜑 → ( 𝐷1 ) < ( 𝐷 ‘ ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) ) )
74 2 4 33 3 8 47 49 73 deg1sub ( 𝜑 → ( 𝐷 ‘ ( ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) 1 ) ) = ( 𝐷 ‘ ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) ) )
75 53 74 eqtrid ( 𝜑 → ( 𝐷𝑇 ) = ( 𝐷 ‘ ( ( ( 𝑃 − 1 ) / 2 ) 𝑋 ) ) )
76 75 72 eqtrd ( 𝜑 → ( 𝐷𝑇 ) = ( ( 𝑃 − 1 ) / 2 ) )
77 76 44 eqeltrd ( 𝜑 → ( 𝐷𝑇 ) ∈ ℕ0 )
78 4 2 23 3 deg1nn0clb ( ( 𝑌 ∈ Ring ∧ 𝑇𝐵 ) → ( 𝑇 ≠ ( 0g𝑆 ) ↔ ( 𝐷𝑇 ) ∈ ℕ0 ) )
79 33 52 78 syl2anc ( 𝜑 → ( 𝑇 ≠ ( 0g𝑆 ) ↔ ( 𝐷𝑇 ) ∈ ℕ0 ) )
80 77 79 mpbird ( 𝜑𝑇 ≠ ( 0g𝑆 ) )
81 2 3 4 5 22 23 28 52 80 fta1g ( 𝜑 → ( ♯ ‘ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) ≤ ( 𝐷𝑇 ) )
82 81 76 breqtrd ( 𝜑 → ( ♯ ‘ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
83 hashfz1 ( ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) )
84 44 83 syl ( 𝜑 → ( ♯ ‘ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) = ( ( 𝑃 − 1 ) / 2 ) )
85 82 84 breqtrrd ( 𝜑 → ( ♯ ‘ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) ≤ ( ♯ ‘ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) )
86 hashbnd ( ( ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∈ V ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ∧ ( ♯ ‘ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) → ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∈ Fin )
87 19 44 82 86 mp3an2i ( 𝜑 → ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∈ Fin )
88 fzfid ( 𝜑 → ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ Fin )
89 hashdom ( ( ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∈ Fin ∧ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ∈ Fin ) → ( ( ♯ ‘ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) ≤ ( ♯ ‘ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ↔ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ≼ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) )
90 87 88 89 syl2anc ( 𝜑 → ( ( ♯ ‘ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) ≤ ( ♯ ‘ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) ↔ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ≼ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) )
91 85 90 mpbid ( 𝜑 → ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ≼ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
92 sbth ( ( ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ≼ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∧ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ≼ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ) → ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ≈ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) )
93 21 91 92 syl2anc ( 𝜑 → ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ≈ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) )
94 f1finf1o ( ( ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ≈ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∧ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∈ Fin ) → ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ↔ 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) )
95 93 87 94 syl2anc ( 𝜑 → ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ↔ 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) )
96 16 95 mpbid ( 𝜑𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) )
97 f1ocnv ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) → 𝐺 : ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) –1-1-onto→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
98 f1of ( 𝐺 : ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) –1-1-onto→ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → 𝐺 : ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
99 96 97 98 3syl ( 𝜑 𝐺 : ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ⟶ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
100 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 lgsqrlem3 ( 𝜑 → ( 𝐿𝐴 ) ∈ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) )
101 99 100 ffvelcdmd ( 𝜑 → ( 𝐺 ‘ ( 𝐿𝐴 ) ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
102 101 elfzelzd ( 𝜑 → ( 𝐺 ‘ ( 𝐿𝐴 ) ) ∈ ℤ )
103 fvoveq1 ( 𝑥 = ( 𝐺 ‘ ( 𝐿𝐴 ) ) → ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) = ( 𝐿 ‘ ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ) )
104 fvoveq1 ( 𝑦 = 𝑥 → ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) = ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
105 104 cbvmptv ( 𝑦 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 𝑦 ↑ 2 ) ) ) = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
106 13 105 eqtri 𝐺 = ( 𝑥 ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↦ ( 𝐿 ‘ ( 𝑥 ↑ 2 ) ) )
107 fvex ( 𝐿 ‘ ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ) ∈ V
108 103 106 107 fvmpt ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) → ( 𝐺 ‘ ( 𝐺 ‘ ( 𝐿𝐴 ) ) ) = ( 𝐿 ‘ ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ) )
109 101 108 syl ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ ( 𝐿𝐴 ) ) ) = ( 𝐿 ‘ ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ) )
110 f1ocnvfv2 ( ( 𝐺 : ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) –1-1-onto→ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ∧ ( 𝐿𝐴 ) ∈ ( ( 𝑂𝑇 ) “ { ( 0g𝑌 ) } ) ) → ( 𝐺 ‘ ( 𝐺 ‘ ( 𝐿𝐴 ) ) ) = ( 𝐿𝐴 ) )
111 96 100 110 syl2anc ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ ( 𝐿𝐴 ) ) ) = ( 𝐿𝐴 ) )
112 109 111 eqtr3d ( 𝜑 → ( 𝐿 ‘ ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ) = ( 𝐿𝐴 ) )
113 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
114 24 113 syl ( 𝜑𝑃 ∈ ℕ )
115 114 nnnn0d ( 𝜑𝑃 ∈ ℕ0 )
116 zsqcl ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ∈ ℤ → ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ∈ ℤ )
117 102 116 syl ( 𝜑 → ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ∈ ℤ )
118 1 11 zndvds ( ( 𝑃 ∈ ℕ0 ∧ ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ) = ( 𝐿𝐴 ) ↔ 𝑃 ∥ ( ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) − 𝐴 ) ) )
119 115 117 14 118 syl3anc ( 𝜑 → ( ( 𝐿 ‘ ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) ) = ( 𝐿𝐴 ) ↔ 𝑃 ∥ ( ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) − 𝐴 ) ) )
120 112 119 mpbid ( 𝜑𝑃 ∥ ( ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) − 𝐴 ) )
121 oveq1 ( 𝑥 = ( 𝐺 ‘ ( 𝐿𝐴 ) ) → ( 𝑥 ↑ 2 ) = ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) )
122 121 oveq1d ( 𝑥 = ( 𝐺 ‘ ( 𝐿𝐴 ) ) → ( ( 𝑥 ↑ 2 ) − 𝐴 ) = ( ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) − 𝐴 ) )
123 122 breq2d ( 𝑥 = ( 𝐺 ‘ ( 𝐿𝐴 ) ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ↔ 𝑃 ∥ ( ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) − 𝐴 ) ) )
124 123 rspcev ( ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ∈ ℤ ∧ 𝑃 ∥ ( ( ( 𝐺 ‘ ( 𝐿𝐴 ) ) ↑ 2 ) − 𝐴 ) ) → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) )
125 102 120 124 syl2anc ( 𝜑 → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) )