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

Metamath Proof Explorer

Theorem divdivdivi

Description: Division of two ratios. Theorem I.15 of Apostol p. 18. (Contributed by NM, 22-Feb-1995)

Ref Expression
Hypotheses divclz.1 ⊢ A ∈ ℂ
divclz.2 ⊢ B ∈ ℂ
divmulz.3 ⊢ C ∈ ℂ
divmuldiv.4 ⊢ D ∈ ℂ
divmuldiv.5 ⊢ B ≠ 0
divmuldiv.6 ⊢ D ≠ 0
divdivdiv.7 ⊢ C ≠ 0
Assertion divdivdivi ⊢ A B C D = A ⁢ D B ⁢ C

Proof

Step Hyp Ref Expression
1 divclz.1 ⊢ A ∈ ℂ
2 divclz.2 ⊢ B ∈ ℂ
3 divmulz.3 ⊢ C ∈ ℂ
4 divmuldiv.4 ⊢ D ∈ ℂ
5 divmuldiv.5 ⊢ B ≠ 0
6 divmuldiv.6 ⊢ D ≠ 0
7 divdivdiv.7 ⊢ C ≠ 0
8 2 5 pm3.2i ⊢ B ∈ ℂ ∧ B ≠ 0
9 3 7 pm3.2i ⊢ C ∈ ℂ ∧ C ≠ 0
10 4 6 pm3.2i ⊢ D ∈ ℂ ∧ D ≠ 0
11 divdivdiv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A B C D = A ⁢ D B ⁢ C
12 1 8 9 10 11 mp4an ⊢ A B C D = A ⁢ D B ⁢ C