Metamath Proof Explorer

Theorem 2sqlem7

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

Ref Expression
Hypotheses 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
Assertion 2sqlem7 𝑌 ⊆ ( 𝑆 ∩ ℕ )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 2sqlem7.2 ⊢ 𝑌 = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
3 simpr ⊢ ( ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
4 3 reximi ⊢ ( ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
5 4 reximi ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
6 1 2sqlem2 ⊢ ( 𝑧 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
7 5 6 sylibr ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑧 ∈ 𝑆 )
8 ax-1ne0 ⊢ 1 ≠ 0
9 gcdeq0 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 gcd 𝑦 ) = 0 ↔ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) )
10 9 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( 𝑥 gcd 𝑦 ) = 0 ↔ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) )
11 simpr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( 𝑥 gcd 𝑦 ) = 1 )
12 11 eqeq1d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( 𝑥 gcd 𝑦 ) = 0 ↔ 1 = 0 ) )
13 10 12 bitr3d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) ↔ 1 = 0 ) )
14 13 necon3bbid ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ¬ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ↔ 1 ≠ 0 ) )
15 8 14 mpbiri ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ¬ ( 𝑥 = 0 ∧ 𝑦 = 0 ) )
16 zsqcl2 ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ↑ 2 ) ∈ ℕ0 )
17 16 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( 𝑥 ↑ 2 ) ∈ ℕ0 )
18 17 nn0red ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( 𝑥 ↑ 2 ) ∈ ℝ )
19 17 nn0ge0d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → 0 ≤ ( 𝑥 ↑ 2 ) )
20 zsqcl2 ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 ↑ 2 ) ∈ ℕ0 )
21 20 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( 𝑦 ↑ 2 ) ∈ ℕ0 )
22 21 nn0red ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( 𝑦 ↑ 2 ) ∈ ℝ )
23 21 nn0ge0d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → 0 ≤ ( 𝑦 ↑ 2 ) )
24 add20 ⊢ ( ( ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ↑ 2 ) ) ∧ ( ( 𝑦 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑦 ↑ 2 ) ) ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = 0 ↔ ( ( 𝑥 ↑ 2 ) = 0 ∧ ( 𝑦 ↑ 2 ) = 0 ) ) )
25 18 19 22 23 24 syl22anc ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = 0 ↔ ( ( 𝑥 ↑ 2 ) = 0 ∧ ( 𝑦 ↑ 2 ) = 0 ) ) )
26 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
27 26 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → 𝑥 ∈ ℂ )
28 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
29 28 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → 𝑦 ∈ ℂ )
30 sqeq0 ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 ↑ 2 ) = 0 ↔ 𝑥 = 0 ) )
31 sqeq0 ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 ↑ 2 ) = 0 ↔ 𝑦 = 0 ) )
32 30 31 bi2anan9 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ ( 𝑦 ↑ 2 ) = 0 ) ↔ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) )
33 27 29 32 syl2anc ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ ( 𝑦 ↑ 2 ) = 0 ) ↔ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) )
34 25 33 bitrd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = 0 ↔ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) )
35 15 34 mtbird ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ¬ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = 0 )
36 nn0addcl ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℕ0 ∧ ( 𝑦 ↑ 2 ) ∈ ℕ0 ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ0 )
37 16 20 36 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ0 )
38 37 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ0 )
39 elnn0 ⊢ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ0 ↔ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ ∨ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = 0 ) )
40 38 39 sylib ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ ∨ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = 0 ) )
41 40 ord ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ¬ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = 0 ) )
42 35 41 mt3d ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ )
43 eleq1 ⊢ ( 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → ( 𝑧 ∈ ℕ ↔ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ ) )
44 42 43 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑥 gcd 𝑦 ) = 1 ) → ( 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → 𝑧 ∈ ℕ ) )
45 44 expimpd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑧 ∈ ℕ ) )
46 45 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑧 ∈ ℕ )
47 7 46 elind ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) → 𝑧 ∈ ( 𝑆 ∩ ℕ ) )
48 47 abssi ⊢ { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) } ⊆ ( 𝑆 ∩ ℕ )
49 2 48 eqsstri ⊢ 𝑌 ⊆ ( 𝑆 ∩ ℕ )