Metamath Proof Explorer

Theorem divadddiv

Description: Addition of two ratios. Theorem I.13 of Apostol p. 18. (Contributed by NM, 1-Aug-2004) (Revised by Mario Carneiro, 2-May-2016)

Ref Expression
Assertion divadddiv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C + B D = A ⁢ D + B ⁢ C C ⁢ D

Proof

Step Hyp Ref Expression
1 mulcl ⊢ A ∈ ℂ ∧ D ∈ ℂ → A ⁢ D ∈ ℂ
2 1 ad2ant2r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D ∈ ℂ
3 2 adantrl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D ∈ ℂ
4 mulcl ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C ∈ ℂ
5 4 adantrr ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ⁢ C ∈ ℂ
6 5 ad2ant2lr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B ⁢ C ∈ ℂ
7 mulcl ⊢ C ∈ ℂ ∧ D ∈ ℂ → C ⁢ D ∈ ℂ
8 7 ad2ant2r ⊢ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ⁢ D ∈ ℂ
9 mulne0 ⊢ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ⁢ D ≠ 0
10 8 9 jca ⊢ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ⁢ D ∈ ℂ ∧ C ⁢ D ≠ 0
11 10 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ⁢ D ∈ ℂ ∧ C ⁢ D ≠ 0
12 divdir ⊢ A ⁢ D ∈ ℂ ∧ B ⁢ C ∈ ℂ ∧ C ⁢ D ∈ ℂ ∧ C ⁢ D ≠ 0 → A ⁢ D + B ⁢ C C ⁢ D = A ⁢ D C ⁢ D + B ⁢ C C ⁢ D
13 3 6 11 12 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D + B ⁢ C C ⁢ D = A ⁢ D C ⁢ D + B ⁢ C C ⁢ D
14 simpll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ∈ ℂ
15 simprr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → D ∈ ℂ ∧ D ≠ 0
16 15 simpld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → D ∈ ℂ
17 14 16 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D = D ⁢ A
18 simprll ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ∈ ℂ
19 18 16 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ⁢ D = D ⁢ C
20 17 19 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D C ⁢ D = D ⁢ A D ⁢ C
21 simprl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ∈ ℂ ∧ C ≠ 0
22 divcan5 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → D ⁢ A D ⁢ C = A C
23 14 21 15 22 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → D ⁢ A D ⁢ C = A C
24 20 23 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D C ⁢ D = A C
25 simplr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B ∈ ℂ
26 25 18 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B ⁢ C = C ⁢ B
27 26 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B ⁢ C C ⁢ D = C ⁢ B C ⁢ D
28 divcan5 ⊢ B ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C ⁢ D = B D
29 25 15 21 28 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → C ⁢ B C ⁢ D = B D
30 27 29 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B ⁢ C C ⁢ D = B D
31 24 30 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ D C ⁢ D + B ⁢ C C ⁢ D = A C + B D
32 13 31 eqtr2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C + B D = A ⁢ D + B ⁢ C C ⁢ D