This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
2 1 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
3 2 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
4 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℝ )
5 4 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
6 5 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐷 ↑ 2 ) ∈ ℂ )
7 3 6 addcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) = ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) )
8 7 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) ) )
9 bhmafibid1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) )
10 9 ancom2s ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) )
11 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
12 11 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℂ )
13 12 5 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
14 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
15 14 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
16 15 2 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
17 13 16 subcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ∈ ℂ )
18 17 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ∈ ℂ )
19 12 2 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
20 15 5 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
21 19 20 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ∈ ℂ )
22 21 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℂ )
23 18 22 addcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
24 8 10 23 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )