# 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 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}{B}\right|=\left|{A}\right|\left|{B}\right|$

### Proof

Step Hyp Ref Expression
1 cjmul ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \stackrel{‾}{{A}{B}}=\stackrel{‾}{{A}}\stackrel{‾}{{B}}$
2 1 oveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{B}\stackrel{‾}{{A}{B}}={A}{B}\stackrel{‾}{{A}}\stackrel{‾}{{B}}$
3 simpl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}\in ℂ$
4 simpr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {B}\in ℂ$
5 3 cjcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \stackrel{‾}{{A}}\in ℂ$
6 4 cjcld ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \stackrel{‾}{{B}}\in ℂ$
7 3 4 5 6 mul4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{B}\stackrel{‾}{{A}}\stackrel{‾}{{B}}={A}\stackrel{‾}{{A}}{B}\stackrel{‾}{{B}}$
8 2 7 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{B}\stackrel{‾}{{A}{B}}={A}\stackrel{‾}{{A}}{B}\stackrel{‾}{{B}}$
9 8 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \sqrt{{A}{B}\stackrel{‾}{{A}{B}}}=\sqrt{{A}\stackrel{‾}{{A}}{B}\stackrel{‾}{{B}}}$
10 cjmulrcl ${⊢}{A}\in ℂ\to {A}\stackrel{‾}{{A}}\in ℝ$
11 cjmulge0 ${⊢}{A}\in ℂ\to 0\le {A}\stackrel{‾}{{A}}$
12 10 11 jca ${⊢}{A}\in ℂ\to \left({A}\stackrel{‾}{{A}}\in ℝ\wedge 0\le {A}\stackrel{‾}{{A}}\right)$
13 cjmulrcl ${⊢}{B}\in ℂ\to {B}\stackrel{‾}{{B}}\in ℝ$
14 cjmulge0 ${⊢}{B}\in ℂ\to 0\le {B}\stackrel{‾}{{B}}$
15 13 14 jca ${⊢}{B}\in ℂ\to \left({B}\stackrel{‾}{{B}}\in ℝ\wedge 0\le {B}\stackrel{‾}{{B}}\right)$
16 sqrtmul ${⊢}\left(\left({A}\stackrel{‾}{{A}}\in ℝ\wedge 0\le {A}\stackrel{‾}{{A}}\right)\wedge \left({B}\stackrel{‾}{{B}}\in ℝ\wedge 0\le {B}\stackrel{‾}{{B}}\right)\right)\to \sqrt{{A}\stackrel{‾}{{A}}{B}\stackrel{‾}{{B}}}=\sqrt{{A}\stackrel{‾}{{A}}}\sqrt{{B}\stackrel{‾}{{B}}}$
17 12 15 16 syl2an ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \sqrt{{A}\stackrel{‾}{{A}}{B}\stackrel{‾}{{B}}}=\sqrt{{A}\stackrel{‾}{{A}}}\sqrt{{B}\stackrel{‾}{{B}}}$
18 9 17 eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \sqrt{{A}{B}\stackrel{‾}{{A}{B}}}=\sqrt{{A}\stackrel{‾}{{A}}}\sqrt{{B}\stackrel{‾}{{B}}}$
19 mulcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{B}\in ℂ$
20 absval ${⊢}{A}{B}\in ℂ\to \left|{A}{B}\right|=\sqrt{{A}{B}\stackrel{‾}{{A}{B}}}$
21 19 20 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}{B}\right|=\sqrt{{A}{B}\stackrel{‾}{{A}{B}}}$
22 absval ${⊢}{A}\in ℂ\to \left|{A}\right|=\sqrt{{A}\stackrel{‾}{{A}}}$
23 absval ${⊢}{B}\in ℂ\to \left|{B}\right|=\sqrt{{B}\stackrel{‾}{{B}}}$
24 22 23 oveqan12d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}\right|\left|{B}\right|=\sqrt{{A}\stackrel{‾}{{A}}}\sqrt{{B}\stackrel{‾}{{B}}}$
25 18 21 24 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}{B}\right|=\left|{A}\right|\left|{B}\right|$