2sqlem3

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

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2		2sqlem5.1	$⊢ φ \to N \in ℕ$
3		2sqlem5.2	$⊢ φ \to P \in ℙ$
4		2sqlem4.3	$⊢ φ \to A \in ℤ$
5		2sqlem4.4	$⊢ φ \to B \in ℤ$
6		2sqlem4.5	$⊢ φ \to C \in ℤ$
7		2sqlem4.6	$⊢ φ \to D \in ℤ$
8		2sqlem4.7	$⊢ φ \to N P = A^{2} + B^{2}$
9		2sqlem4.8	$⊢ φ \to P = C^{2} + D^{2}$
10		2sqlem4.9	$⊢ φ \to P ∥ (C B + A D)$
11		gzreim	$⊢ (A \in ℤ \land B \in ℤ) \to A + i B \in ℤ [i]$
12	4 5 11	syl2anc	$⊢ φ \to A + i B \in ℤ [i]$
13		gzreim	$⊢ (C \in ℤ \land D \in ℤ) \to C + i D \in ℤ [i]$
14	6 7 13	syl2anc	$⊢ φ \to C + i D \in ℤ [i]$
15		gzmulcl	$⊢ (A + i B \in ℤ [i] \land C + i D \in ℤ [i]) \to (A + i B) (C + i D) \in ℤ [i]$
16	12 14 15	syl2anc	$⊢ φ \to (A + i B) (C + i D) \in ℤ [i]$
17		gzcn	$⊢ (A + i B) (C + i D) \in ℤ [i] \to (A + i B) (C + i D) \in ℂ$
18	16 17	syl	$⊢ φ \to (A + i B) (C + i D) \in ℂ$
19		prmnn	$⊢ P \in ℙ \to P \in ℕ$
20	3 19	syl	$⊢ φ \to P \in ℕ$
21	20	nncnd	$⊢ φ \to P \in ℂ$
22	20	nnne0d	$⊢ φ \to P \neq 0$
23	18 21 22	divcld	$⊢ φ \to \frac{(A + i B) (C + i D)}{P} \in ℂ$
24	20	nnred	$⊢ φ \to P \in ℝ$
25	24 18 22	redivd	$⊢ φ \to ℜ (\frac{(A + i B) (C + i D)}{P}) = \frac{ℜ ((A + i B) (C + i D))}{P}$
26		prmz	$⊢ P \in ℙ \to P \in ℤ$
27	3 26	syl	$⊢ φ \to P \in ℤ$
28		zsqcl	$⊢ P \in ℤ \to P^{2} \in ℤ$
29	27 28	syl	$⊢ φ \to P^{2} \in ℤ$
30	2	nnzd	$⊢ φ \to N \in ℤ$
31	30 29	zmulcld	$⊢ φ \to N P^{2} \in ℤ$
32		dvdsmul2	$⊢ (P \in ℤ \land P \in ℤ) \to P ∥ P P$
33	27 27 32	syl2anc	$⊢ φ \to P ∥ P P$
34	21	sqvald	$⊢ φ \to P^{2} = P P$
35	33 34	breqtrrd	$⊢ φ \to P ∥ P^{2}$
36		dvdsmul2	$⊢ (N \in ℤ \land P^{2} \in ℤ) \to P^{2} ∥ N P^{2}$
37	30 29 36	syl2anc	$⊢ φ \to P^{2} ∥ N P^{2}$
38	27 29 31 35 37	dvdstrd	$⊢ φ \to P ∥ N P^{2}$
39		gzcn	$⊢ A + i B \in ℤ [i] \to A + i B \in ℂ$
40	12 39	syl	$⊢ φ \to A + i B \in ℂ$
41	40	abscld	$⊢ φ \to \|A + i B\| \in ℝ$
42	41	recnd	$⊢ φ \to \|A + i B\| \in ℂ$
43		gzcn	$⊢ C + i D \in ℤ [i] \to C + i D \in ℂ$
44	14 43	syl	$⊢ φ \to C + i D \in ℂ$
45	44	abscld	$⊢ φ \to \|C + i D\| \in ℝ$
46	45	recnd	$⊢ φ \to \|C + i D\| \in ℂ$
47	42 46	sqmuld	$⊢ φ \to {\|A + i B\| \|C + i D\|}^{2} = {\|A + i B\|}^{2} {\|C + i D\|}^{2}$
48	4	zred	$⊢ φ \to A \in ℝ$
49	5	zred	$⊢ φ \to B \in ℝ$
50	48 49	crred	$⊢ φ \to ℜ (A + i B) = A$
51	50	oveq1d	$⊢ φ \to {ℜ (A + i B)}^{2} = A^{2}$
52	48 49	crimd	$⊢ φ \to ℑ (A + i B) = B$
53	52	oveq1d	$⊢ φ \to {ℑ (A + i B)}^{2} = B^{2}$
54	51 53	oveq12d	$⊢ φ \to {ℜ (A + i B)}^{2} + {ℑ (A + i B)}^{2} = A^{2} + B^{2}$
55	40	absvalsq2d	$⊢ φ \to {\|A + i B\|}^{2} = {ℜ (A + i B)}^{2} + {ℑ (A + i B)}^{2}$
56	54 55 8	3eqtr4d	$⊢ φ \to {\|A + i B\|}^{2} = N P$
57	6	zred	$⊢ φ \to C \in ℝ$
58	7	zred	$⊢ φ \to D \in ℝ$
59	57 58	crred	$⊢ φ \to ℜ (C + i D) = C$
60	59	oveq1d	$⊢ φ \to {ℜ (C + i D)}^{2} = C^{2}$
61	57 58	crimd	$⊢ φ \to ℑ (C + i D) = D$
62	61	oveq1d	$⊢ φ \to {ℑ (C + i D)}^{2} = D^{2}$
63	60 62	oveq12d	$⊢ φ \to {ℜ (C + i D)}^{2} + {ℑ (C + i D)}^{2} = C^{2} + D^{2}$
64	44	absvalsq2d	$⊢ φ \to {\|C + i D\|}^{2} = {ℜ (C + i D)}^{2} + {ℑ (C + i D)}^{2}$
65	63 64 9	3eqtr4d	$⊢ φ \to {\|C + i D\|}^{2} = P$
66	56 65	oveq12d	$⊢ φ \to {\|A + i B\|}^{2} {\|C + i D\|}^{2} = N P P$
67	2	nncnd	$⊢ φ \to N \in ℂ$
68	67 21 21	mulassd	$⊢ φ \to N P P = N P P$
69	47 66 68	3eqtrd	$⊢ φ \to {\|A + i B\| \|C + i D\|}^{2} = N P P$
70	40 44	absmuld	$⊢ φ \to \|(A + i B) (C + i D)\| = \|A + i B\| \|C + i D\|$
71	70	oveq1d	$⊢ φ \to {\|(A + i B) (C + i D)\|}^{2} = {\|A + i B\| \|C + i D\|}^{2}$
72	34	oveq2d	$⊢ φ \to N P^{2} = N P P$
73	69 71 72	3eqtr4d	$⊢ φ \to {\|(A + i B) (C + i D)\|}^{2} = N P^{2}$
74	38 73	breqtrrd	$⊢ φ \to P ∥ {\|(A + i B) (C + i D)\|}^{2}$
75	18	absvalsq2d	$⊢ φ \to {\|(A + i B) (C + i D)\|}^{2} = {ℜ ((A + i B) (C + i D))}^{2} + {ℑ ((A + i B) (C + i D))}^{2}$
76		elgz	$⊢ (A + i B) (C + i D) \in ℤ [i] \leftrightarrow ((A + i B) (C + i D) \in ℂ \land ℜ ((A + i B) (C + i D)) \in ℤ \land ℑ ((A + i B) (C + i D)) \in ℤ)$
77	76	simp2bi	$⊢ (A + i B) (C + i D) \in ℤ [i] \to ℜ ((A + i B) (C + i D)) \in ℤ$
78	16 77	syl	$⊢ φ \to ℜ ((A + i B) (C + i D)) \in ℤ$
79		zsqcl	$⊢ ℜ ((A + i B) (C + i D)) \in ℤ \to {ℜ ((A + i B) (C + i D))}^{2} \in ℤ$
80	78 79	syl	$⊢ φ \to {ℜ ((A + i B) (C + i D))}^{2} \in ℤ$
81	80	zcnd	$⊢ φ \to {ℜ ((A + i B) (C + i D))}^{2} \in ℂ$
82	76	simp3bi	$⊢ (A + i B) (C + i D) \in ℤ [i] \to ℑ ((A + i B) (C + i D)) \in ℤ$
83	16 82	syl	$⊢ φ \to ℑ ((A + i B) (C + i D)) \in ℤ$
84		zsqcl	$⊢ ℑ ((A + i B) (C + i D)) \in ℤ \to {ℑ ((A + i B) (C + i D))}^{2} \in ℤ$
85	83 84	syl	$⊢ φ \to {ℑ ((A + i B) (C + i D))}^{2} \in ℤ$
86	85	zcnd	$⊢ φ \to {ℑ ((A + i B) (C + i D))}^{2} \in ℂ$
87	81 86	addcomd	$⊢ φ \to {ℜ ((A + i B) (C + i D))}^{2} + {ℑ ((A + i B) (C + i D))}^{2} = {ℑ ((A + i B) (C + i D))}^{2} + {ℜ ((A + i B) (C + i D))}^{2}$
88	75 87	eqtrd	$⊢ φ \to {\|(A + i B) (C + i D)\|}^{2} = {ℑ ((A + i B) (C + i D))}^{2} + {ℜ ((A + i B) (C + i D))}^{2}$
89	74 88	breqtrd	$⊢ φ \to P ∥ ({ℑ ((A + i B) (C + i D))}^{2} + {ℜ ((A + i B) (C + i D))}^{2})$
90	6	zcnd	$⊢ φ \to C \in ℂ$
91	5	zcnd	$⊢ φ \to B \in ℂ$
92	90 91	mulcld	$⊢ φ \to C B \in ℂ$
93	4	zcnd	$⊢ φ \to A \in ℂ$
94	7	zcnd	$⊢ φ \to D \in ℂ$
95	93 94	mulcld	$⊢ φ \to A D \in ℂ$
96	92 95	addcomd	$⊢ φ \to C B + A D = A D + C B$
97	90 91	mulcomd	$⊢ φ \to C B = B C$
98	97	oveq2d	$⊢ φ \to A D + C B = A D + B C$
99	96 98	eqtrd	$⊢ φ \to C B + A D = A D + B C$
100	10 99	breqtrd	$⊢ φ \to P ∥ (A D + B C)$
101	40 44	immuld	$⊢ φ \to ℑ ((A + i B) (C + i D)) = ℜ (A + i B) ℑ (C + i D) + ℑ (A + i B) ℜ (C + i D)$
102	50 61	oveq12d	$⊢ φ \to ℜ (A + i B) ℑ (C + i D) = A D$
103	52 59	oveq12d	$⊢ φ \to ℑ (A + i B) ℜ (C + i D) = B C$
104	102 103	oveq12d	$⊢ φ \to ℜ (A + i B) ℑ (C + i D) + ℑ (A + i B) ℜ (C + i D) = A D + B C$
105	101 104	eqtrd	$⊢ φ \to ℑ ((A + i B) (C + i D)) = A D + B C$
106	100 105	breqtrrd	$⊢ φ \to P ∥ ℑ ((A + i B) (C + i D))$
107		2nn	$⊢ 2 \in ℕ$
108	107	a1i	$⊢ φ \to 2 \in ℕ$
109		prmdvdsexp	$⊢ (P \in ℙ \land ℑ ((A + i B) (C + i D)) \in ℤ \land 2 \in ℕ) \to (P ∥ {ℑ ((A + i B) (C + i D))}^{2} \leftrightarrow P ∥ ℑ ((A + i B) (C + i D)))$
110	3 83 108 109	syl3anc	$⊢ φ \to (P ∥ {ℑ ((A + i B) (C + i D))}^{2} \leftrightarrow P ∥ ℑ ((A + i B) (C + i D)))$
111	106 110	mpbird	$⊢ φ \to P ∥ {ℑ ((A + i B) (C + i D))}^{2}$
112		dvdsadd2b	$⊢ (P \in ℤ \land {ℜ ((A + i B) (C + i D))}^{2} \in ℤ \land ({ℑ ((A + i B) (C + i D))}^{2} \in ℤ \land P ∥ {ℑ ((A + i B) (C + i D))}^{2})) \to (P ∥ {ℜ ((A + i B) (C + i D))}^{2} \leftrightarrow P ∥ ({ℑ ((A + i B) (C + i D))}^{2} + {ℜ ((A + i B) (C + i D))}^{2}))$
113	27 80 85 111 112	syl112anc	$⊢ φ \to (P ∥ {ℜ ((A + i B) (C + i D))}^{2} \leftrightarrow P ∥ ({ℑ ((A + i B) (C + i D))}^{2} + {ℜ ((A + i B) (C + i D))}^{2}))$
114	89 113	mpbird	$⊢ φ \to P ∥ {ℜ ((A + i B) (C + i D))}^{2}$
115		prmdvdsexp	$⊢ (P \in ℙ \land ℜ ((A + i B) (C + i D)) \in ℤ \land 2 \in ℕ) \to (P ∥ {ℜ ((A + i B) (C + i D))}^{2} \leftrightarrow P ∥ ℜ ((A + i B) (C + i D)))$
116	3 78 108 115	syl3anc	$⊢ φ \to (P ∥ {ℜ ((A + i B) (C + i D))}^{2} \leftrightarrow P ∥ ℜ ((A + i B) (C + i D)))$
117	114 116	mpbid	$⊢ φ \to P ∥ ℜ ((A + i B) (C + i D))$
118		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land ℜ ((A + i B) (C + i D)) \in ℤ) \to (P ∥ ℜ ((A + i B) (C + i D)) \leftrightarrow \frac{ℜ ((A + i B) (C + i D))}{P} \in ℤ)$
119	27 22 78 118	syl3anc	$⊢ φ \to (P ∥ ℜ ((A + i B) (C + i D)) \leftrightarrow \frac{ℜ ((A + i B) (C + i D))}{P} \in ℤ)$
120	117 119	mpbid	$⊢ φ \to \frac{ℜ ((A + i B) (C + i D))}{P} \in ℤ$
121	25 120	eqeltrd	$⊢ φ \to ℜ (\frac{(A + i B) (C + i D)}{P}) \in ℤ$
122	24 18 22	imdivd	$⊢ φ \to ℑ (\frac{(A + i B) (C + i D)}{P}) = \frac{ℑ ((A + i B) (C + i D))}{P}$
123		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land ℑ ((A + i B) (C + i D)) \in ℤ) \to (P ∥ ℑ ((A + i B) (C + i D)) \leftrightarrow \frac{ℑ ((A + i B) (C + i D))}{P} \in ℤ)$
124	27 22 83 123	syl3anc	$⊢ φ \to (P ∥ ℑ ((A + i B) (C + i D)) \leftrightarrow \frac{ℑ ((A + i B) (C + i D))}{P} \in ℤ)$
125	106 124	mpbid	$⊢ φ \to \frac{ℑ ((A + i B) (C + i D))}{P} \in ℤ$
126	122 125	eqeltrd	$⊢ φ \to ℑ (\frac{(A + i B) (C + i D)}{P}) \in ℤ$
127		elgz	$⊢ \frac{(A + i B) (C + i D)}{P} \in ℤ [i] \leftrightarrow (\frac{(A + i B) (C + i D)}{P} \in ℂ \land ℜ (\frac{(A + i B) (C + i D)}{P}) \in ℤ \land ℑ (\frac{(A + i B) (C + i D)}{P}) \in ℤ)$
128	23 121 126 127	syl3anbrc	$⊢ φ \to \frac{(A + i B) (C + i D)}{P} \in ℤ [i]$
129	18 21 22	absdivd	$⊢ φ \to \|\frac{(A + i B) (C + i D)}{P}\| = \frac{\|(A + i B) (C + i D)\|}{\|P\|}$
130	20	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
131	130	nn0ge0d	$⊢ φ \to 0 \leq P$
132	24 131	absidd	$⊢ φ \to \|P\| = P$
133	132	oveq2d	$⊢ φ \to \frac{\|(A + i B) (C + i D)\|}{\|P\|} = \frac{\|(A + i B) (C + i D)\|}{P}$
134	129 133	eqtrd	$⊢ φ \to \|\frac{(A + i B) (C + i D)}{P}\| = \frac{\|(A + i B) (C + i D)\|}{P}$
135	134	oveq1d	$⊢ φ \to {\|\frac{(A + i B) (C + i D)}{P}\|}^{2} = {(\frac{\|(A + i B) (C + i D)\|}{P})}^{2}$
136	18	abscld	$⊢ φ \to \|(A + i B) (C + i D)\| \in ℝ$
137	136	recnd	$⊢ φ \to \|(A + i B) (C + i D)\| \in ℂ$
138	137 21 22	sqdivd	$⊢ φ \to {(\frac{\|(A + i B) (C + i D)\|}{P})}^{2} = \frac{{\|(A + i B) (C + i D)\|}^{2}}{P^{2}}$
139	73	oveq1d	$⊢ φ \to \frac{{\|(A + i B) (C + i D)\|}^{2}}{P^{2}} = \frac{N P^{2}}{P^{2}}$
140	20	nnsqcld	$⊢ φ \to P^{2} \in ℕ$
141	140	nncnd	$⊢ φ \to P^{2} \in ℂ$
142	140	nnne0d	$⊢ φ \to P^{2} \neq 0$
143	67 141 142	divcan4d	$⊢ φ \to \frac{N P^{2}}{P^{2}} = N$
144	139 143	eqtrd	$⊢ φ \to \frac{{\|(A + i B) (C + i D)\|}^{2}}{P^{2}} = N$
145	135 138 144	3eqtrrd	$⊢ φ \to N = {\|\frac{(A + i B) (C + i D)}{P}\|}^{2}$
146		fveq2	$⊢ x = \frac{(A + i B) (C + i D)}{P} \to \|x\| = \|\frac{(A + i B) (C + i D)}{P}\|$
147	146	oveq1d	$⊢ x = \frac{(A + i B) (C + i D)}{P} \to {\|x\|}^{2} = {\|\frac{(A + i B) (C + i D)}{P}\|}^{2}$
148	147	rspceeqv	$⊢ (\frac{(A + i B) (C + i D)}{P} \in ℤ [i] \land N = {\|\frac{(A + i B) (C + i D)}{P}\|}^{2}) \to \exists x \in ℤ [i] N = {\|x\|}^{2}$
149	128 145 148	syl2anc	$⊢ φ \to \exists x \in ℤ [i] N = {\|x\|}^{2}$
150	1	2sqlem1	$⊢ N \in S \leftrightarrow \exists x \in ℤ [i] N = {\|x\|}^{2}$
151	149 150	sylibr	$⊢ φ \to N \in S$

Metamath Proof Explorer

Theorem 2sqlem3

Proof