MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2sqblem Structured version   Visualization version   GIF version

Theorem 2sqblem 25398
Description: The converse to 2sq 25397. (Contributed by Mario Carneiro, 20-Jun-2015.)
Hypotheses
Ref Expression
2sqb.1 (𝜑 → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
2sqb.2 (𝜑 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))
2sqb.3 (𝜑𝑃 = ((𝑋↑2) + (𝑌↑2)))
2sqb.4 (𝜑𝐴 ∈ ℤ)
2sqb.5 (𝜑𝐵 ∈ ℤ)
2sqb.6 (𝜑 → (𝑃 gcd 𝑌) = ((𝑃 · 𝐴) + (𝑌 · 𝐵)))
Assertion
Ref Expression
2sqblem (𝜑 → (𝑃 mod 4) = 1)

Proof of Theorem 2sqblem
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 2sqb.1 . . . . . 6 (𝜑 → (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
21simpld 483 . . . . 5 (𝜑𝑃 ∈ ℙ)
3 nprmdvds1 15645 . . . . 5 (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
42, 3syl 17 . . . 4 (𝜑 → ¬ 𝑃 ∥ 1)
5 prmz 15617 . . . . . 6 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
62, 5syl 17 . . . . 5 (𝜑𝑃 ∈ ℤ)
7 1z 11631 . . . . 5 1 ∈ ℤ
8 dvdsnegb 15230 . . . . 5 ((𝑃 ∈ ℤ ∧ 1 ∈ ℤ) → (𝑃 ∥ 1 ↔ 𝑃 ∥ -1))
96, 7, 8sylancl 575 . . . 4 (𝜑 → (𝑃 ∥ 1 ↔ 𝑃 ∥ -1))
104, 9mtbid 314 . . 3 (𝜑 → ¬ 𝑃 ∥ -1)
11 2sqb.2 . . . . . 6 (𝜑 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))
1211simpld 483 . . . . 5 (𝜑𝑋 ∈ ℤ)
13 2sqb.5 . . . . 5 (𝜑𝐵 ∈ ℤ)
1412, 13zmulcld 11712 . . . 4 (𝜑 → (𝑋 · 𝐵) ∈ ℤ)
15 zsqcl 13163 . . . . . . . . 9 (𝐵 ∈ ℤ → (𝐵↑2) ∈ ℤ)
1613, 15syl 17 . . . . . . . 8 (𝜑 → (𝐵↑2) ∈ ℤ)
17 dvdsmul1 15234 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ (𝐵↑2) ∈ ℤ) → 𝑃 ∥ (𝑃 · (𝐵↑2)))
186, 16, 17syl2anc 574 . . . . . . 7 (𝜑𝑃 ∥ (𝑃 · (𝐵↑2)))
1911simprd 484 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℤ)
2019, 13zmulcld 11712 . . . . . . . . . . . 12 (𝜑 → (𝑌 · 𝐵) ∈ ℤ)
21 zsqcl 13163 . . . . . . . . . . . 12 ((𝑌 · 𝐵) ∈ ℤ → ((𝑌 · 𝐵)↑2) ∈ ℤ)
2220, 21syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑌 · 𝐵)↑2) ∈ ℤ)
23 peano2zm 11644 . . . . . . . . . . 11 (((𝑌 · 𝐵)↑2) ∈ ℤ → (((𝑌 · 𝐵)↑2) − 1) ∈ ℤ)
2422, 23syl 17 . . . . . . . . . 10 (𝜑 → (((𝑌 · 𝐵)↑2) − 1) ∈ ℤ)
2524zcnd 11707 . . . . . . . . 9 (𝜑 → (((𝑌 · 𝐵)↑2) − 1) ∈ ℂ)
26 zsqcl 13163 . . . . . . . . . . . 12 ((𝑋 · 𝐵) ∈ ℤ → ((𝑋 · 𝐵)↑2) ∈ ℤ)
2714, 26syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑋 · 𝐵)↑2) ∈ ℤ)
2827peano2zd 11709 . . . . . . . . . 10 (𝜑 → (((𝑋 · 𝐵)↑2) + 1) ∈ ℤ)
2928zcnd 11707 . . . . . . . . 9 (𝜑 → (((𝑋 · 𝐵)↑2) + 1) ∈ ℂ)
3025, 29addcomd 10461 . . . . . . . 8 (𝜑 → ((((𝑌 · 𝐵)↑2) − 1) + (((𝑋 · 𝐵)↑2) + 1)) = ((((𝑋 · 𝐵)↑2) + 1) + (((𝑌 · 𝐵)↑2) − 1)))
3127zcnd 11707 . . . . . . . . 9 (𝜑 → ((𝑋 · 𝐵)↑2) ∈ ℂ)
32 ax-1cn 10217 . . . . . . . . . 10 1 ∈ ℂ
3332a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℂ)
3422zcnd 11707 . . . . . . . . 9 (𝜑 → ((𝑌 · 𝐵)↑2) ∈ ℂ)
3531, 33, 34ppncand 10655 . . . . . . . 8 (𝜑 → ((((𝑋 · 𝐵)↑2) + 1) + (((𝑌 · 𝐵)↑2) − 1)) = (((𝑋 · 𝐵)↑2) + ((𝑌 · 𝐵)↑2)))
36 zsqcl 13163 . . . . . . . . . . . 12 (𝑋 ∈ ℤ → (𝑋↑2) ∈ ℤ)
3712, 36syl 17 . . . . . . . . . . 11 (𝜑 → (𝑋↑2) ∈ ℤ)
3837zcnd 11707 . . . . . . . . . 10 (𝜑 → (𝑋↑2) ∈ ℂ)
39 zsqcl 13163 . . . . . . . . . . . 12 (𝑌 ∈ ℤ → (𝑌↑2) ∈ ℤ)
4019, 39syl 17 . . . . . . . . . . 11 (𝜑 → (𝑌↑2) ∈ ℤ)
4140zcnd 11707 . . . . . . . . . 10 (𝜑 → (𝑌↑2) ∈ ℂ)
4216zcnd 11707 . . . . . . . . . 10 (𝜑 → (𝐵↑2) ∈ ℂ)
4338, 41, 42adddird 10288 . . . . . . . . 9 (𝜑 → (((𝑋↑2) + (𝑌↑2)) · (𝐵↑2)) = (((𝑋↑2) · (𝐵↑2)) + ((𝑌↑2) · (𝐵↑2))))
44 2sqb.3 . . . . . . . . . 10 (𝜑𝑃 = ((𝑋↑2) + (𝑌↑2)))
4544oveq1d 6827 . . . . . . . . 9 (𝜑 → (𝑃 · (𝐵↑2)) = (((𝑋↑2) + (𝑌↑2)) · (𝐵↑2)))
4612zcnd 11707 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℂ)
4713zcnd 11707 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℂ)
4846, 47sqmuld 13249 . . . . . . . . . 10 (𝜑 → ((𝑋 · 𝐵)↑2) = ((𝑋↑2) · (𝐵↑2)))
4919zcnd 11707 . . . . . . . . . . 11 (𝜑𝑌 ∈ ℂ)
5049, 47sqmuld 13249 . . . . . . . . . 10 (𝜑 → ((𝑌 · 𝐵)↑2) = ((𝑌↑2) · (𝐵↑2)))
5148, 50oveq12d 6830 . . . . . . . . 9 (𝜑 → (((𝑋 · 𝐵)↑2) + ((𝑌 · 𝐵)↑2)) = (((𝑋↑2) · (𝐵↑2)) + ((𝑌↑2) · (𝐵↑2))))
5243, 45, 513eqtr4rd 2819 . . . . . . . 8 (𝜑 → (((𝑋 · 𝐵)↑2) + ((𝑌 · 𝐵)↑2)) = (𝑃 · (𝐵↑2)))
5330, 35, 523eqtrd 2812 . . . . . . 7 (𝜑 → ((((𝑌 · 𝐵)↑2) − 1) + (((𝑋 · 𝐵)↑2) + 1)) = (𝑃 · (𝐵↑2)))
5418, 53breqtrrd 4825 . . . . . 6 (𝜑𝑃 ∥ ((((𝑌 · 𝐵)↑2) − 1) + (((𝑋 · 𝐵)↑2) + 1)))
55 2sqb.4 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℤ)
56 dvdsmul1 15234 . . . . . . . . . . . 12 ((𝑃 ∈ ℤ ∧ 𝐴 ∈ ℤ) → 𝑃 ∥ (𝑃 · 𝐴))
576, 55, 56syl2anc 574 . . . . . . . . . . 11 (𝜑𝑃 ∥ (𝑃 · 𝐴))
586, 55zmulcld 11712 . . . . . . . . . . . 12 (𝜑 → (𝑃 · 𝐴) ∈ ℤ)
59 dvdsnegb 15230 . . . . . . . . . . . 12 ((𝑃 ∈ ℤ ∧ (𝑃 · 𝐴) ∈ ℤ) → (𝑃 ∥ (𝑃 · 𝐴) ↔ 𝑃 ∥ -(𝑃 · 𝐴)))
606, 58, 59syl2anc 574 . . . . . . . . . . 11 (𝜑 → (𝑃 ∥ (𝑃 · 𝐴) ↔ 𝑃 ∥ -(𝑃 · 𝐴)))
6157, 60mpbid 223 . . . . . . . . . 10 (𝜑𝑃 ∥ -(𝑃 · 𝐴))
6220zcnd 11707 . . . . . . . . . . . 12 (𝜑 → (𝑌 · 𝐵) ∈ ℂ)
63 negsubdi2 10563 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ (𝑌 · 𝐵) ∈ ℂ) → -(1 − (𝑌 · 𝐵)) = ((𝑌 · 𝐵) − 1))
6432, 62, 63sylancr 576 . . . . . . . . . . 11 (𝜑 → -(1 − (𝑌 · 𝐵)) = ((𝑌 · 𝐵) − 1))
6519zred 11706 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑌 ∈ ℝ)
66 absresq 14272 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 ∈ ℝ → ((abs‘𝑌)↑2) = (𝑌↑2))
6765, 66syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((abs‘𝑌)↑2) = (𝑌↑2))
6865resqcld 13264 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑌↑2) ∈ ℝ)
69 prmnn 15616 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
702, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑃 ∈ ℕ)
7170nnred 11258 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃 ∈ ℝ)
7271resqcld 13264 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃↑2) ∈ ℝ)
73 zsqcl2 13170 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋 ∈ ℤ → (𝑋↑2) ∈ ℕ0)
7412, 73syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑋↑2) ∈ ℕ0)
75 nn0addge2 11564 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑌↑2) ∈ ℝ ∧ (𝑋↑2) ∈ ℕ0) → (𝑌↑2) ≤ ((𝑋↑2) + (𝑌↑2)))
7668, 74, 75syl2anc 574 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑌↑2) ≤ ((𝑋↑2) + (𝑌↑2)))
7776, 44breqtrrd 4825 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑌↑2) ≤ 𝑃)
786zcnd 11707 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℂ)
7978exp1d 13232 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑1) = 𝑃)
807a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ ℤ)
81 2z 11633 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℤ
8281a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 2 ∈ ℤ)
83 prmuz2 15636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ‘2))
842, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑃 ∈ (ℤ‘2))
85 eluz2b2 11986 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ (ℤ‘2) ↔ (𝑃 ∈ ℕ ∧ 1 < 𝑃))
8685simprbi 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ (ℤ‘2) → 1 < 𝑃)
8784, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 < 𝑃)
88 1lt2 11418 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 < 2
8988a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 < 2)
90 ltexp2a 13141 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑃 ∈ ℝ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ) ∧ (1 < 𝑃 ∧ 1 < 2)) → (𝑃↑1) < (𝑃↑2))
9171, 80, 82, 87, 89, 90syl32anc 1487 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑃↑1) < (𝑃↑2))
9279, 91eqbrtrrd 4821 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃 < (𝑃↑2))
9368, 71, 72, 77, 92lelttrd 10418 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑌↑2) < (𝑃↑2))
9467, 93eqbrtrd 4819 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((abs‘𝑌)↑2) < (𝑃↑2))
9549abscld 14405 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (abs‘𝑌) ∈ ℝ)
9649absge0d 14413 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ (abs‘𝑌))
9770nnnn0d 11575 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑃 ∈ ℕ0)
9897nn0ge0d 11578 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ 𝑃)
9995, 71, 96, 98lt2sqd 13272 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((abs‘𝑌) < 𝑃 ↔ ((abs‘𝑌)↑2) < (𝑃↑2)))
10094, 99mpbird 248 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘𝑌) < 𝑃)
1016zred 11706 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑃 ∈ ℝ)
10295, 101ltnled 10407 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((abs‘𝑌) < 𝑃 ↔ ¬ 𝑃 ≤ (abs‘𝑌)))
103100, 102mpbid 223 . . . . . . . . . . . . . . . . . 18 (𝜑 → ¬ 𝑃 ≤ (abs‘𝑌))
104 sqnprm 15641 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 ∈ ℤ → ¬ (𝑋↑2) ∈ ℙ)
10512, 104syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑋↑2) ∈ ℙ)
10649abs00ad 14260 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((abs‘𝑌) = 0 ↔ 𝑌 = 0))
10744, 2eqeltrrd 2854 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑋↑2) + (𝑌↑2)) ∈ ℙ)
108 sq0i 13185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑌 = 0 → (𝑌↑2) = 0)
109108oveq2d 6828 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑌 = 0 → ((𝑋↑2) + (𝑌↑2)) = ((𝑋↑2) + 0))
110109eleq1d 2838 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑌 = 0 → (((𝑋↑2) + (𝑌↑2)) ∈ ℙ ↔ ((𝑋↑2) + 0) ∈ ℙ))
111107, 110syl5ibcom 236 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑌 = 0 → ((𝑋↑2) + 0) ∈ ℙ))
11238addid1d 10459 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑋↑2) + 0) = (𝑋↑2))
113112eleq1d 2838 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝑋↑2) + 0) ∈ ℙ ↔ (𝑋↑2) ∈ ℙ))
114111, 113sylibd 230 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑌 = 0 → (𝑋↑2) ∈ ℙ))
115106, 114sylbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((abs‘𝑌) = 0 → (𝑋↑2) ∈ ℙ))
116105, 115mtod 189 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ (abs‘𝑌) = 0)
117 nn0abscl 14282 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑌 ∈ ℤ → (abs‘𝑌) ∈ ℕ0)
11819, 117syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (abs‘𝑌) ∈ ℕ0)
119 elnn0 11518 . . . . . . . . . . . . . . . . . . . . . 22 ((abs‘𝑌) ∈ ℕ0 ↔ ((abs‘𝑌) ∈ ℕ ∨ (abs‘𝑌) = 0))
120118, 119sylib 209 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((abs‘𝑌) ∈ ℕ ∨ (abs‘𝑌) = 0))
121120ord 880 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (¬ (abs‘𝑌) ∈ ℕ → (abs‘𝑌) = 0))
122116, 121mt3d 142 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘𝑌) ∈ ℕ)
123 dvdsle 15263 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ (abs‘𝑌) ∈ ℕ) → (𝑃 ∥ (abs‘𝑌) → 𝑃 ≤ (abs‘𝑌)))
1246, 122, 123syl2anc 574 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 ∥ (abs‘𝑌) → 𝑃 ≤ (abs‘𝑌)))
125103, 124mtod 189 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ 𝑃 ∥ (abs‘𝑌))
126 dvdsabsb 15232 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑃𝑌𝑃 ∥ (abs‘𝑌)))
1276, 19, 126syl2anc 574 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃𝑌𝑃 ∥ (abs‘𝑌)))
128125, 127mtbird 315 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝑃𝑌)
129 coprm 15650 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℙ ∧ 𝑌 ∈ ℤ) → (¬ 𝑃𝑌 ↔ (𝑃 gcd 𝑌) = 1))
1302, 19, 129syl2anc 574 . . . . . . . . . . . . . . . 16 (𝜑 → (¬ 𝑃𝑌 ↔ (𝑃 gcd 𝑌) = 1))
131128, 130mpbid 223 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 gcd 𝑌) = 1)
132 2sqb.6 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 gcd 𝑌) = ((𝑃 · 𝐴) + (𝑌 · 𝐵)))
133131, 132eqtr3d 2810 . . . . . . . . . . . . . 14 (𝜑 → 1 = ((𝑃 · 𝐴) + (𝑌 · 𝐵)))
134133oveq1d 6827 . . . . . . . . . . . . 13 (𝜑 → (1 − (𝑌 · 𝐵)) = (((𝑃 · 𝐴) + (𝑌 · 𝐵)) − (𝑌 · 𝐵)))
13558zcnd 11707 . . . . . . . . . . . . . 14 (𝜑 → (𝑃 · 𝐴) ∈ ℂ)
136135, 62pncand 10616 . . . . . . . . . . . . 13 (𝜑 → (((𝑃 · 𝐴) + (𝑌 · 𝐵)) − (𝑌 · 𝐵)) = (𝑃 · 𝐴))
137134, 136eqtrd 2808 . . . . . . . . . . . 12 (𝜑 → (1 − (𝑌 · 𝐵)) = (𝑃 · 𝐴))
138137negeqd 10498 . . . . . . . . . . 11 (𝜑 → -(1 − (𝑌 · 𝐵)) = -(𝑃 · 𝐴))
13964, 138eqtr3d 2810 . . . . . . . . . 10 (𝜑 → ((𝑌 · 𝐵) − 1) = -(𝑃 · 𝐴))
14061, 139breqtrrd 4825 . . . . . . . . 9 (𝜑𝑃 ∥ ((𝑌 · 𝐵) − 1))
14120peano2zd 11709 . . . . . . . . . 10 (𝜑 → ((𝑌 · 𝐵) + 1) ∈ ℤ)
142 peano2zm 11644 . . . . . . . . . . 11 ((𝑌 · 𝐵) ∈ ℤ → ((𝑌 · 𝐵) − 1) ∈ ℤ)
14320, 142syl 17 . . . . . . . . . 10 (𝜑 → ((𝑌 · 𝐵) − 1) ∈ ℤ)
144 dvdsmultr2 15252 . . . . . . . . . 10 ((𝑃 ∈ ℤ ∧ ((𝑌 · 𝐵) + 1) ∈ ℤ ∧ ((𝑌 · 𝐵) − 1) ∈ ℤ) → (𝑃 ∥ ((𝑌 · 𝐵) − 1) → 𝑃 ∥ (((𝑌 · 𝐵) + 1) · ((𝑌 · 𝐵) − 1))))
1456, 141, 143, 144syl3anc 1480 . . . . . . . . 9 (𝜑 → (𝑃 ∥ ((𝑌 · 𝐵) − 1) → 𝑃 ∥ (((𝑌 · 𝐵) + 1) · ((𝑌 · 𝐵) − 1))))
146140, 145mpd 15 . . . . . . . 8 (𝜑𝑃 ∥ (((𝑌 · 𝐵) + 1) · ((𝑌 · 𝐵) − 1)))
147 sq1 13187 . . . . . . . . . 10 (1↑2) = 1
148147oveq2i 6823 . . . . . . . . 9 (((𝑌 · 𝐵)↑2) − (1↑2)) = (((𝑌 · 𝐵)↑2) − 1)
149 subsq 13201 . . . . . . . . . 10 (((𝑌 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑌 · 𝐵)↑2) − (1↑2)) = (((𝑌 · 𝐵) + 1) · ((𝑌 · 𝐵) − 1)))
15062, 32, 149sylancl 575 . . . . . . . . 9 (𝜑 → (((𝑌 · 𝐵)↑2) − (1↑2)) = (((𝑌 · 𝐵) + 1) · ((𝑌 · 𝐵) − 1)))
151148, 150syl5eqr 2822 . . . . . . . 8 (𝜑 → (((𝑌 · 𝐵)↑2) − 1) = (((𝑌 · 𝐵) + 1) · ((𝑌 · 𝐵) − 1)))
152146, 151breqtrrd 4825 . . . . . . 7 (𝜑𝑃 ∥ (((𝑌 · 𝐵)↑2) − 1))
153 dvdsadd2b 15259 . . . . . . 7 ((𝑃 ∈ ℤ ∧ (((𝑋 · 𝐵)↑2) + 1) ∈ ℤ ∧ ((((𝑌 · 𝐵)↑2) − 1) ∈ ℤ ∧ 𝑃 ∥ (((𝑌 · 𝐵)↑2) − 1))) → (𝑃 ∥ (((𝑋 · 𝐵)↑2) + 1) ↔ 𝑃 ∥ ((((𝑌 · 𝐵)↑2) − 1) + (((𝑋 · 𝐵)↑2) + 1))))
1546, 28, 24, 152, 153syl112anc 1483 . . . . . 6 (𝜑 → (𝑃 ∥ (((𝑋 · 𝐵)↑2) + 1) ↔ 𝑃 ∥ ((((𝑌 · 𝐵)↑2) − 1) + (((𝑋 · 𝐵)↑2) + 1))))
15554, 154mpbird 248 . . . . 5 (𝜑𝑃 ∥ (((𝑋 · 𝐵)↑2) + 1))
156 subneg 10553 . . . . . 6 ((((𝑋 · 𝐵)↑2) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑋 · 𝐵)↑2) − -1) = (((𝑋 · 𝐵)↑2) + 1))
15731, 32, 156sylancl 575 . . . . 5 (𝜑 → (((𝑋 · 𝐵)↑2) − -1) = (((𝑋 · 𝐵)↑2) + 1))
158155, 157breqtrrd 4825 . . . 4 (𝜑𝑃 ∥ (((𝑋 · 𝐵)↑2) − -1))
159 oveq1 6819 . . . . . . 7 (𝑥 = (𝑋 · 𝐵) → (𝑥↑2) = ((𝑋 · 𝐵)↑2))
160159oveq1d 6827 . . . . . 6 (𝑥 = (𝑋 · 𝐵) → ((𝑥↑2) − -1) = (((𝑋 · 𝐵)↑2) − -1))
161160breq2d 4809 . . . . 5 (𝑥 = (𝑋 · 𝐵) → (𝑃 ∥ ((𝑥↑2) − -1) ↔ 𝑃 ∥ (((𝑋 · 𝐵)↑2) − -1)))
162161rspcev 3465 . . . 4 (((𝑋 · 𝐵) ∈ ℤ ∧ 𝑃 ∥ (((𝑋 · 𝐵)↑2) − -1)) → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − -1))
16314, 158, 162syl2anc 574 . . 3 (𝜑 → ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − -1))
164 neg1z 11637 . . . 4 -1 ∈ ℤ
165 eldifsn 4464 . . . . 5 (𝑃 ∈ (ℙ ∖ {2}) ↔ (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2))
1661, 165sylibr 225 . . . 4 (𝜑𝑃 ∈ (ℙ ∖ {2}))
167 lgsqr 25318 . . . 4 ((-1 ∈ ℤ ∧ 𝑃 ∈ (ℙ ∖ {2})) → ((-1 /L 𝑃) = 1 ↔ (¬ 𝑃 ∥ -1 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − -1))))
168164, 166, 167sylancr 576 . . 3 (𝜑 → ((-1 /L 𝑃) = 1 ↔ (¬ 𝑃 ∥ -1 ∧ ∃𝑥 ∈ ℤ 𝑃 ∥ ((𝑥↑2) − -1))))
16910, 163, 168mpbir2and 693 . 2 (𝜑 → (-1 /L 𝑃) = 1)
170 m1lgs 25355 . . 3 (𝑃 ∈ (ℙ ∖ {2}) → ((-1 /L 𝑃) = 1 ↔ (𝑃 mod 4) = 1))
171166, 170syl 17 . 2 (𝜑 → ((-1 /L 𝑃) = 1 ↔ (𝑃 mod 4) = 1))
172169, 171mpbid 223 1 (𝜑 → (𝑃 mod 4) = 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  wo 863   = wceq 1634  wcel 2148  wne 2946  wrex 3065  cdif 3726  {csn 4326   class class class wbr 4797  cfv 6042  (class class class)co 6812  cc 10157  cr 10158  0cc0 10159  1c1 10160   + caddc 10162   · cmul 10164   < clt 10297  cle 10298  cmin 10489  -cneg 10490  cn 11243  2c2 11293  4c4 11295  0cn0 11516  cz 11601  cuz 11910   mod cmo 12898  cexp 13089  abscabs 14204  cdvds 15211   gcd cgcd 15445  cprime 15613   /L clgs 25261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-inf2 8723  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236  ax-pre-sup 10237  ax-addf 10238  ax-mulf 10239
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-iin 4668  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-of 7065  df-ofr 7066  df-om 7234  df-1st 7336  df-2nd 7337  df-supp 7468  df-tpos 7525  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-2o 7735  df-oadd 7738  df-er 7917  df-ec 7919  df-qs 7923  df-map 8032  df-pm 8033  df-ixp 8084  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-fsupp 8453  df-sup 8525  df-inf 8526  df-oi 8592  df-card 8986  df-cda 9213  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-nn 11244  df-2 11302  df-3 11303  df-4 11304  df-5 11305  df-6 11306  df-7 11307  df-8 11308  df-9 11309  df-n0 11517  df-xnn0 11588  df-z 11602  df-dec 11718  df-uz 11911  df-q 12014  df-rp 12053  df-fz 12556  df-fzo 12696  df-fl 12823  df-mod 12899  df-seq 13031  df-exp 13090  df-hash 13344  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-dvds 15212  df-gcd 15446  df-prm 15614  df-phi 15698  df-pc 15769  df-struct 16086  df-ndx 16087  df-slot 16088  df-base 16090  df-sets 16091  df-ress 16092  df-plusg 16182  df-mulr 16183  df-starv 16184  df-sca 16185  df-vsca 16186  df-ip 16187  df-tset 16188  df-ple 16189  df-ds 16192  df-unif 16193  df-hom 16194  df-cco 16195  df-0g 16330  df-gsum 16331  df-prds 16336  df-pws 16338  df-imas 16396  df-qus 16397  df-mre 16474  df-mrc 16475  df-acs 16477  df-mgm 17470  df-sgrp 17512  df-mnd 17523  df-mhm 17563  df-submnd 17564  df-grp 17653  df-minusg 17654  df-sbg 17655  df-mulg 17769  df-subg 17819  df-nsg 17820  df-eqg 17821  df-ghm 17886  df-cntz 17977  df-cmn 18422  df-abl 18423  df-mgp 18718  df-ur 18730  df-srg 18734  df-ring 18777  df-cring 18778  df-oppr 18851  df-dvdsr 18869  df-unit 18870  df-invr 18900  df-dvr 18911  df-rnghom 18945  df-drng 18979  df-field 18980  df-subrg 19008  df-lmod 19095  df-lss 19163  df-lsp 19205  df-sra 19407  df-rgmod 19408  df-lidl 19409  df-rsp 19410  df-2idl 19467  df-nzr 19493  df-rlreg 19518  df-domn 19519  df-idom 19520  df-assa 19547  df-asp 19548  df-ascl 19549  df-psr 19591  df-mvr 19592  df-mpl 19593  df-opsr 19595  df-evls 19741  df-evl 19742  df-psr1 19785  df-vr1 19786  df-ply1 19787  df-coe1 19788  df-evl1 19916  df-cnfld 19982  df-zring 20054  df-zrh 20087  df-zn 20090  df-mdeg 24056  df-deg1 24057  df-mon1 24131  df-uc1p 24132  df-q1p 24133  df-r1p 24134  df-lgs 25262
This theorem is referenced by:  2sqb  25399
  Copyright terms: Public domain W3C validator