bhmafibid1cn

Description: The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. First result. (Contributed by Thierry Arnoux, 1-Feb-2020) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023)

		Ref	Expression
	Assertion	bhmafibid1cn	$⊢ ((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		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A \in ℂ$
2	1	sqcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A^{2} \in ℂ$
3		simprl	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C \in ℂ$
4	3	sqcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C^{2} \in ℂ$
5	2 4	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A^{2} C^{2} \in ℂ$
6		simprr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D \in ℂ$
7	6	sqcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D^{2} \in ℂ$
8		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B \in ℂ$
9	8	sqcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B^{2} \in ℂ$
10	7 9	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D^{2} B^{2} \in ℂ$
11	2 7	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A^{2} D^{2} \in ℂ$
12	4 9	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C^{2} B^{2} \in ℂ$
13	5 10 11 12	add4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A^{2} C^{2} + D^{2} B^{2} + A^{2} D^{2} + C^{2} B^{2} = A^{2} C^{2} + A^{2} D^{2} + D^{2} B^{2} + C^{2} B^{2}$
14	7 9	mulcomd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D^{2} B^{2} = B^{2} D^{2}$
15	4 9	mulcomd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to C^{2} B^{2} = B^{2} C^{2}$
16	14 15	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to D^{2} B^{2} + C^{2} B^{2} = B^{2} D^{2} + B^{2} C^{2}$
17	16	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A^{2} C^{2} + A^{2} D^{2} + D^{2} B^{2} + C^{2} B^{2} = A^{2} C^{2} + A^{2} D^{2} + B^{2} D^{2} + B^{2} C^{2}$
18	13 17	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A^{2} C^{2} + D^{2} B^{2} + A^{2} D^{2} + C^{2} B^{2} = A^{2} C^{2} + A^{2} D^{2} + B^{2} D^{2} + B^{2} C^{2}$
19	2 9 4 7	muladdd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to (A^{2} + B^{2}) (C^{2} + D^{2}) = A^{2} C^{2} + D^{2} B^{2} + A^{2} D^{2} + C^{2} B^{2}$
20	1 3	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C \in ℂ$
21	8 6	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B D \in ℂ$
22		binom2sub	$⊢ (A C \in ℂ \land B D \in ℂ) \to {(A C - B D)}^{2} = {A C}^{2} - 2 A C B D + {B D}^{2}$
23	20 21 22	syl2anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {(A C - B D)}^{2} = {A C}^{2} - 2 A C B D + {B D}^{2}$
24	1 6	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A D \in ℂ$
25	8 3	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to B C \in ℂ$
26		binom2	$⊢ (A D \in ℂ \land B C \in ℂ) \to {(A D + B C)}^{2} = {A D}^{2} + 2 A D B C + {B C}^{2}$
27	24 25 26	syl2anc	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {(A D + B C)}^{2} = {A D}^{2} + 2 A D B C + {B C}^{2}$
28	23 27	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {(A C - B D)}^{2} + {(A D + B C)}^{2} = ({A C}^{2} - 2 A C B D) + {B D}^{2} + ({A D}^{2} + 2 A D B C) + {B C}^{2}$
29	20	sqcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A C}^{2} \in ℂ$
30		2cnd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to 2 \in ℂ$
31	20 21	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C B D \in ℂ$
32	30 31	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to 2 A C B D \in ℂ$
33	29 32	subcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A C}^{2} - 2 A C B D \in ℂ$
34	21	sqcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {B D}^{2} \in ℂ$
35	24	sqcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A D}^{2} \in ℂ$
36	24 25	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A D B C \in ℂ$
37	30 36	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to 2 A D B C \in ℂ$
38	35 37	addcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A D}^{2} + 2 A D B C \in ℂ$
39	25	sqcld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {B C}^{2} \in ℂ$
40	33 34 38 39	add4d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to ({A C}^{2} - 2 A C B D) + {B D}^{2} + ({A D}^{2} + 2 A D B C) + {B C}^{2} = ({A C}^{2} - 2 A C B D) + ({A D}^{2} + 2 A D B C) + {B D}^{2} + {B C}^{2}$
41		mul4r	$⊢ ((A \in ℂ \land C \in ℂ) \land (B \in ℂ \land D \in ℂ)) \to A C B D = A D B C$
42	41	an4s	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C B D = A D B C$
43	42	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to 2 A C B D = 2 A D B C$
44	43	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A C}^{2} - 2 A C B D = {A C}^{2} - 2 A D B C$
45	44	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to ({A C}^{2} - 2 A C B D) + {A D}^{2} + 2 A D B C = ({A C}^{2} - 2 A D B C) + {A D}^{2} + 2 A D B C$
46	29 37 35	nppcan3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to ({A C}^{2} - 2 A D B C) + {A D}^{2} + 2 A D B C = {A C}^{2} + {A D}^{2}$
47	45 46	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to ({A C}^{2} - 2 A C B D) + {A D}^{2} + 2 A D B C = {A C}^{2} + {A D}^{2}$
48	8 6	sqmuld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {B D}^{2} = B^{2} D^{2}$
49	8 3	sqmuld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {B C}^{2} = B^{2} C^{2}$
50	48 49	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {B D}^{2} + {B C}^{2} = B^{2} D^{2} + B^{2} C^{2}$
51	47 50	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to ({A C}^{2} - 2 A C B D) + ({A D}^{2} + 2 A D B C) + {B D}^{2} + {B C}^{2} = {A C}^{2} + {A D}^{2} + B^{2} D^{2} + B^{2} C^{2}$
52	1 3	sqmuld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A C}^{2} = A^{2} C^{2}$
53	1 6	sqmuld	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A D}^{2} = A^{2} D^{2}$
54	52 53	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A C}^{2} + {A D}^{2} = A^{2} C^{2} + A^{2} D^{2}$
55	54	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {A C}^{2} + {A D}^{2} + B^{2} D^{2} + B^{2} C^{2} = A^{2} C^{2} + A^{2} D^{2} + B^{2} D^{2} + B^{2} C^{2}$
56	51 55	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to ({A C}^{2} - 2 A C B D) + ({A D}^{2} + 2 A D B C) + {B D}^{2} + {B C}^{2} = A^{2} C^{2} + A^{2} D^{2} + B^{2} D^{2} + B^{2} C^{2}$
57	28 40 56	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to {(A C - B D)}^{2} + {(A D + B C)}^{2} = A^{2} C^{2} + A^{2} D^{2} + B^{2} D^{2} + B^{2} C^{2}$
58	18 19 57	3eqtr4d	$⊢ ((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 bhmafibid1cn

Proof