This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∗ ‘ ( 𝐴 / 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) / ( ∗ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 divcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
2 cjcl ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℂ → ( ∗ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
3 1 2 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∗ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
4 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
5 cjcl ⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) ∈ ℂ )
6 4 5 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∗ ‘ 𝐵 ) ∈ ℂ )
7 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → 𝐵 ≠ 0 )
8 cjne0 ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ≠ 0 ↔ ( ∗ ‘ 𝐵 ) ≠ 0 ) )
9 4 8 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐵 ≠ 0 ↔ ( ∗ ‘ 𝐵 ) ≠ 0 ) )
10 7 9 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∗ ‘ 𝐵 ) ≠ 0 )
11 3 6 10 divcan4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( ( ∗ ‘ ( 𝐴 / 𝐵 ) ) · ( ∗ ‘ 𝐵 ) ) / ( ∗ ‘ 𝐵 ) ) = ( ∗ ‘ ( 𝐴 / 𝐵 ) ) )
12 cjmul ⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∗ ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ( ∗ ‘ ( 𝐴 / 𝐵 ) ) · ( ∗ ‘ 𝐵 ) ) )
13 1 4 12 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∗ ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ( ∗ ‘ ( 𝐴 / 𝐵 ) ) · ( ∗ ‘ 𝐵 ) ) )
14 divcan1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) · 𝐵 ) = 𝐴 )
15 14 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∗ ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ∗ ‘ 𝐴 ) )
16 13 15 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( ∗ ‘ ( 𝐴 / 𝐵 ) ) · ( ∗ ‘ 𝐵 ) ) = ( ∗ ‘ 𝐴 ) )
17 16 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( ( ∗ ‘ ( 𝐴 / 𝐵 ) ) · ( ∗ ‘ 𝐵 ) ) / ( ∗ ‘ 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) / ( ∗ ‘ 𝐵 ) ) )
18 11 17 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∗ ‘ ( 𝐴 / 𝐵 ) ) = ( ( ∗ ‘ 𝐴 ) / ( ∗ ‘ 𝐵 ) ) )