# Metamath Proof Explorer

## Theorem cjdiv

Description: Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion cjdiv ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \stackrel{‾}{\frac{{A}}{{B}}}=\frac{\stackrel{‾}{{A}}}{\stackrel{‾}{{B}}}$

### Proof

Step Hyp Ref Expression
1 divcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{A}}{{B}}\in ℂ$
2 cjcl ${⊢}\frac{{A}}{{B}}\in ℂ\to \stackrel{‾}{\frac{{A}}{{B}}}\in ℂ$
3 1 2 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \stackrel{‾}{\frac{{A}}{{B}}}\in ℂ$
4 simp2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}\in ℂ$
5 cjcl ${⊢}{B}\in ℂ\to \stackrel{‾}{{B}}\in ℂ$
6 4 5 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \stackrel{‾}{{B}}\in ℂ$
7 simp3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}\ne 0$
8 cjne0 ${⊢}{B}\in ℂ\to \left({B}\ne 0↔\stackrel{‾}{{B}}\ne 0\right)$
9 4 8 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left({B}\ne 0↔\stackrel{‾}{{B}}\ne 0\right)$
10 7 9 mpbid ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \stackrel{‾}{{B}}\ne 0$
11 3 6 10 divcan4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{\stackrel{‾}{\frac{{A}}{{B}}}\stackrel{‾}{{B}}}{\stackrel{‾}{{B}}}=\stackrel{‾}{\frac{{A}}{{B}}}$
12 cjmul ${⊢}\left(\frac{{A}}{{B}}\in ℂ\wedge {B}\in ℂ\right)\to \stackrel{‾}{\left(\frac{{A}}{{B}}\right){B}}=\stackrel{‾}{\frac{{A}}{{B}}}\stackrel{‾}{{B}}$
13 1 4 12 syl2anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \stackrel{‾}{\left(\frac{{A}}{{B}}\right){B}}=\stackrel{‾}{\frac{{A}}{{B}}}\stackrel{‾}{{B}}$
14 divcan1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left(\frac{{A}}{{B}}\right){B}={A}$
15 14 fveq2d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \stackrel{‾}{\left(\frac{{A}}{{B}}\right){B}}=\stackrel{‾}{{A}}$
16 13 15 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \stackrel{‾}{\frac{{A}}{{B}}}\stackrel{‾}{{B}}=\stackrel{‾}{{A}}$
17 16 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{\stackrel{‾}{\frac{{A}}{{B}}}\stackrel{‾}{{B}}}{\stackrel{‾}{{B}}}=\frac{\stackrel{‾}{{A}}}{\stackrel{‾}{{B}}}$
18 11 17 eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \stackrel{‾}{\frac{{A}}{{B}}}=\frac{\stackrel{‾}{{A}}}{\stackrel{‾}{{B}}}$