Theorem divadddivt 5691

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

Assertion

Ref	Expression
divadddivt	|- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) + (C / D)) = (((A x. D) + (B x. C)) / (B x. D)))

Proof of Theorem divadddivt

Step	Hyp	Ref	Expression
1		muln0bt 5617	. . . . 5 |- ((B e. CC /\ D e. CC) -> ((B =/= 0 /\ D =/= 0) <-> (B x. D) =/= 0))
2	1	ad2ant2l 408	. . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((B =/= 0 /\ D =/= 0) <-> (B x. D) =/= 0))
3		divdirt 5664	. . . . . 6 |- ((((A x. D) e. CC /\ (B x. C) e. CC /\ (B x. D) e. CC) /\ (B x. D) =/= 0) -> (((A x. D) + (B x. C)) / (B x. D)) = (((A x. D) / (B x. D)) + ((B x. C) / (B x. D))))
4	3	ex 373	. . . . 5 |- (((A x. D) e. CC /\ (B x. C) e. CC /\ (B x. D) e. CC) -> ((B x. D) =/= 0 -> (((A x. D) + (B x. C)) / (B x. D)) = (((A x. D) / (B x. D)) + ((B x. C) / (B x. D)))))
5		axmulcl 5196	. . . . . 6 |- ((A e. CC /\ D e. CC) -> (A x. D) e. CC)
6	5	ad2ant2rl 411	. . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (A x. D) e. CC)
7		axmulcl 5196	. . . . . 6 |- ((B e. CC /\ C e. CC) -> (B x. C) e. CC)
8	7	ad2ant2lr 410	. . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (B x. C) e. CC)
9		axmulcl 5196	. . . . . 6 |- ((B e. CC /\ D e. CC) -> (B x. D) e. CC)
10	9	ad2ant2l 408	. . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (B x. D) e. CC)
11	4, 6, 8, 10	syl3anc 855	. . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((B x. D) =/= 0 -> (((A x. D) + (B x. C)) / (B x. D)) = (((A x. D) / (B x. D)) + ((B x. C) / (B x. D)))))
12	2, 11	sylbid 203	. . 3 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((B =/= 0 /\ D =/= 0) -> (((A x. D) + (B x. C)) / (B x. D)) = (((A x. D) / (B x. D)) + ((B x. C) / (B x. D)))))
13	12	imp 350	. 2 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (((A x. D) + (B x. C)) / (B x. D)) = (((A x. D) / (B x. D)) + ((B x. C) / (B x. D))))
14		dividt 5673	. . . . . . 7 |- ((D e. CC /\ D =/= 0) -> (D / D) = 1)
15	14	ad2ant2l 408	. . . . . 6 |- (((C e. CC /\ D e. CC) /\ (B =/= 0 /\ D =/= 0)) -> (D / D) = 1)
16	15	adantll 392	. . . . 5 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (D / D) = 1)
17	16	opreq2d 3915	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) x. (D / D)) = ((A / B) x. 1))
18		divmuldivt 5687	. . . . 5 |- ((((A e. CC /\ B e. CC) /\ (D e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) x. (D / D)) = ((A x. D) / (B x. D)))
19		pm3.27 323	. . . . . 6 |- ((C e. CC /\ D e. CC) -> D e. CC)
20	19, 19	jca 288	. . . . 5 |- ((C e. CC /\ D e. CC) -> (D e. CC /\ D e. CC))
21	18, 20	sylanl2 461	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) x. (D / D)) = ((A x. D) / (B x. D)))
22		divclt 5632	. . . . . . 7 |- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) e. CC)
23	22	3expa 830	. . . . . 6 |- (((A e. CC /\ B e. CC) /\ B =/= 0) -> (A / B) e. CC)
24		ax1id 5205	. . . . . 6 |- ((A / B) e. CC -> ((A / B) x. 1) = (A / B))
25	23, 24	syl 10	. . . . 5 |- (((A e. CC /\ B e. CC) /\ B =/= 0) -> ((A / B) x. 1) = (A / B))
26	25	ad2ant2r 409	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) x. 1) = (A / B))
27	17, 21, 26	3eqtr3d 1491	. . 3 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A x. D) / (B x. D)) = (A / B))
28		dividt 5673	. . . . . . 7 |- ((B e. CC /\ B =/= 0) -> (B / B) = 1)
29	28	ad2ant2lr 410	. . . . . 6 |- (((A e. CC /\ B e. CC) /\ (B =/= 0 /\ D =/= 0)) -> (B / B) = 1)
30	29	adantlr 393	. . . . 5 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (B / B) = 1)
31	30	opreq1d 3914	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((B / B) x. (C / D)) = (1 x. (C / D)))
32		divmuldivt 5687	. . . . 5 |- ((((B e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((B / B) x. (C / D)) = ((B x. C) / (B x. D)))
33		pm3.27 323	. . . . . 6 |- ((A e. CC /\ B e. CC) -> B e. CC)
34	33, 33	jca 288	. . . . 5 |- ((A e. CC /\ B e. CC) -> (B e. CC /\ B e. CC))
35	32, 34	sylanl1 460	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((B / B) x. (C / D)) = ((B x. C) / (B x. D)))
36		divclt 5632	. . . . . . 7 |- ((C e. CC /\ D e. CC /\ D =/= 0) -> (C / D) e. CC)
37	36	3expa 830	. . . . . 6 |- (((C e. CC /\ D e. CC) /\ D =/= 0) -> (C / D) e. CC)
38		mulid2t 5340	. . . . . 6 |- ((C / D) e. CC -> (1 x. (C / D)) = (C / D))
39	37, 38	syl 10	. . . . 5 |- (((C e. CC /\ D e. CC) /\ D =/= 0) -> (1 x. (C / D)) = (C / D))
40	39	ad2ant2l 408	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (1 x. (C / D)) = (C / D))
41	31, 35, 40	3eqtr3d 1491	. . 3 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((B x. C) / (B x. D)) = (C / D))
42	27, 41	opreq12d 3917	. 2 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (((A x. D) / (B x. D)) + ((B x. C) / (B x. D))) = ((A / B) + (C / D)))
43	13, 42	eqtr2d 1484	1 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) + (C / D)) = (((A x. D) + (B x. C)) / (B x. D)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 772   = wceq 1099   e. wcel 1105   =/= wne 1561  (class class class)co 3902  CCcc 5155  0cc0 5157  1c1 5158   + caddc 5160   x. cmul 5162   / cdiv 5217

This theorem is referenced by:  divadddiv 5695  qaddclt 6158

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-nel 1564  df-ral 16