bhmafibid2

Description: The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020)

		Ref	Expression
	Assertion	bhmafibid2	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A^{2} + B^{2}) (C^{2} + D^{2}) = {(A C + B D)}^{2} + {(A D - B C)}^{2}$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C \in ℝ$
2	1	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C \in ℂ$
3	2	sqcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C^{2} \in ℂ$
4		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D \in ℝ$
5	4	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D \in ℂ$
6	5	sqcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D^{2} \in ℂ$
7	3 6	addcomd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C^{2} + D^{2} = D^{2} + C^{2}$
8	7	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A^{2} + B^{2}) (C^{2} + D^{2}) = (A^{2} + B^{2}) (D^{2} + C^{2})$
9		bhmafibid1	$⊢ ((A \in ℝ \land B \in ℝ) \land (D \in ℝ \land C \in ℝ)) \to (A^{2} + B^{2}) (D^{2} + C^{2}) = {(A D - B C)}^{2} + {(A C + B D)}^{2}$
10	9	ancom2s	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A^{2} + B^{2}) (D^{2} + C^{2}) = {(A D - B C)}^{2} + {(A C + B D)}^{2}$
11		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A \in ℝ$
12	11	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A \in ℂ$
13	12 5	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A D \in ℂ$
14		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B \in ℝ$
15	14	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B \in ℂ$
16	15 2	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B C \in ℂ$
17	13 16	subcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A D - B C \in ℂ$
18	17	sqcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {(A D - B C)}^{2} \in ℂ$
19	12 2	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A C \in ℂ$
20	15 5	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B D \in ℂ$
21	19 20	addcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A C + B D \in ℂ$
22	21	sqcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {(A C + B D)}^{2} \in ℂ$
23	18 22	addcomd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {(A D - B C)}^{2} + {(A C + B D)}^{2} = {(A C + B D)}^{2} + {(A D - B C)}^{2}$
24	8 10 23	3eqtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A^{2} + B^{2}) (C^{2} + D^{2}) = {(A C + B D)}^{2} + {(A D - B C)}^{2}$

Metamath Proof Explorer

Theorem bhmafibid2

Proof