Metamath Proof Explorer

Theorem divdiv32

Description: Swap denominators in a division. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion divdiv32 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C = A C B

Proof

Step Hyp Ref Expression
1 reccl ⊢ B ∈ ℂ ∧ B ≠ 0 → 1 B ∈ ℂ
2 div23 ⊢ A ∈ ℂ ∧ 1 B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ 1 B C = A C ⁢ 1 B
3 1 2 syl3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ 1 B C = A C ⁢ 1 B
4 divrec ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B
5 4 3expb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B
6 5 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B = A ⁢ 1 B
7 6 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C = A ⁢ 1 B C
8 divcl ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
9 8 3expb ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
10 divrec ⊢ A C ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A C B = A C ⁢ 1 B
11 9 10 syl3an1 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A C B = A C ⁢ 1 B
12 11 3expb ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A C B = A C ⁢ 1 B
13 12 3impa ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A C B = A C ⁢ 1 B
14 13 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A C B = A C ⁢ 1 B
15 3 7 14 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C = A C B