Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem divadddivt 5740

Description: Addition of two ratios. Theorem I.13 of [Apostol] p. 18.

Assertion

Ref	Expression
divadddivt

---

Proof of Theorem divadddivt

Step	Hyp	Ref	Expression
1		muln0bt 5666	. . . . 5
2	1	ad2ant2l 408	. . . 4
3		divdirt 5713	. . . . . 6
4	3	ex 373	. . . . 5
5		axmulcl 5245	. . . . . 6
6	5	ad2ant2rl 411	. . . . 5
7		axmulcl 5245	. . . . . 6
8	7	ad2ant2lr 410	. . . . 5
9		axmulcl 5245	. . . . . 6
10	9	ad2ant2l 408	. . . . 5
11	4, 6, 8, 10	syl3anc 856	. . . 4
12	2, 11	sylbid 203	. . 3
13	12	imp 350	. 2
14		dividt 5722	. . . . . . 7
15	14	ad2ant2l 408	. . . . . 6
16	15	adantll 392	. . . . 5
17	16	opreq2d 3961	. . . 4
18		divmuldivt 5736	. . . . 5
19		pm3.27 323	. . . . . 6
20	19, 19	jca 288	. . . . 5
21	18, 20	sylanl2 461	. . . 4
22		divclt 5681	. . . . . . 7
23	22	3expa 831	. . . . . 6
24		ax1id 5254	. . . . . 6
25	23, 24	syl 10	. . . . 5
26	25	ad2ant2r 409	. . . 4
27	17, 21, 26	3eqtr3d 1507	. . 3
28		dividt 5722	. . . . . . 7
29	28	ad2ant2lr 410	. . . . . 6
30	29	adantlr 393	. . . . 5
31	30	opreq1d 3960	. . . 4
32		divmuldivt 5736	. . . . 5
33		pm3.27 323	. . . . . 6
34	33, 33	jca 288	. . . . 5
35	32, 34	sylanl1 460	. . . 4
36		divclt 5681	. . . . . . 7
37	36	3expa 831	. . . . . 6
38		mulid2t 5389	. . . . . 6
39	37, 38	syl 10	. . . . 5
40	39	ad2ant2l 408	. . . 4
41	31, 35, 40	3eqtr3d 1507	. . 3
42	27, 41	opreq12d 3963	. 2
43	13, 42	eqtr2d 1500	1

Colors of variables: wff set class

Syntax hints:   wi 3   wb 146   wa 223   w3a 773   wceq 953   wcel 955   wne 1577  (class class class)co 3948  cc 5204  cc0 5206  c1 5207   caddc 5209   cmul 5211   cdiv 5266

This theorem is referenced by:  divadddiv 5744  qaddclt 6207

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580