Metamath Proof Explorer

Theorem absmul

Description: Absolute value distributes over multiplication. Proposition 10-3.7(f) of Gleason p. 133. (Contributed by NM, 11-Oct-1999) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion absmul ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = A ⁢ B

Proof

Step Hyp Ref Expression
1 cjmul ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ‾ = A ‾ ⁢ B ‾
2 1 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ⁢ A ⁢ B ‾ = A ⁢ B ⁢ A ‾ ⁢ B ‾
3 simpl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ
4 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ
5 3 cjcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ‾ ∈ ℂ
6 4 cjcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ‾ ∈ ℂ
7 3 4 5 6 mul4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ⁢ A ‾ ⁢ B ‾ = A ⁢ A ‾ ⁢ B ⁢ B ‾
8 2 7 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ⁢ A ⁢ B ‾ = A ⁢ A ‾ ⁢ B ⁢ B ‾
9 8 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ⁢ A ⁢ B ‾ = A ⁢ A ‾ ⁢ B ⁢ B ‾
10 cjmulrcl ⊢ A ∈ ℂ → A ⁢ A ‾ ∈ ℝ
11 cjmulge0 ⊢ A ∈ ℂ → 0 ≤ A ⁢ A ‾
12 10 11 jca ⊢ A ∈ ℂ → A ⁢ A ‾ ∈ ℝ ∧ 0 ≤ A ⁢ A ‾
13 cjmulrcl ⊢ B ∈ ℂ → B ⁢ B ‾ ∈ ℝ
14 cjmulge0 ⊢ B ∈ ℂ → 0 ≤ B ⁢ B ‾
15 13 14 jca ⊢ B ∈ ℂ → B ⁢ B ‾ ∈ ℝ ∧ 0 ≤ B ⁢ B ‾
16 sqrtmul ⊢ A ⁢ A ‾ ∈ ℝ ∧ 0 ≤ A ⁢ A ‾ ∧ B ⁢ B ‾ ∈ ℝ ∧ 0 ≤ B ⁢ B ‾ → A ⁢ A ‾ ⁢ B ⁢ B ‾ = A ⁢ A ‾ ⁢ B ⁢ B ‾
17 12 15 16 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ A ‾ ⁢ B ⁢ B ‾ = A ⁢ A ‾ ⁢ B ⁢ B ‾
18 9 17 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ⁢ A ⁢ B ‾ = A ⁢ A ‾ ⁢ B ⁢ B ‾
19 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
20 absval ⊢ A ⁢ B ∈ ℂ → A ⁢ B = A ⁢ B ⁢ A ⁢ B ‾
21 19 20 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = A ⁢ B ⁢ A ⁢ B ‾
22 absval ⊢ A ∈ ℂ → A = A ⁢ A ‾
23 absval ⊢ B ∈ ℂ → B = B ⁢ B ‾
24 22 23 oveqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = A ⁢ A ‾ ⁢ B ⁢ B ‾
25 18 21 24 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = A ⁢ B