Metamath Proof Explorer

Theorem 2sqb

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

Ref Expression
Assertion 2sqb ${⊢}{P}\in ℙ\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}↔\left({P}=2\vee {P}\mathrm{mod}4=1\right)\right)$

Proof

Step Hyp Ref Expression
1 df-ne ${⊢}{P}\ne 2↔¬{P}=2$
2 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
3 2 ad3antrrr ${⊢}\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\to {P}\in ℤ$
4 simplrr ${⊢}\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\to {y}\in ℤ$
5 bezout ${⊢}\left({P}\in ℤ\wedge {y}\in ℤ\right)\to \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\mathrm{gcd}{y}={P}{a}+{y}{b}$
6 3 4 5 syl2anc ${⊢}\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\to \exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\mathrm{gcd}{y}={P}{a}+{y}{b}$
7 simplll ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\wedge \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge {P}\mathrm{gcd}{y}={P}{a}+{y}{b}\right)\right)\to \left({P}\in ℙ\wedge {P}\ne 2\right)$
8 simpllr ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\wedge \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge {P}\mathrm{gcd}{y}={P}{a}+{y}{b}\right)\right)\to \left({x}\in ℤ\wedge {y}\in ℤ\right)$
9 simplr ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\wedge \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge {P}\mathrm{gcd}{y}={P}{a}+{y}{b}\right)\right)\to {P}={{x}}^{2}+{{y}}^{2}$
10 simprll ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\wedge \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge {P}\mathrm{gcd}{y}={P}{a}+{y}{b}\right)\right)\to {a}\in ℤ$
11 simprlr ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\wedge \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge {P}\mathrm{gcd}{y}={P}{a}+{y}{b}\right)\right)\to {b}\in ℤ$
12 simprr ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\wedge \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge {P}\mathrm{gcd}{y}={P}{a}+{y}{b}\right)\right)\to {P}\mathrm{gcd}{y}={P}{a}+{y}{b}$
13 7 8 9 10 11 12 2sqblem ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\wedge \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge {P}\mathrm{gcd}{y}={P}{a}+{y}{b}\right)\right)\to {P}\mathrm{mod}4=1$
14 13 expr ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\wedge \left({a}\in ℤ\wedge {b}\in ℤ\right)\right)\to \left({P}\mathrm{gcd}{y}={P}{a}+{y}{b}\to {P}\mathrm{mod}4=1\right)$
15 14 rexlimdvva ${⊢}\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\to \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\mathrm{gcd}{y}={P}{a}+{y}{b}\to {P}\mathrm{mod}4=1\right)$
16 6 15 mpd ${⊢}\left(\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge {P}={{x}}^{2}+{{y}}^{2}\right)\to {P}\mathrm{mod}4=1$
17 16 ex ${⊢}\left(\left({P}\in ℙ\wedge {P}\ne 2\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\to \left({P}={{x}}^{2}+{{y}}^{2}\to {P}\mathrm{mod}4=1\right)$
18 17 rexlimdvva ${⊢}\left({P}\in ℙ\wedge {P}\ne 2\right)\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}\to {P}\mathrm{mod}4=1\right)$
19 18 impancom ${⊢}\left({P}\in ℙ\wedge \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}\right)\to \left({P}\ne 2\to {P}\mathrm{mod}4=1\right)$
20 1 19 syl5bir ${⊢}\left({P}\in ℙ\wedge \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}\right)\to \left(¬{P}=2\to {P}\mathrm{mod}4=1\right)$
21 20 orrd ${⊢}\left({P}\in ℙ\wedge \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}\right)\to \left({P}=2\vee {P}\mathrm{mod}4=1\right)$
22 1z ${⊢}1\in ℤ$
23 oveq1 ${⊢}{x}=1\to {{x}}^{2}={1}^{2}$
24 sq1 ${⊢}{1}^{2}=1$
25 23 24 syl6eq ${⊢}{x}=1\to {{x}}^{2}=1$
26 25 oveq1d ${⊢}{x}=1\to {{x}}^{2}+{{y}}^{2}=1+{{y}}^{2}$
27 26 eqeq2d ${⊢}{x}=1\to \left({P}={{x}}^{2}+{{y}}^{2}↔{P}=1+{{y}}^{2}\right)$
28 oveq1 ${⊢}{y}=1\to {{y}}^{2}={1}^{2}$
29 28 24 syl6eq ${⊢}{y}=1\to {{y}}^{2}=1$
30 29 oveq2d ${⊢}{y}=1\to 1+{{y}}^{2}=1+1$
31 1p1e2 ${⊢}1+1=2$
32 30 31 syl6eq ${⊢}{y}=1\to 1+{{y}}^{2}=2$
33 32 eqeq2d ${⊢}{y}=1\to \left({P}=1+{{y}}^{2}↔{P}=2\right)$
34 27 33 rspc2ev ${⊢}\left(1\in ℤ\wedge 1\in ℤ\wedge {P}=2\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}$
35 22 22 34 mp3an12 ${⊢}{P}=2\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}$
36 35 adantl ${⊢}\left({P}\in ℙ\wedge {P}=2\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}$
37 2sq ${⊢}\left({P}\in ℙ\wedge {P}\mathrm{mod}4=1\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}$
38 36 37 jaodan ${⊢}\left({P}\in ℙ\wedge \left({P}=2\vee {P}\mathrm{mod}4=1\right)\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}$
39 21 38 impbida ${⊢}{P}\in ℙ\to \left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}{P}={{x}}^{2}+{{y}}^{2}↔\left({P}=2\vee {P}\mathrm{mod}4=1\right)\right)$