# Metamath Proof Explorer

## Theorem 2sqlem7

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

Ref Expression
Hypotheses 2sq.1 ${⊢}{S}=\mathrm{ran}\left({w}\in ℤ\left[i\right]⟼{\left|{w}\right|}^{2}\right)$
2sqlem7.2 ${⊢}{Y}=\left\{{z}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\right\}$
Assertion 2sqlem7 ${⊢}{Y}\subseteq {S}\cap ℕ$

### Proof

Step Hyp Ref Expression
1 2sq.1 ${⊢}{S}=\mathrm{ran}\left({w}\in ℤ\left[i\right]⟼{\left|{w}\right|}^{2}\right)$
2 2sqlem7.2 ${⊢}{Y}=\left\{{z}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\right\}$
3 simpr ${⊢}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\to {z}={{x}}^{2}+{{y}}^{2}$
4 3 reximi ${⊢}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\to \exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={{x}}^{2}+{{y}}^{2}$
5 4 reximi ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={{x}}^{2}+{{y}}^{2}$
6 1 2sqlem2 ${⊢}{z}\in {S}↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{z}={{x}}^{2}+{{y}}^{2}$
7 5 6 sylibr ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\to {z}\in {S}$
8 ax-1ne0 ${⊢}1\ne 0$
9 gcdeq0 ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\right)\to \left({x}\mathrm{gcd}{y}=0↔\left({x}=0\wedge {y}=0\right)\right)$
10 9 adantr ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left({x}\mathrm{gcd}{y}=0↔\left({x}=0\wedge {y}=0\right)\right)$
11 simpr ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {x}\mathrm{gcd}{y}=1$
12 11 eqeq1d ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left({x}\mathrm{gcd}{y}=0↔1=0\right)$
13 10 12 bitr3d ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left(\left({x}=0\wedge {y}=0\right)↔1=0\right)$
14 13 necon3bbid ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left(¬\left({x}=0\wedge {y}=0\right)↔1\ne 0\right)$
15 8 14 mpbiri ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to ¬\left({x}=0\wedge {y}=0\right)$
16 zsqcl2 ${⊢}{x}\in ℤ\to {{x}}^{2}\in {ℕ}_{0}$
17 16 ad2antrr ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {{x}}^{2}\in {ℕ}_{0}$
18 17 nn0red ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {{x}}^{2}\in ℝ$
19 17 nn0ge0d ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to 0\le {{x}}^{2}$
20 zsqcl2 ${⊢}{y}\in ℤ\to {{y}}^{2}\in {ℕ}_{0}$
21 20 ad2antlr ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {{y}}^{2}\in {ℕ}_{0}$
22 21 nn0red ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {{y}}^{2}\in ℝ$
23 21 nn0ge0d ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to 0\le {{y}}^{2}$
24 add20 ${⊢}\left(\left({{x}}^{2}\in ℝ\wedge 0\le {{x}}^{2}\right)\wedge \left({{y}}^{2}\in ℝ\wedge 0\le {{y}}^{2}\right)\right)\to \left({{x}}^{2}+{{y}}^{2}=0↔\left({{x}}^{2}=0\wedge {{y}}^{2}=0\right)\right)$
25 18 19 22 23 24 syl22anc ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left({{x}}^{2}+{{y}}^{2}=0↔\left({{x}}^{2}=0\wedge {{y}}^{2}=0\right)\right)$
26 zcn ${⊢}{x}\in ℤ\to {x}\in ℂ$
27 26 ad2antrr ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {x}\in ℂ$
28 zcn ${⊢}{y}\in ℤ\to {y}\in ℂ$
29 28 ad2antlr ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {y}\in ℂ$
30 sqeq0 ${⊢}{x}\in ℂ\to \left({{x}}^{2}=0↔{x}=0\right)$
31 sqeq0 ${⊢}{y}\in ℂ\to \left({{y}}^{2}=0↔{y}=0\right)$
32 30 31 bi2anan9 ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to \left(\left({{x}}^{2}=0\wedge {{y}}^{2}=0\right)↔\left({x}=0\wedge {y}=0\right)\right)$
33 27 29 32 syl2anc ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left(\left({{x}}^{2}=0\wedge {{y}}^{2}=0\right)↔\left({x}=0\wedge {y}=0\right)\right)$
34 25 33 bitrd ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left({{x}}^{2}+{{y}}^{2}=0↔\left({x}=0\wedge {y}=0\right)\right)$
35 15 34 mtbird ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to ¬{{x}}^{2}+{{y}}^{2}=0$
36 nn0addcl ${⊢}\left({{x}}^{2}\in {ℕ}_{0}\wedge {{y}}^{2}\in {ℕ}_{0}\right)\to {{x}}^{2}+{{y}}^{2}\in {ℕ}_{0}$
37 16 20 36 syl2an ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\right)\to {{x}}^{2}+{{y}}^{2}\in {ℕ}_{0}$
38 37 adantr ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {{x}}^{2}+{{y}}^{2}\in {ℕ}_{0}$
39 elnn0 ${⊢}{{x}}^{2}+{{y}}^{2}\in {ℕ}_{0}↔\left({{x}}^{2}+{{y}}^{2}\in ℕ\vee {{x}}^{2}+{{y}}^{2}=0\right)$
40 38 39 sylib ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left({{x}}^{2}+{{y}}^{2}\in ℕ\vee {{x}}^{2}+{{y}}^{2}=0\right)$
41 40 ord ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left(¬{{x}}^{2}+{{y}}^{2}\in ℕ\to {{x}}^{2}+{{y}}^{2}=0\right)$
42 35 41 mt3d ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to {{x}}^{2}+{{y}}^{2}\in ℕ$
43 eleq1 ${⊢}{z}={{x}}^{2}+{{y}}^{2}\to \left({z}\in ℕ↔{{x}}^{2}+{{y}}^{2}\in ℕ\right)$
44 42 43 syl5ibrcom ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℤ\right)\wedge {x}\mathrm{gcd}{y}=1\right)\to \left({z}={{x}}^{2}+{{y}}^{2}\to {z}\in ℕ\right)$
45 44 expimpd ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\right)\to \left(\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\to {z}\in ℕ\right)$
46 45 rexlimivv ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\to {z}\in ℕ$
47 7 46 elind ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\to {z}\in \left({S}\cap ℕ\right)$
48 47 abssi ${⊢}\left\{{z}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{gcd}{y}=1\wedge {z}={{x}}^{2}+{{y}}^{2}\right)\right\}\subseteq {S}\cap ℕ$
49 2 48 eqsstri ${⊢}{Y}\subseteq {S}\cap ℕ$