Metamath Proof Explorer

Theorem 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 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
Assertion mul2sq ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 1 2sqlem1 ⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) )
3 1 2sqlem1 ⊢ ( 𝐵 ∈ 𝑆 ↔ ∃ 𝑦 ∈ ℤ[i] 𝐵 = ( ( abs ‘ 𝑦 ) ↑ 2 ) )
4 reeanv ⊢ ( ∃ 𝑥 ∈ ℤ[i] ∃ 𝑦 ∈ ℤ[i] ( 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) ∧ 𝐵 = ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ↔ ( ∃ 𝑥 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) ∧ ∃ 𝑦 ∈ ℤ[i] 𝐵 = ( ( abs ‘ 𝑦 ) ↑ 2 ) ) )
5 gzmulcl ⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( 𝑥 · 𝑦 ) ∈ ℤ[i] )
6 gzcn ⊢ ( 𝑥 ∈ ℤ[i] → 𝑥 ∈ ℂ )
7 gzcn ⊢ ( 𝑦 ∈ ℤ[i] → 𝑦 ∈ ℂ )
8 absmul ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 · 𝑦 ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) )
9 6 7 8 syl2an ⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( abs ‘ ( 𝑥 · 𝑦 ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) )
10 9 oveq1d ⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( ( abs ‘ ( 𝑥 · 𝑦 ) ) ↑ 2 ) = ( ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) ↑ 2 ) )
11 6 abscld ⊢ ( 𝑥 ∈ ℤ[i] → ( abs ‘ 𝑥 ) ∈ ℝ )
12 11 recnd ⊢ ( 𝑥 ∈ ℤ[i] → ( abs ‘ 𝑥 ) ∈ ℂ )
13 7 abscld ⊢ ( 𝑦 ∈ ℤ[i] → ( abs ‘ 𝑦 ) ∈ ℝ )
14 13 recnd ⊢ ( 𝑦 ∈ ℤ[i] → ( abs ‘ 𝑦 ) ∈ ℂ )
15 sqmul ⊢ ( ( ( abs ‘ 𝑥 ) ∈ ℂ ∧ ( abs ‘ 𝑦 ) ∈ ℂ ) → ( ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) ↑ 2 ) = ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) )
16 12 14 15 syl2an ⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) ↑ 2 ) = ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) )
17 10 16 eqtr2d ⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) = ( ( abs ‘ ( 𝑥 · 𝑦 ) ) ↑ 2 ) )
18 fveq2 ⊢ ( 𝑧 = ( 𝑥 · 𝑦 ) → ( abs ‘ 𝑧 ) = ( abs ‘ ( 𝑥 · 𝑦 ) ) )
19 18 oveq1d ⊢ ( 𝑧 = ( 𝑥 · 𝑦 ) → ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( abs ‘ ( 𝑥 · 𝑦 ) ) ↑ 2 ) )
20 19 rspceeqv ⊢ ( ( ( 𝑥 · 𝑦 ) ∈ ℤ[i] ∧ ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) = ( ( abs ‘ ( 𝑥 · 𝑦 ) ) ↑ 2 ) ) → ∃ 𝑧 ∈ ℤ[i] ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
21 5 17 20 syl2anc ⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ∃ 𝑧 ∈ ℤ[i] ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
22 1 2sqlem1 ⊢ ( ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ∈ 𝑆 ↔ ∃ 𝑧 ∈ ℤ[i] ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
23 21 22 sylibr ⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ∈ 𝑆 )
24 oveq12 ⊢ ( ( 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) ∧ 𝐵 = ( ( abs ‘ 𝑦 ) ↑ 2 ) ) → ( 𝐴 · 𝐵 ) = ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) )
25 24 eleq1d ⊢ ( ( 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) ∧ 𝐵 = ( ( abs ‘ 𝑦 ) ↑ 2 ) ) → ( ( 𝐴 · 𝐵 ) ∈ 𝑆 ↔ ( ( ( abs ‘ 𝑥 ) ↑ 2 ) · ( ( abs ‘ 𝑦 ) ↑ 2 ) ) ∈ 𝑆 ) )
26 23 25 syl5ibrcom ⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( ( 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) ∧ 𝐵 = ( ( abs ‘ 𝑦 ) ↑ 2 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 ) )
27 26 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℤ[i] ∃ 𝑦 ∈ ℤ[i] ( 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) ∧ 𝐵 = ( ( abs ‘ 𝑦 ) ↑ 2 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 )
28 4 27 sylbir ⊢ ( ( ∃ 𝑥 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑥 ) ↑ 2 ) ∧ ∃ 𝑦 ∈ ℤ[i] 𝐵 = ( ( abs ‘ 𝑦 ) ↑ 2 ) ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 )
29 2 3 28 syl2anb ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 · 𝐵 ) ∈ 𝑆 )