bhmafibid1

Description: The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. First result. Remark: The proof uses a different approach than the proof of bhmafibid1cn , and is a little bit shorter. (Contributed by Thierry Arnoux, 1-Feb-2020) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bhmafibid1	$⊢ ((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	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A \in ℂ$
3		ax-icn	$⊢ i \in ℂ$
4	3	a1i	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to i \in ℂ$
5		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B \in ℝ$
6	5	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B \in ℂ$
7	4 6	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to i B \in ℂ$
8	2 7	addcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A + i B \in ℂ$
9		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C \in ℝ$
10	9	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C \in ℂ$
11		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D \in ℝ$
12	11	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D \in ℂ$
13	4 12	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to i D \in ℂ$
14	10 13	addcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C + i D \in ℂ$
15	8 14	mulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A + i B) (C + i D) \in ℂ$
16	15	replimd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A + i B) (C + i D) = ℜ ((A + i B) (C + i D)) + i ℑ ((A + i B) (C + i D))$
17	8 14	remuld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ ((A + i B) (C + i D)) = ℜ (A + i B) ℜ (C + i D) - ℑ (A + i B) ℑ (C + i D)$
18	1 5	crred	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ (A + i B) = A$
19	9 11	crred	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ (C + i D) = C$
20	18 19	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ (A + i B) ℜ (C + i D) = A C$
21	1 5	crimd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℑ (A + i B) = B$
22	9 11	crimd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℑ (C + i D) = D$
23	21 22	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℑ (A + i B) ℑ (C + i D) = B D$
24	20 23	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ (A + i B) ℜ (C + i D) - ℑ (A + i B) ℑ (C + i D) = A C - B D$
25	17 24	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ ((A + i B) (C + i D)) = A C - B D$
26	8 14	immuld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℑ ((A + i B) (C + i D)) = ℜ (A + i B) ℑ (C + i D) + ℑ (A + i B) ℜ (C + i D)$
27	18 22	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ (A + i B) ℑ (C + i D) = A D$
28	21 19	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℑ (A + i B) ℜ (C + i D) = B C$
29	27 28	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ (A + i B) ℑ (C + i D) + ℑ (A + i B) ℜ (C + i D) = A D + B C$
30	26 29	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℑ ((A + i B) (C + i D)) = A D + B C$
31	30	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to i ℑ ((A + i B) (C + i D)) = i (A D + B C)$
32	25 31	oveq12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ℜ ((A + i B) (C + i D)) + i ℑ ((A + i B) (C + i D)) = A C - B D + i (A D + B C)$
33	16 32	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A + i B) (C + i D) = A C - B D + i (A D + B C)$
34	33	fveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to \|(A + i B) (C + i D)\| = \|A C - B D + i (A D + B C)\|$
35	34	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {\|(A + i B) (C + i D)\|}^{2} = {\|A C - B D + i (A D + B C)\|}^{2}$
36	8 14	absmuld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to \|(A + i B) (C + i D)\| = \|A + i B\| \|C + i D\|$
37	36	oveq1d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {\|(A + i B) (C + i D)\|}^{2} = {\|A + i B\| \|C + i D\|}^{2}$
38	8	abscld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to \|A + i B\| \in ℝ$
39	38	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to \|A + i B\| \in ℂ$
40	14	abscld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to \|C + i D\| \in ℝ$
41	40	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to \|C + i D\| \in ℂ$
42	39 41	sqmuld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {\|A + i B\| \|C + i D\|}^{2} = {\|A + i B\|}^{2} {\|C + i D\|}^{2}$
43		absreimsq	$⊢ (A \in ℝ \land B \in ℝ) \to {\|A + i B\|}^{2} = A^{2} + B^{2}$
44		absreimsq	$⊢ (C \in ℝ \land D \in ℝ) \to {\|C + i D\|}^{2} = C^{2} + D^{2}$
45	43 44	oveqan12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {\|A + i B\|}^{2} {\|C + i D\|}^{2} = (A^{2} + B^{2}) (C^{2} + D^{2})$
46	37 42 45	3eqtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {\|(A + i B) (C + i D)\|}^{2} = (A^{2} + B^{2}) (C^{2} + D^{2})$
47	1 9	remulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A C \in ℝ$
48	5 11	remulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B D \in ℝ$
49	47 48	resubcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A C - B D \in ℝ$
50	1 11	remulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A D \in ℝ$
51	5 9	remulcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B C \in ℝ$
52	50 51	readdcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A D + B C \in ℝ$
53		absreimsq	$⊢ (A C - B D \in ℝ \land A D + B C \in ℝ) \to {\|A C - B D + i (A D + B C)\|}^{2} = {(A C - B D)}^{2} + {(A D + B C)}^{2}$
54	49 52 53	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to {\|A C - B D + i (A D + B C)\|}^{2} = {(A C - B D)}^{2} + {(A D + B C)}^{2}$
55	35 46 54	3eqtr3d	$⊢ ((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 bhmafibid1

Proof