Metamath Proof Explorer

Theorem 2sqlem7

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

Ref Expression
Hypotheses 2sq.1 ⊢ S = ran ⁡ w ∈ ℤ i ⟼ w 2
2sqlem7.2 ⊢ Y = z | ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ z = x 2 + y 2
Assertion 2sqlem7 ⊢ Y ⊆ S ∩ ℕ

Proof

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