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

Metamath Proof Explorer

Theorem 2sqlem3

Proof