Theorem divadddivt 5750

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 5676	. . . . 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 5723	. . . . . 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 5256	. . . . . 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 5256	. . . . . 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 5256	. . . . . 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 857	. . . 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 5732	. . . . . . 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 3971	. . . 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 5746	. . . . 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 5691	. . . . . . 7 |- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) e. CC)
23	22	3expa 832	. . . . . 6 |- (((A e. CC /\ B e. CC) /\ B =/= 0) -> (A / B) e. CC)
24		ax1id 5265	. . . . . 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 1513	. . 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 5732	. . . . . . 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 3970	. . . 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 5746	. . . . 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 5691	. . . . . . 7 |- ((C e. CC /\ D e. CC /\ D =/= 0) -> (C / D) e. CC)
37	36	3expa 832	. . . . . 6 |- (((C e. CC /\ D e. CC) /\ D =/= 0) -> (C / D) e. CC)
38		mulid2t 5400	. . . . . 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 1513	. . 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 3973	. 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 1506	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 774   = wceq 955   e. wcel 957   =/= wne 1583  (class class class)co 3958  CCcc 5215  0cc0 5217  1c1 5218   + caddc 5220   x. cmul 5222   / cdiv 5277

This theorem is referenced by:  divadddiv 5754  qaddclt 6219

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862  ax-inf2 4608

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-nel 1586  df-ral&n