# Metamath Proof Explorer

## Theorem 2sqlem4

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

Ref Expression
Hypotheses 2sq.1 ${⊢}{S}=\mathrm{ran}\left({w}\in ℤ\left[i\right]⟼{\left|{w}\right|}^{2}\right)$
2sqlem5.1 ${⊢}{\phi }\to {N}\in ℕ$
2sqlem5.2 ${⊢}{\phi }\to {P}\in ℙ$
2sqlem4.3 ${⊢}{\phi }\to {A}\in ℤ$
2sqlem4.4 ${⊢}{\phi }\to {B}\in ℤ$
2sqlem4.5 ${⊢}{\phi }\to {C}\in ℤ$
2sqlem4.6 ${⊢}{\phi }\to {D}\in ℤ$
2sqlem4.7 ${⊢}{\phi }\to {N}{P}={{A}}^{2}+{{B}}^{2}$
2sqlem4.8 ${⊢}{\phi }\to {P}={{C}}^{2}+{{D}}^{2}$
Assertion 2sqlem4 ${⊢}{\phi }\to {N}\in {S}$

### Proof

Step Hyp Ref Expression
1 2sq.1 ${⊢}{S}=\mathrm{ran}\left({w}\in ℤ\left[i\right]⟼{\left|{w}\right|}^{2}\right)$
2 2sqlem5.1 ${⊢}{\phi }\to {N}\in ℕ$
3 2sqlem5.2 ${⊢}{\phi }\to {P}\in ℙ$
4 2sqlem4.3 ${⊢}{\phi }\to {A}\in ℤ$
5 2sqlem4.4 ${⊢}{\phi }\to {B}\in ℤ$
6 2sqlem4.5 ${⊢}{\phi }\to {C}\in ℤ$
7 2sqlem4.6 ${⊢}{\phi }\to {D}\in ℤ$
8 2sqlem4.7 ${⊢}{\phi }\to {N}{P}={{A}}^{2}+{{B}}^{2}$
9 2sqlem4.8 ${⊢}{\phi }\to {P}={{C}}^{2}+{{D}}^{2}$
10 2 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {N}\in ℕ$
11 3 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {P}\in ℙ$
12 4 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {A}\in ℤ$
13 5 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {B}\in ℤ$
14 6 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {C}\in ℤ$
15 7 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {D}\in ℤ$
16 8 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {N}{P}={{A}}^{2}+{{B}}^{2}$
17 9 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {P}={{C}}^{2}+{{D}}^{2}$
18 simpr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {P}\parallel \left({C}{B}+{A}{D}\right)$
19 1 10 11 12 13 14 15 16 17 18 2sqlem3 ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}+{A}{D}\right)\right)\to {N}\in {S}$
20 2 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {N}\in ℕ$
21 3 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {P}\in ℙ$
22 4 znegcld ${⊢}{\phi }\to -{A}\in ℤ$
23 22 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to -{A}\in ℤ$
24 5 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {B}\in ℤ$
25 6 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {C}\in ℤ$
26 7 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {D}\in ℤ$
27 4 zcnd ${⊢}{\phi }\to {A}\in ℂ$
28 sqneg ${⊢}{A}\in ℂ\to {\left(-{A}\right)}^{2}={{A}}^{2}$
29 27 28 syl ${⊢}{\phi }\to {\left(-{A}\right)}^{2}={{A}}^{2}$
30 29 oveq1d ${⊢}{\phi }\to {\left(-{A}\right)}^{2}+{{B}}^{2}={{A}}^{2}+{{B}}^{2}$
31 8 30 eqtr4d ${⊢}{\phi }\to {N}{P}={\left(-{A}\right)}^{2}+{{B}}^{2}$
32 31 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {N}{P}={\left(-{A}\right)}^{2}+{{B}}^{2}$
33 9 adantr ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {P}={{C}}^{2}+{{D}}^{2}$
34 7 zcnd ${⊢}{\phi }\to {D}\in ℂ$
35 27 34 mulneg1d ${⊢}{\phi }\to \left(-{A}\right){D}=-{A}{D}$
36 35 oveq2d ${⊢}{\phi }\to {C}{B}+\left(-{A}\right){D}={C}{B}+\left(-{A}{D}\right)$
37 6 5 zmulcld ${⊢}{\phi }\to {C}{B}\in ℤ$
38 37 zcnd ${⊢}{\phi }\to {C}{B}\in ℂ$
39 4 7 zmulcld ${⊢}{\phi }\to {A}{D}\in ℤ$
40 39 zcnd ${⊢}{\phi }\to {A}{D}\in ℂ$
41 38 40 negsubd ${⊢}{\phi }\to {C}{B}+\left(-{A}{D}\right)={C}{B}-{A}{D}$
42 36 41 eqtrd ${⊢}{\phi }\to {C}{B}+\left(-{A}\right){D}={C}{B}-{A}{D}$
43 42 breq2d ${⊢}{\phi }\to \left({P}\parallel \left({C}{B}+\left(-{A}\right){D}\right)↔{P}\parallel \left({C}{B}-{A}{D}\right)\right)$
44 43 biimpar ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {P}\parallel \left({C}{B}+\left(-{A}\right){D}\right)$
45 1 20 21 23 24 25 26 32 33 44 2sqlem3 ${⊢}\left({\phi }\wedge {P}\parallel \left({C}{B}-{A}{D}\right)\right)\to {N}\in {S}$
46 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
47 3 46 syl ${⊢}{\phi }\to {P}\in ℤ$
48 zsqcl ${⊢}{C}\in ℤ\to {{C}}^{2}\in ℤ$
49 6 48 syl ${⊢}{\phi }\to {{C}}^{2}\in ℤ$
50 2 nnzd ${⊢}{\phi }\to {N}\in ℤ$
51 49 50 zmulcld ${⊢}{\phi }\to {{C}}^{2}\cdot {N}\in ℤ$
52 zsqcl ${⊢}{A}\in ℤ\to {{A}}^{2}\in ℤ$
53 4 52 syl ${⊢}{\phi }\to {{A}}^{2}\in ℤ$
54 51 53 zsubcld ${⊢}{\phi }\to {{C}}^{2}\cdot {N}-{{A}}^{2}\in ℤ$
55 dvdsmul1 ${⊢}\left({P}\in ℤ\wedge {{C}}^{2}\cdot {N}-{{A}}^{2}\in ℤ\right)\to {P}\parallel {P}\left({{C}}^{2}\cdot {N}-{{A}}^{2}\right)$
56 47 54 55 syl2anc ${⊢}{\phi }\to {P}\parallel {P}\left({{C}}^{2}\cdot {N}-{{A}}^{2}\right)$
57 6 4 zmulcld ${⊢}{\phi }\to {C}{A}\in ℤ$
58 57 zcnd ${⊢}{\phi }\to {C}{A}\in ℂ$
59 58 sqcld ${⊢}{\phi }\to {{C}{A}}^{2}\in ℂ$
60 38 sqcld ${⊢}{\phi }\to {{C}{B}}^{2}\in ℂ$
61 40 sqcld ${⊢}{\phi }\to {{A}{D}}^{2}\in ℂ$
62 59 60 61 pnpcand ${⊢}{\phi }\to {{C}{A}}^{2}+{{C}{B}}^{2}-\left({{C}{A}}^{2}+{{A}{D}}^{2}\right)={{C}{B}}^{2}-{{A}{D}}^{2}$
63 6 zcnd ${⊢}{\phi }\to {C}\in ℂ$
64 63 27 sqmuld ${⊢}{\phi }\to {{C}{A}}^{2}={{C}}^{2}{{A}}^{2}$
65 5 zcnd ${⊢}{\phi }\to {B}\in ℂ$
66 63 65 sqmuld ${⊢}{\phi }\to {{C}{B}}^{2}={{C}}^{2}{{B}}^{2}$
67 64 66 oveq12d ${⊢}{\phi }\to {{C}{A}}^{2}+{{C}{B}}^{2}={{C}}^{2}{{A}}^{2}+{{C}}^{2}{{B}}^{2}$
68 63 sqcld ${⊢}{\phi }\to {{C}}^{2}\in ℂ$
69 53 zcnd ${⊢}{\phi }\to {{A}}^{2}\in ℂ$
70 65 sqcld ${⊢}{\phi }\to {{B}}^{2}\in ℂ$
71 68 69 70 adddid ${⊢}{\phi }\to {{C}}^{2}\left({{A}}^{2}+{{B}}^{2}\right)={{C}}^{2}{{A}}^{2}+{{C}}^{2}{{B}}^{2}$
72 67 71 eqtr4d ${⊢}{\phi }\to {{C}{A}}^{2}+{{C}{B}}^{2}={{C}}^{2}\left({{A}}^{2}+{{B}}^{2}\right)$
73 2 nncnd ${⊢}{\phi }\to {N}\in ℂ$
74 47 zcnd ${⊢}{\phi }\to {P}\in ℂ$
75 73 74 mulcomd ${⊢}{\phi }\to {N}{P}={P}\cdot {N}$
76 8 75 eqtr3d ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}={P}\cdot {N}$
77 76 oveq2d ${⊢}{\phi }\to {{C}}^{2}\left({{A}}^{2}+{{B}}^{2}\right)={{C}}^{2}{P}\cdot {N}$
78 68 74 73 mul12d ${⊢}{\phi }\to {{C}}^{2}{P}\cdot {N}={P}{{C}}^{2}\cdot {N}$
79 77 78 eqtrd ${⊢}{\phi }\to {{C}}^{2}\left({{A}}^{2}+{{B}}^{2}\right)={P}{{C}}^{2}\cdot {N}$
80 72 79 eqtrd ${⊢}{\phi }\to {{C}{A}}^{2}+{{C}{B}}^{2}={P}{{C}}^{2}\cdot {N}$
81 27 34 sqmuld ${⊢}{\phi }\to {{A}{D}}^{2}={{A}}^{2}{{D}}^{2}$
82 34 sqcld ${⊢}{\phi }\to {{D}}^{2}\in ℂ$
83 69 82 mulcomd ${⊢}{\phi }\to {{A}}^{2}{{D}}^{2}={{D}}^{2}{{A}}^{2}$
84 81 83 eqtrd ${⊢}{\phi }\to {{A}{D}}^{2}={{D}}^{2}{{A}}^{2}$
85 64 84 oveq12d ${⊢}{\phi }\to {{C}{A}}^{2}+{{A}{D}}^{2}={{C}}^{2}{{A}}^{2}+{{D}}^{2}{{A}}^{2}$
86 49 zcnd ${⊢}{\phi }\to {{C}}^{2}\in ℂ$
87 86 82 69 adddird ${⊢}{\phi }\to \left({{C}}^{2}+{{D}}^{2}\right){{A}}^{2}={{C}}^{2}{{A}}^{2}+{{D}}^{2}{{A}}^{2}$
88 85 87 eqtr4d ${⊢}{\phi }\to {{C}{A}}^{2}+{{A}{D}}^{2}=\left({{C}}^{2}+{{D}}^{2}\right){{A}}^{2}$
89 9 oveq1d ${⊢}{\phi }\to {P}{{A}}^{2}=\left({{C}}^{2}+{{D}}^{2}\right){{A}}^{2}$
90 88 89 eqtr4d ${⊢}{\phi }\to {{C}{A}}^{2}+{{A}{D}}^{2}={P}{{A}}^{2}$
91 80 90 oveq12d ${⊢}{\phi }\to {{C}{A}}^{2}+{{C}{B}}^{2}-\left({{C}{A}}^{2}+{{A}{D}}^{2}\right)={P}{{C}}^{2}\cdot {N}-{P}{{A}}^{2}$
92 51 zcnd ${⊢}{\phi }\to {{C}}^{2}\cdot {N}\in ℂ$
93 74 92 69 subdid ${⊢}{\phi }\to {P}\left({{C}}^{2}\cdot {N}-{{A}}^{2}\right)={P}{{C}}^{2}\cdot {N}-{P}{{A}}^{2}$
94 91 93 eqtr4d ${⊢}{\phi }\to {{C}{A}}^{2}+{{C}{B}}^{2}-\left({{C}{A}}^{2}+{{A}{D}}^{2}\right)={P}\left({{C}}^{2}\cdot {N}-{{A}}^{2}\right)$
95 62 94 eqtr3d ${⊢}{\phi }\to {{C}{B}}^{2}-{{A}{D}}^{2}={P}\left({{C}}^{2}\cdot {N}-{{A}}^{2}\right)$
96 subsq ${⊢}\left({C}{B}\in ℂ\wedge {A}{D}\in ℂ\right)\to {{C}{B}}^{2}-{{A}{D}}^{2}=\left({C}{B}+{A}{D}\right)\left({C}{B}-{A}{D}\right)$
97 38 40 96 syl2anc ${⊢}{\phi }\to {{C}{B}}^{2}-{{A}{D}}^{2}=\left({C}{B}+{A}{D}\right)\left({C}{B}-{A}{D}\right)$
98 95 97 eqtr3d ${⊢}{\phi }\to {P}\left({{C}}^{2}\cdot {N}-{{A}}^{2}\right)=\left({C}{B}+{A}{D}\right)\left({C}{B}-{A}{D}\right)$
99 56 98 breqtrd ${⊢}{\phi }\to {P}\parallel \left({C}{B}+{A}{D}\right)\left({C}{B}-{A}{D}\right)$
100 37 39 zaddcld ${⊢}{\phi }\to {C}{B}+{A}{D}\in ℤ$
101 37 39 zsubcld ${⊢}{\phi }\to {C}{B}-{A}{D}\in ℤ$
102 euclemma ${⊢}\left({P}\in ℙ\wedge {C}{B}+{A}{D}\in ℤ\wedge {C}{B}-{A}{D}\in ℤ\right)\to \left({P}\parallel \left({C}{B}+{A}{D}\right)\left({C}{B}-{A}{D}\right)↔\left({P}\parallel \left({C}{B}+{A}{D}\right)\vee {P}\parallel \left({C}{B}-{A}{D}\right)\right)\right)$
103 3 100 101 102 syl3anc ${⊢}{\phi }\to \left({P}\parallel \left({C}{B}+{A}{D}\right)\left({C}{B}-{A}{D}\right)↔\left({P}\parallel \left({C}{B}+{A}{D}\right)\vee {P}\parallel \left({C}{B}-{A}{D}\right)\right)\right)$
104 99 103 mpbid ${⊢}{\phi }\to \left({P}\parallel \left({C}{B}+{A}{D}\right)\vee {P}\parallel \left({C}{B}-{A}{D}\right)\right)$
105 19 45 104 mpjaodan ${⊢}{\phi }\to {N}\in {S}$