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