mul2sq

Description: Fibonacci's identity (actually due to Diophantus). The product of two sums of two squares is also a sum of two squares. We can take advantage of Gaussian integers here to trivialize the proof. (Contributed by Mario Carneiro, 19-Jun-2015)

		Ref	Expression
	Hypothesis	2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
	Assertion	mul2sq	$⊢ (A \in S \land B \in S) \to A B \in S$

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2	1	2sqlem1	$⊢ A \in S \leftrightarrow \exists x \in ℤ [i] A = {\|x\|}^{2}$
3	1	2sqlem1	$⊢ B \in S \leftrightarrow \exists y \in ℤ [i] B = {\|y\|}^{2}$
4		reeanv	$⊢ \exists x \in ℤ [i] \exists y \in ℤ [i] (A = {\|x\|}^{2} \land B = {\|y\|}^{2}) \leftrightarrow (\exists x \in ℤ [i] A = {\|x\|}^{2} \land \exists y \in ℤ [i] B = {\|y\|}^{2})$
5		gzmulcl	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to x y \in ℤ [i]$
6		gzcn	$⊢ x \in ℤ [i] \to x \in ℂ$
7		gzcn	$⊢ y \in ℤ [i] \to y \in ℂ$
8		absmul	$⊢ (x \in ℂ \land y \in ℂ) \to \|x y\| = \|x\| \|y\|$
9	6 7 8	syl2an	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to \|x y\| = \|x\| \|y\|$
10	9	oveq1d	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to {\|x y\|}^{2} = {\|x\| \|y\|}^{2}$
11	6	abscld	$⊢ x \in ℤ [i] \to \|x\| \in ℝ$
12	11	recnd	$⊢ x \in ℤ [i] \to \|x\| \in ℂ$
13	7	abscld	$⊢ y \in ℤ [i] \to \|y\| \in ℝ$
14	13	recnd	$⊢ y \in ℤ [i] \to \|y\| \in ℂ$
15		sqmul	$⊢ (\|x\| \in ℂ \land \|y\| \in ℂ) \to {\|x\| \|y\|}^{2} = {\|x\|}^{2} {\|y\|}^{2}$
16	12 14 15	syl2an	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to {\|x\| \|y\|}^{2} = {\|x\|}^{2} {\|y\|}^{2}$
17	10 16	eqtr2d	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to {\|x\|}^{2} {\|y\|}^{2} = {\|x y\|}^{2}$
18		fveq2	$⊢ z = x y \to \|z\| = \|x y\|$
19	18	oveq1d	$⊢ z = x y \to {\|z\|}^{2} = {\|x y\|}^{2}$
20	19	rspceeqv	$⊢ (x y \in ℤ [i] \land {\|x\|}^{2} {\|y\|}^{2} = {\|x y\|}^{2}) \to \exists z \in ℤ [i] {\|x\|}^{2} {\|y\|}^{2} = {\|z\|}^{2}$
21	5 17 20	syl2anc	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to \exists z \in ℤ [i] {\|x\|}^{2} {\|y\|}^{2} = {\|z\|}^{2}$
22	1	2sqlem1	$⊢ {\|x\|}^{2} {\|y\|}^{2} \in S \leftrightarrow \exists z \in ℤ [i] {\|x\|}^{2} {\|y\|}^{2} = {\|z\|}^{2}$
23	21 22	sylibr	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to {\|x\|}^{2} {\|y\|}^{2} \in S$
24		oveq12	$⊢ (A = {\|x\|}^{2} \land B = {\|y\|}^{2}) \to A B = {\|x\|}^{2} {\|y\|}^{2}$
25	24	eleq1d	$⊢ (A = {\|x\|}^{2} \land B = {\|y\|}^{2}) \to (A B \in S \leftrightarrow {\|x\|}^{2} {\|y\|}^{2} \in S)$
26	23 25	syl5ibrcom	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to ((A = {\|x\|}^{2} \land B = {\|y\|}^{2}) \to A B \in S)$
27	26	rexlimivv	$⊢ \exists x \in ℤ [i] \exists y \in ℤ [i] (A = {\|x\|}^{2} \land B = {\|y\|}^{2}) \to A B \in S$
28	4 27	sylbir	$⊢ (\exists x \in ℤ [i] A = {\|x\|}^{2} \land \exists y \in ℤ [i] B = {\|y\|}^{2}) \to A B \in S$
29	2 3 28	syl2anb	$⊢ (A \in S \land B \in S) \to A B \in S$

Metamath Proof Explorer

Theorem mul2sq

Proof