Metamath Proof Explorer

Theorem 2sqblem

Description: Lemma for 2sqb . (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 2sqb.1 ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
2sqb.2 ⊢ ( 𝜑 → ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) )
2sqb.3 ⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
2sqb.4 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2sqb.5 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
2sqb.6 ⊢ ( 𝜑 → ( 𝑃 gcd 𝑌 ) = ( ( 𝑃 · 𝐴 ) + ( 𝑌 · 𝐵 ) ) )
Assertion 2sqblem ( 𝜑 → ( 𝑃 mod 4 ) = 1 )

Proof

Step Hyp Ref Expression
1 2sqb.1 ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
2 2sqb.2 ⊢ ( 𝜑 → ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) )
3 2sqb.3 ⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
4 2sqb.4 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
5 2sqb.5 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
6 2sqb.6 ⊢ ( 𝜑 → ( 𝑃 gcd 𝑌 ) = ( ( 𝑃 · 𝐴 ) + ( 𝑌 · 𝐵 ) ) )
7 1 simpld ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
8 nprmdvds1 ⊢ ( 𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1 )
9 7 8 syl ⊢ ( 𝜑 → ¬ 𝑃 ∥ 1 )
10 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
11 7 10 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
12 1z ⊢ 1 ∈ ℤ
13 dvdsnegb ⊢ ( ( 𝑃 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑃 ∥ 1 ↔ 𝑃 ∥ - 1 ) )
14 11 12 13 sylancl ⊢ ( 𝜑 → ( 𝑃 ∥ 1 ↔ 𝑃 ∥ - 1 ) )
15 9 14 mtbid ⊢ ( 𝜑 → ¬ 𝑃 ∥ - 1 )
16 2 simpld ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
17 16 5 zmulcld ⊢ ( 𝜑 → ( 𝑋 · 𝐵 ) ∈ ℤ )
18 zsqcl ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
19 5 18 syl ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℤ )
20 dvdsmul1 ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝐵 ↑ 2 ) ∈ ℤ ) → 𝑃 ∥ ( 𝑃 · ( 𝐵 ↑ 2 ) ) )
21 11 19 20 syl2anc ⊢ ( 𝜑 → 𝑃 ∥ ( 𝑃 · ( 𝐵 ↑ 2 ) ) )
22 2 simprd ⊢ ( 𝜑 → 𝑌 ∈ ℤ )
23 22 5 zmulcld ⊢ ( 𝜑 → ( 𝑌 · 𝐵 ) ∈ ℤ )
24 zsqcl ⊢ ( ( 𝑌 · 𝐵 ) ∈ ℤ → ( ( 𝑌 · 𝐵 ) ↑ 2 ) ∈ ℤ )
25 23 24 syl ⊢ ( 𝜑 → ( ( 𝑌 · 𝐵 ) ↑ 2 ) ∈ ℤ )
26 peano2zm ⊢ ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) ∈ ℤ → ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) ∈ ℤ )
27 25 26 syl ⊢ ( 𝜑 → ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) ∈ ℤ )
28 27 zcnd ⊢ ( 𝜑 → ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) ∈ ℂ )
29 zsqcl ⊢ ( ( 𝑋 · 𝐵 ) ∈ ℤ → ( ( 𝑋 · 𝐵 ) ↑ 2 ) ∈ ℤ )
30 17 29 syl ⊢ ( 𝜑 → ( ( 𝑋 · 𝐵 ) ↑ 2 ) ∈ ℤ )
31 30 peano2zd ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ∈ ℤ )
32 31 zcnd ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ∈ ℂ )
33 28 32 addcomd ⊢ ( 𝜑 → ( ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) + ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ) = ( ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) + ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) ) )
34 30 zcnd ⊢ ( 𝜑 → ( ( 𝑋 · 𝐵 ) ↑ 2 ) ∈ ℂ )
35 ax-1cn ⊢ 1 ∈ ℂ
36 35 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
37 25 zcnd ⊢ ( 𝜑 → ( ( 𝑌 · 𝐵 ) ↑ 2 ) ∈ ℂ )
38 34 36 37 ppncand ⊢ ( 𝜑 → ( ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) + ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) ) = ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + ( ( 𝑌 · 𝐵 ) ↑ 2 ) ) )
39 zsqcl ⊢ ( 𝑋 ∈ ℤ → ( 𝑋 ↑ 2 ) ∈ ℤ )
40 16 39 syl ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℤ )
41 40 zcnd ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
42 zsqcl ⊢ ( 𝑌 ∈ ℤ → ( 𝑌 ↑ 2 ) ∈ ℤ )
43 22 42 syl ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℤ )
44 43 zcnd ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℂ )
45 19 zcnd ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
46 41 44 45 adddird ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) = ( ( ( 𝑋 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝑌 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
47 3 oveq1d ⊢ ( 𝜑 → ( 𝑃 · ( 𝐵 ↑ 2 ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) )
48 16 zcnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
49 5 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
50 48 49 sqmuld ⊢ ( 𝜑 → ( ( 𝑋 · 𝐵 ) ↑ 2 ) = ( ( 𝑋 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
51 22 zcnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
52 51 49 sqmuld ⊢ ( 𝜑 → ( ( 𝑌 · 𝐵 ) ↑ 2 ) = ( ( 𝑌 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
53 50 52 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + ( ( 𝑌 · 𝐵 ) ↑ 2 ) ) = ( ( ( 𝑋 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) + ( ( 𝑌 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
54 46 47 53 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + ( ( 𝑌 · 𝐵 ) ↑ 2 ) ) = ( 𝑃 · ( 𝐵 ↑ 2 ) ) )
55 33 38 54 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) + ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ) = ( 𝑃 · ( 𝐵 ↑ 2 ) ) )
56 21 55 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) + ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ) )
57 dvdsmul1 ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → 𝑃 ∥ ( 𝑃 · 𝐴 ) )
58 11 4 57 syl2anc ⊢ ( 𝜑 → 𝑃 ∥ ( 𝑃 · 𝐴 ) )
59 11 4 zmulcld ⊢ ( 𝜑 → ( 𝑃 · 𝐴 ) ∈ ℤ )
60 dvdsnegb ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑃 · 𝐴 ) ∈ ℤ ) → ( 𝑃 ∥ ( 𝑃 · 𝐴 ) ↔ 𝑃 ∥ - ( 𝑃 · 𝐴 ) ) )
61 11 59 60 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( 𝑃 · 𝐴 ) ↔ 𝑃 ∥ - ( 𝑃 · 𝐴 ) ) )
62 58 61 mpbid ⊢ ( 𝜑 → 𝑃 ∥ - ( 𝑃 · 𝐴 ) )
63 23 zcnd ⊢ ( 𝜑 → ( 𝑌 · 𝐵 ) ∈ ℂ )
64 negsubdi2 ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑌 · 𝐵 ) ∈ ℂ ) → - ( 1 − ( 𝑌 · 𝐵 ) ) = ( ( 𝑌 · 𝐵 ) − 1 ) )
65 35 63 64 sylancr ⊢ ( 𝜑 → - ( 1 − ( 𝑌 · 𝐵 ) ) = ( ( 𝑌 · 𝐵 ) − 1 ) )
66 59 zcnd ⊢ ( 𝜑 → ( 𝑃 · 𝐴 ) ∈ ℂ )
67 22 zred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
68 absresq ⊢ ( 𝑌 ∈ ℝ → ( ( abs ‘ 𝑌 ) ↑ 2 ) = ( 𝑌 ↑ 2 ) )
69 67 68 syl ⊢ ( 𝜑 → ( ( abs ‘ 𝑌 ) ↑ 2 ) = ( 𝑌 ↑ 2 ) )
70 67 resqcld ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℝ )
71 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
72 7 71 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
73 72 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
74 73 resqcld ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℝ )
75 zsqcl2 ⊢ ( 𝑋 ∈ ℤ → ( 𝑋 ↑ 2 ) ∈ ℕ0 )
76 16 75 syl ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℕ0 )
77 nn0addge2 ⊢ ( ( ( 𝑌 ↑ 2 ) ∈ ℝ ∧ ( 𝑋 ↑ 2 ) ∈ ℕ0 ) → ( 𝑌 ↑ 2 ) ≤ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
78 70 76 77 syl2anc ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ≤ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
79 78 3 breqtrrd ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ≤ 𝑃 )
80 11 zcnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
81 80 exp1d ⊢ ( 𝜑 → ( 𝑃 ↑ 1 ) = 𝑃 )
82 12 a1i ⊢ ( 𝜑 → 1 ∈ ℤ )
83 2z ⊢ 2 ∈ ℤ
84 83 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
85 prmuz2 ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
86 7 85 syl ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
87 eluz2gt1 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑃 )
88 86 87 syl ⊢ ( 𝜑 → 1 < 𝑃 )
89 1lt2 ⊢ 1 < 2
90 89 a1i ⊢ ( 𝜑 → 1 < 2 )
91 ltexp2a ⊢ ( ( ( 𝑃 ∈ ℝ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 1 < 𝑃 ∧ 1 < 2 ) ) → ( 𝑃 ↑ 1 ) < ( 𝑃 ↑ 2 ) )
92 73 82 84 88 90 91 syl32anc ⊢ ( 𝜑 → ( 𝑃 ↑ 1 ) < ( 𝑃 ↑ 2 ) )
93 81 92 eqbrtrrd ⊢ ( 𝜑 → 𝑃 < ( 𝑃 ↑ 2 ) )
94 70 73 74 79 93 lelttrd ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) < ( 𝑃 ↑ 2 ) )
95 69 94 eqbrtrd ⊢ ( 𝜑 → ( ( abs ‘ 𝑌 ) ↑ 2 ) < ( 𝑃 ↑ 2 ) )
96 51 abscld ⊢ ( 𝜑 → ( abs ‘ 𝑌 ) ∈ ℝ )
97 51 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑌 ) )
98 72 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
99 98 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑃 )
100 96 73 97 99 lt2sqd ⊢ ( 𝜑 → ( ( abs ‘ 𝑌 ) < 𝑃 ↔ ( ( abs ‘ 𝑌 ) ↑ 2 ) < ( 𝑃 ↑ 2 ) ) )
101 95 100 mpbird ⊢ ( 𝜑 → ( abs ‘ 𝑌 ) < 𝑃 )
102 11 zred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
103 96 102 ltnled ⊢ ( 𝜑 → ( ( abs ‘ 𝑌 ) < 𝑃 ↔ ¬ 𝑃 ≤ ( abs ‘ 𝑌 ) ) )
104 101 103 mpbid ⊢ ( 𝜑 → ¬ 𝑃 ≤ ( abs ‘ 𝑌 ) )
105 sqnprm ⊢ ( 𝑋 ∈ ℤ → ¬ ( 𝑋 ↑ 2 ) ∈ ℙ )
106 16 105 syl ⊢ ( 𝜑 → ¬ ( 𝑋 ↑ 2 ) ∈ ℙ )
107 51 abs00ad ⊢ ( 𝜑 → ( ( abs ‘ 𝑌 ) = 0 ↔ 𝑌 = 0 ) )
108 3 7 eqeltrrd ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ∈ ℙ )
109 sq0i ⊢ ( 𝑌 = 0 → ( 𝑌 ↑ 2 ) = 0 )
110 109 oveq2d ⊢ ( 𝑌 = 0 → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( 𝑋 ↑ 2 ) + 0 ) )
111 110 eleq1d ⊢ ( 𝑌 = 0 → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ∈ ℙ ↔ ( ( 𝑋 ↑ 2 ) + 0 ) ∈ ℙ ) )
112 108 111 syl5ibcom ⊢ ( 𝜑 → ( 𝑌 = 0 → ( ( 𝑋 ↑ 2 ) + 0 ) ∈ ℙ ) )
113 41 addridd ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + 0 ) = ( 𝑋 ↑ 2 ) )
114 113 eleq1d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + 0 ) ∈ ℙ ↔ ( 𝑋 ↑ 2 ) ∈ ℙ ) )
115 112 114 sylibd ⊢ ( 𝜑 → ( 𝑌 = 0 → ( 𝑋 ↑ 2 ) ∈ ℙ ) )
116 107 115 sylbid ⊢ ( 𝜑 → ( ( abs ‘ 𝑌 ) = 0 → ( 𝑋 ↑ 2 ) ∈ ℙ ) )
117 106 116 mtod ⊢ ( 𝜑 → ¬ ( abs ‘ 𝑌 ) = 0 )
118 nn0abscl ⊢ ( 𝑌 ∈ ℤ → ( abs ‘ 𝑌 ) ∈ ℕ0 )
119 22 118 syl ⊢ ( 𝜑 → ( abs ‘ 𝑌 ) ∈ ℕ0 )
120 elnn0 ⊢ ( ( abs ‘ 𝑌 ) ∈ ℕ0 ↔ ( ( abs ‘ 𝑌 ) ∈ ℕ ∨ ( abs ‘ 𝑌 ) = 0 ) )
121 119 120 sylib ⊢ ( 𝜑 → ( ( abs ‘ 𝑌 ) ∈ ℕ ∨ ( abs ‘ 𝑌 ) = 0 ) )
122 121 ord ⊢ ( 𝜑 → ( ¬ ( abs ‘ 𝑌 ) ∈ ℕ → ( abs ‘ 𝑌 ) = 0 ) )
123 117 122 mt3d ⊢ ( 𝜑 → ( abs ‘ 𝑌 ) ∈ ℕ )
124 dvdsle ⊢ ( ( 𝑃 ∈ ℤ ∧ ( abs ‘ 𝑌 ) ∈ ℕ ) → ( 𝑃 ∥ ( abs ‘ 𝑌 ) → 𝑃 ≤ ( abs ‘ 𝑌 ) ) )
125 11 123 124 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( abs ‘ 𝑌 ) → 𝑃 ≤ ( abs ‘ 𝑌 ) ) )
126 104 125 mtod ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( abs ‘ 𝑌 ) )
127 dvdsabsb ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑃 ∥ 𝑌 ↔ 𝑃 ∥ ( abs ‘ 𝑌 ) ) )
128 11 22 127 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ 𝑌 ↔ 𝑃 ∥ ( abs ‘ 𝑌 ) ) )
129 126 128 mtbird ⊢ ( 𝜑 → ¬ 𝑃 ∥ 𝑌 )
130 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑌 ∈ ℤ ) → ( ¬ 𝑃 ∥ 𝑌 ↔ ( 𝑃 gcd 𝑌 ) = 1 ) )
131 7 22 130 syl2anc ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ 𝑌 ↔ ( 𝑃 gcd 𝑌 ) = 1 ) )
132 129 131 mpbid ⊢ ( 𝜑 → ( 𝑃 gcd 𝑌 ) = 1 )
133 132 6 eqtr3d ⊢ ( 𝜑 → 1 = ( ( 𝑃 · 𝐴 ) + ( 𝑌 · 𝐵 ) ) )
134 66 63 133 mvrraddd ⊢ ( 𝜑 → ( 1 − ( 𝑌 · 𝐵 ) ) = ( 𝑃 · 𝐴 ) )
135 134 negeqd ⊢ ( 𝜑 → - ( 1 − ( 𝑌 · 𝐵 ) ) = - ( 𝑃 · 𝐴 ) )
136 65 135 eqtr3d ⊢ ( 𝜑 → ( ( 𝑌 · 𝐵 ) − 1 ) = - ( 𝑃 · 𝐴 ) )
137 62 136 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( 𝑌 · 𝐵 ) − 1 ) )
138 23 peano2zd ⊢ ( 𝜑 → ( ( 𝑌 · 𝐵 ) + 1 ) ∈ ℤ )
139 peano2zm ⊢ ( ( 𝑌 · 𝐵 ) ∈ ℤ → ( ( 𝑌 · 𝐵 ) − 1 ) ∈ ℤ )
140 23 139 syl ⊢ ( 𝜑 → ( ( 𝑌 · 𝐵 ) − 1 ) ∈ ℤ )
141 dvdsmultr2 ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝑌 · 𝐵 ) + 1 ) ∈ ℤ ∧ ( ( 𝑌 · 𝐵 ) − 1 ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝑌 · 𝐵 ) − 1 ) → 𝑃 ∥ ( ( ( 𝑌 · 𝐵 ) + 1 ) · ( ( 𝑌 · 𝐵 ) − 1 ) ) ) )
142 11 138 140 141 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝑌 · 𝐵 ) − 1 ) → 𝑃 ∥ ( ( ( 𝑌 · 𝐵 ) + 1 ) · ( ( 𝑌 · 𝐵 ) − 1 ) ) ) )
143 137 142 mpd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( 𝑌 · 𝐵 ) + 1 ) · ( ( 𝑌 · 𝐵 ) − 1 ) ) )
144 sq1 ⊢ ( 1 ↑ 2 ) = 1
145 144 oveq2i ⊢ ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − ( 1 ↑ 2 ) ) = ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 )
146 subsq ⊢ ( ( ( 𝑌 · 𝐵 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − ( 1 ↑ 2 ) ) = ( ( ( 𝑌 · 𝐵 ) + 1 ) · ( ( 𝑌 · 𝐵 ) − 1 ) ) )
147 63 35 146 sylancl ⊢ ( 𝜑 → ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − ( 1 ↑ 2 ) ) = ( ( ( 𝑌 · 𝐵 ) + 1 ) · ( ( 𝑌 · 𝐵 ) − 1 ) ) )
148 145 147 eqtr3id ⊢ ( 𝜑 → ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) = ( ( ( 𝑌 · 𝐵 ) + 1 ) · ( ( 𝑌 · 𝐵 ) − 1 ) ) )
149 143 148 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) )
150 dvdsadd2b ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ∈ ℤ ∧ ( ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) ∈ ℤ ∧ 𝑃 ∥ ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) ) ) → ( 𝑃 ∥ ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ↔ 𝑃 ∥ ( ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) + ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ) ) )
151 11 31 27 149 150 syl112anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ↔ 𝑃 ∥ ( ( ( ( 𝑌 · 𝐵 ) ↑ 2 ) − 1 ) + ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) ) ) )
152 56 151 mpbird ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) )
153 subneg ⊢ ( ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) − - 1 ) = ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) )
154 34 35 153 sylancl ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) − - 1 ) = ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) + 1 ) )
155 152 154 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) − - 1 ) )
156 oveq1 ⊢ ( 𝑥 = ( 𝑋 · 𝐵 ) → ( 𝑥 ↑ 2 ) = ( ( 𝑋 · 𝐵 ) ↑ 2 ) )
157 156 oveq1d ⊢ ( 𝑥 = ( 𝑋 · 𝐵 ) → ( ( 𝑥 ↑ 2 ) − - 1 ) = ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) − - 1 ) )
158 157 breq2d ⊢ ( 𝑥 = ( 𝑋 · 𝐵 ) → ( 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − - 1 ) ↔ 𝑃 ∥ ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) − - 1 ) ) )
159 158 rspcev ⊢ ( ( ( 𝑋 · 𝐵 ) ∈ ℤ ∧ 𝑃 ∥ ( ( ( 𝑋 · 𝐵 ) ↑ 2 ) − - 1 ) ) → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − - 1 ) )
160 17 155 159 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − - 1 ) )
161 neg1z ⊢ - 1 ∈ ℤ
162 eldifsn ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
163 1 162 sylibr ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
164 lgsqr ⊢ ( ( - 1 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( ¬ 𝑃 ∥ - 1 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − - 1 ) ) ) )
165 161 163 164 sylancr ⊢ ( 𝜑 → ( ( - 1 /L 𝑃 ) = 1 ↔ ( ¬ 𝑃 ∥ - 1 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − - 1 ) ) ) )
166 15 160 165 mpbir2and ⊢ ( 𝜑 → ( - 1 /L 𝑃 ) = 1 )
167 m1lgs ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( - 1 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 4 ) = 1 ) )
168 163 167 syl ⊢ ( 𝜑 → ( ( - 1 /L 𝑃 ) = 1 ↔ ( 𝑃 mod 4 ) = 1 ) )
169 166 168 mpbid ⊢ ( 𝜑 → ( 𝑃 mod 4 ) = 1 )