Metamath Proof Explorer

Theorem rediv

Description: Real part of a division. Related to remul2 . (Contributed by David A. Wheeler, 10-Jun-2015)

Ref Expression
Assertion rediv ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℜ ⁡ A B = ℜ ⁡ A B

Proof

Step Hyp Ref Expression
1 ancom ⊢ B ∈ ℝ ∧ B ≠ 0 ∧ A ∈ ℂ ↔ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0
2 3anass ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 ↔ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0
3 1 2 bitr4i ⊢ B ∈ ℝ ∧ B ≠ 0 ∧ A ∈ ℂ ↔ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0
4 rereccl ⊢ B ∈ ℝ ∧ B ≠ 0 → 1 B ∈ ℝ
5 4 anim1i ⊢ B ∈ ℝ ∧ B ≠ 0 ∧ A ∈ ℂ → 1 B ∈ ℝ ∧ A ∈ ℂ
6 3 5 sylbir ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → 1 B ∈ ℝ ∧ A ∈ ℂ
7 remul2 ⊢ 1 B ∈ ℝ ∧ A ∈ ℂ → ℜ ⁡ 1 B ⁢ A = 1 B ⁢ ℜ ⁡ A
8 6 7 syl ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℜ ⁡ 1 B ⁢ A = 1 B ⁢ ℜ ⁡ A
9 recn ⊢ B ∈ ℝ → B ∈ ℂ
10 divrec2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 B ⁢ A
11 10 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → ℜ ⁡ A B = ℜ ⁡ 1 B ⁢ A
12 9 11 syl3an2 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℜ ⁡ A B = ℜ ⁡ 1 B ⁢ A
13 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
14 13 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
15 14 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℜ ⁡ A ∈ ℂ
16 9 3ad2ant2 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → B ∈ ℂ
17 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → B ≠ 0
18 15 16 17 divrec2d ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℜ ⁡ A B = 1 B ⁢ ℜ ⁡ A
19 8 12 18 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℝ ∧ B ≠ 0 → ℜ ⁡ A B = ℜ ⁡ A B