Metamath Proof Explorer

Theorem 2sqb

Description: The converse to 2sq . (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion 2sqb ( 𝑃 ∈ ℙ → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( 𝑃 = 2 ∨ ( 𝑃 mod 4 ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( 𝑃 ≠ 2 ↔ ¬ 𝑃 = 2 )
2 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
3 2 ad3antrrr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑃 ∈ ℤ )
4 simplrr ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑦 ∈ ℤ )
5 bezout ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) )
6 3 4 5 syl2anc ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) )
7 simplll ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) ) ) → ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
8 simpllr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) ) ) → ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) )
9 simplr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) ) ) → 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
10 simprll ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) ) ) → 𝑎 ∈ ℤ )
11 simprlr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) ) ) → 𝑏 ∈ ℤ )
12 simprr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) ) ) → ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) )
13 7 8 9 10 11 12 2sqblem ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ∧ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) ) ) → ( 𝑃 mod 4 ) = 1 )
14 13 expr ⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) → ( 𝑃 mod 4 ) = 1 ) )
15 14 rexlimdvva ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑦 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑦 · 𝑏 ) ) → ( 𝑃 mod 4 ) = 1 ) )
16 6 15 mpd ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → ( 𝑃 mod 4 ) = 1 )
17 16 ex ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → ( 𝑃 mod 4 ) = 1 ) )
18 17 rexlimdvva ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → ( 𝑃 mod 4 ) = 1 ) )
19 18 impancom ⊢ ( ( 𝑃 ∈ ℙ ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → ( 𝑃 ≠ 2 → ( 𝑃 mod 4 ) = 1 ) )
20 1 19 syl5bir ⊢ ( ( 𝑃 ∈ ℙ ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → ( ¬ 𝑃 = 2 → ( 𝑃 mod 4 ) = 1 ) )
21 20 orrd ⊢ ( ( 𝑃 ∈ ℙ ∧ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → ( 𝑃 = 2 ∨ ( 𝑃 mod 4 ) = 1 ) )
22 1z ⊢ 1 ∈ ℤ
23 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) )
24 sq1 ⊢ ( 1 ↑ 2 ) = 1
25 23 24 eqtrdi ⊢ ( 𝑥 = 1 → ( 𝑥 ↑ 2 ) = 1 )
26 25 oveq1d ⊢ ( 𝑥 = 1 → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( 1 + ( 𝑦 ↑ 2 ) ) )
27 26 eqeq2d ⊢ ( 𝑥 = 1 → ( 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ 𝑃 = ( 1 + ( 𝑦 ↑ 2 ) ) ) )
28 oveq1 ⊢ ( 𝑦 = 1 → ( 𝑦 ↑ 2 ) = ( 1 ↑ 2 ) )
29 28 24 eqtrdi ⊢ ( 𝑦 = 1 → ( 𝑦 ↑ 2 ) = 1 )
30 29 oveq2d ⊢ ( 𝑦 = 1 → ( 1 + ( 𝑦 ↑ 2 ) ) = ( 1 + 1 ) )
31 1p1e2 ⊢ ( 1 + 1 ) = 2
32 30 31 eqtrdi ⊢ ( 𝑦 = 1 → ( 1 + ( 𝑦 ↑ 2 ) ) = 2 )
33 32 eqeq2d ⊢ ( 𝑦 = 1 → ( 𝑃 = ( 1 + ( 𝑦 ↑ 2 ) ) ↔ 𝑃 = 2 ) )
34 27 33 rspc2ev ⊢ ( ( 1 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑃 = 2 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
35 22 22 34 mp3an12 ⊢ ( 𝑃 = 2 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
36 35 adantl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 = 2 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
37 2sq ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
38 36 37 jaodan ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 = 2 ∨ ( 𝑃 mod 4 ) = 1 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
39 21 38 impbida ⊢ ( 𝑃 ∈ ℙ → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( 𝑃 = 2 ∨ ( 𝑃 mod 4 ) = 1 ) ) )