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→AC+BD=A⁢D+B⁢CC⁢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⁢CC⁢D=A⁢DC⁢D+B⁢CC⁢D
13 3 6 11 12 syl3anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→A⁢D+B⁢CC⁢D=A⁢DC⁢D+B⁢CC⁢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⁢DC⁢D=D⁢AD⁢C
21 simprl ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→C∈ℂ∧C≠0
22 divcan5 ⊢A∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→D⁢AD⁢C=AC
23 14 21 15 22 syl3anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→D⁢AD⁢C=AC
24 20 23 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→A⁢DC⁢D=AC
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⁢CC⁢D=C⁢BC⁢D
28 divcan5 ⊢B∈ℂ∧D∈ℂ∧D≠0∧C∈ℂ∧C≠0→C⁢BC⁢D=BD
29 25 15 21 28 syl3anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→C⁢BC⁢D=BD
30 27 29 eqtrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→B⁢CC⁢D=BD
31 24 30 oveq12d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→A⁢DC⁢D+B⁢CC⁢D=AC+BD
32 13 31 eqtr2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→AC+BD=A⁢D+B⁢CC⁢D