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