Metamath Proof Explorer

Theorem divdiv1

Description: Division into a fraction. (Contributed by NM, 31-Dec-2007)

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

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 ax-1ne0 ⊢ 1 ≠ 0
3 1 2 pm3.2i ⊢ 1 ∈ ℂ ∧ 1 ≠ 0
4 divdivdiv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 ∧ 1 ∈ ℂ ∧ 1 ≠ 0 → A B C 1 = A ⋅ 1 B ⁢ C
5 3 4 mpanr2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C 1 = A ⋅ 1 B ⁢ C
6 5 3impa ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C 1 = A ⋅ 1 B ⁢ C
7 div1 ⊢ C ∈ ℂ → C 1 = C
8 7 oveq2d ⊢ C ∈ ℂ → A B C 1 = A B C
9 8 ad2antrl ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C 1 = A B C
10 9 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C 1 = A B C
11 mulid1 ⊢ A ∈ ℂ → A ⋅ 1 = A
12 11 oveq1d ⊢ A ∈ ℂ → A ⋅ 1 B ⁢ C = A B ⁢ C
13 12 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A ⋅ 1 B ⁢ C = A B ⁢ C
14 6 10 13 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A B C = A B ⁢ C