Theorem divadddivt 4264

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 4213	. . . . . 6 |- ((B e. CC /\ D e. CC) -> ((B =/= 0 /\ D =/= 0) <-> (B x. D) =/= 0))
2	1	adantrl 311	. . . . 5 |- ((B e. CC /\ (C e. CC /\ D e. CC)) -> ((B =/= 0 /\ D =/= 0) <-> (B x. D) =/= 0))
3	2	adantll 309	. . . 4 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((B =/= 0 /\ D =/= 0) <-> (B x. D) =/= 0))
4		divdistrt 4246	. . . . . 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))))
5	4	exp 291	. . . . 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)))))
6		axmulcl 4068	. . . . . . 7 |- ((A e. CC /\ D e. CC) -> (A x. D) e. CC)
7	6	adantrl 311	. . . . . 6 |- ((A e. CC /\ (C e. CC /\ D e. CC)) -> (A x. D) e. CC)
8	7	adantlr 310	. . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (A x. D) e. CC)
9		axmulcl 4068	. . . . . . 7 |- ((B e. CC /\ C e. CC) -> (B x. C) e. CC)
10	9	adantrr 312	. . . . . 6 |- ((B e. CC /\ (C e. CC /\ D e. CC)) -> (B x. C) e. CC)
11	10	adantll 309	. . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (B x. C) e. CC)
12		axmulcl 4068	. . . . . . 7 |- ((B e. CC /\ D e. CC) -> (B x. D) e. CC)
13	12	adantrl 311	. . . . . 6 |- ((B e. CC /\ (C e. CC /\ D e. CC)) -> (B x. D) e. CC)
14	13	adantll 309	. . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> (B x. D) e. CC)
15	5, 8, 11, 14	syl3anc 629	. . . 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)))))
16	3, 15	sylbid 178	. . 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)))))
17	16	imp 277	. 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))))
18		dividt 4256	. . . . . . . 8 |- ((D e. CC /\ D =/= 0) -> (D / D) = 1)
19	18	adantrl 311	. . . . . . 7 |- ((D e. CC /\ (B =/= 0 /\ D =/= 0)) -> (D / D) = 1)
20	19	adantll 309	. . . . . 6 |- (((C e. CC /\ D e. CC) /\ (B =/= 0 /\ D =/= 0)) -> (D / D) = 1)
21	20	adantll 309	. . . . 5 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (D / D) = 1)
22	21	opreq2d 3013	. . . 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))
23		divmuldivt 4263	. . . . 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)))
24		pm3.27 260	. . . . . 6 |- ((C e. CC /\ D e. CC) -> D e. CC)
25	24, 24	jca 236	. . . . 5 |- ((C e. CC /\ D e. CC) -> (D e. CC /\ D e. CC))
26	23, 25	sylan12 355	. . . 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)))
27		divclt 4223	. . . . . . 7 |- (((A e. CC /\ B e. CC) /\ B =/= 0) -> (A / B) e. CC)
28		ax1id 4077	. . . . . . 7 |- ((A / B) e. CC -> ((A / B) x. 1) = (A / B))
29	27, 28	syl 12	. . . . . 6 |- (((A e. CC /\ B e. CC) /\ B =/= 0) -> ((A / B) x. 1) = (A / B))
30	29	adantrr 312	. . . . 5 |- (((A e. CC /\ B e. CC) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) x. 1) = (A / B))
31	30	adantlr 310	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> ((A / B) x. 1) = (A / B))
32	22, 26, 31	3eqtr3d 1133	. . 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))
33		dividt 4256	. . . . . . . 8 |- ((B e. CC /\ B =/= 0) -> (B / B) = 1)
34	33	adantrr 312	. . . . . . 7 |- ((B e. CC /\ (B =/= 0 /\ D =/= 0)) -> (B / B) = 1)
35	34	adantll 309	. . . . . 6 |- (((A e. CC /\ B e. CC) /\ (B =/= 0 /\ D =/= 0)) -> (B / B) = 1)
36	35	adantlr 310	. . . . 5 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (B / B) = 1)
37	36	opreq1d 3012	. . . 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)))
38		divmuldivt 4263	. . . . 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)))
39		pm3.27 260	. . . . . . 7 |- ((A e. CC /\ B e. CC) -> B e. CC)
40	39, 39	jca 236	. . . . . 6 |- ((A e. CC /\ B e. CC) -> (B e. CC /\ B e. CC))
41	40	anim1i 269	. . . . 5 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((B e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)))
42	38, 41	sylan 343	. . . 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)))
43		divclt 4223	. . . . . . 7 |- (((C e. CC /\ D e. CC) /\ D =/= 0) -> (C / D) e. CC)
44		mulid2t 4175	. . . . . . 7 |- ((C / D) e. CC -> (1 x. (C / D)) = (C / D))
45	43, 44	syl 12	. . . . . 6 |- (((C e. CC /\ D e. CC) /\ D =/= 0) -> (1 x. (C / D)) = (C / D))
46	45	adantrl 311	. . . . 5 |- (((C e. CC /\ D e. CC) /\ (B =/= 0 /\ D =/= 0)) -> (1 x. (C / D)) = (C / D))
47	46	adantll 309	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (1 x. (C / D)) = (C / D))
48	37, 42, 47	3eqtr3d 1133	. . 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))
49	32, 48	opreq12d 3014	. 2 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ D =/= 0)) -> (((A x. D) / (B x. D))