Theorem divdivdivt 4265

Description: Division of two ratios. Theorem I.15 of [Apostol] p. 18.

Assertion

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

Proof of Theorem divdivdivt

Step	Hyp	Ref	Expression
1		axmulcom 4071	. . . . . . 7 |- (((D / C) e. CC /\ (A / B) e. CC) -> ((D / C) x. (A / B)) = ((A / B) x. (D / C)))
2		divclt 4223	. . . . . . . . . . 11 |- (((D e. CC /\ C e. CC) /\ C =/= 0) -> (D / C) e. CC)
3		ancom 333	. . . . . . . . . . 11 |- ((C e. CC /\ D e. CC) <-> (D e. CC /\ C e. CC))
4	2, 3	sylanb 344	. . . . . . . . . 10 |- (((C e. CC /\ D e. CC) /\ C =/= 0) -> (D / C) e. CC)
5	4	adantrr 312	. . . . . . . . 9 |- (((C e. CC /\ D e. CC) /\ (C =/= 0 /\ D =/= 0)) -> (D / C) e. CC)
6	5	adantrl 311	. . . . . . . 8 |- (((C e. CC /\ D e. CC) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (D / C) e. CC)
7	6	adantll 309	. . . . . . 7 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (D / C) e. CC)
8		divclt 4223	. . . . . . . . 9 |- (((A e. CC /\ B e. CC) /\ B =/= 0) -> (A / B) e. CC)
9	8	adantrr 312	. . . . . . . 8 |- (((A e. CC /\ B e. CC) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (A / B) e. CC)
10	9	adantlr 310	. . . . . . 7 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (A / B) e. CC)
11	1, 7, 10	sylanc 361	. . . . . 6 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> ((D / C) x. (A / B)) = ((A / B) x. (D / C)))
12		divmuldivt 4263	. . . . . . 7 |- ((((A e. CC /\ B e. CC) /\ (D e. CC /\ C e. CC)) /\ (B =/= 0 /\ C =/= 0)) -> ((A / B) x. (D / C)) = ((A x. D) / (B x. C)))
13	3	biimp 133	. . . . . . . 8 |- ((C e. CC /\ D e. CC) -> (D e. CC /\ C e. CC))
14	13	anim2i 270	. . . . . . 7 |- (((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) -> ((A e. CC /\ B e. CC) /\ (D e. CC /\ C e. CC)))
15		pm3.26 256	. . . . . . . 8 |- ((C =/= 0 /\ D =/= 0) -> C =/= 0)
16	15	anim2i 270	. . . . . . 7 |- ((B =/= 0 /\ (C =/= 0 /\ D =/= 0)) -> (B =/= 0 /\ C =/= 0))
17	12, 14, 16	syl2an 349	. . . . . 6 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> ((A / B) x. (D / C)) = ((A x. D) / (B x. C)))
18	11, 17	eqtrd 1128	. . . . 5 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> ((D / C) x. (A / B)) = ((A x. D) / (B x. C)))
19	18	opreq2d 3013	. . . 4 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> ((C / D) x. ((D / C) x. (A / B))) = ((C / D) x. ((A x. D) / (B x. C))))
20	13	ancli 244	. . . . . . . . . 10 |- ((C e. CC /\ D e. CC) -> ((C e. CC /\ D e. CC) /\ (D e. CC /\ C e. CC)))
21		ancom 333	. . . . . . . . . . . 12 |- ((C =/= 0 /\ D =/= 0) <-> (D =/= 0 /\ C =/= 0))
22	21	biimp 133	. . . . . . . . . . 11 |- ((C =/= 0 /\ D =/= 0) -> (D =/= 0 /\ C =/= 0))
23	22	adantl 305	. . . . . . . . . 10 |- ((B =/= 0 /\ (C =/= 0 /\ D =/= 0)) -> (D =/= 0 /\ C =/= 0))
24	20, 23	anim12i 268	. . . . . . . . 9 |- (((C e. CC /\ D e. CC) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (((C e. CC /\ D e. CC) /\ (D e. CC /\ C e. CC)) /\ (D =/= 0 /\ C =/= 0)))
25	24	adantll 309	. . . . . . . 8 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (((C e. CC /\ D e. CC) /\ (D e. CC /\ C e. CC)) /\ (D =/= 0 /\ C =/= 0)))
26		divmuldivt 4263	. . . . . . . 8 |- ((((C e. CC /\ D e. CC) /\ (D e. CC /\ C e. CC)) /\ (D =/= 0 /\ C =/= 0)) -> ((C / D) x. (D / C)) = ((C x. D) / (D x. C)))
27	25, 26	syl 12	. . . . . . 7 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> ((C / D) x. (D / C)) = ((C x. D) / (D x. C)))
28		axmulcom 4071	. . . . . . . . 9 |- ((C e. CC /\ D e. CC) -> (C x. D) = (D x. C))
29	28	ad2antlr 321	. . . . . . . 8 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (C x. D) = (D x. C))
30	29	opreq1d 3012	. . . . . . 7 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> ((C x. D) / (D x. C)) = ((D x. C) / (D x. C)))
31		dividt 4256	. . . . . . . 8 |- (((D x. C) e. CC /\ (D x. C) =/= 0) -> ((D x. C) / (D x. C)) = 1)
32		axmulcl 4068	. . . . . . . . . 10 |- ((D e. CC /\ C e. CC) -> (D x. C) e. CC)
33	32	ancoms 334	. . . . . . . . 9 |- ((C e. CC /\ D e. CC) -> (D x. C) e. CC)
34	33	ad2antlr 321	. . . . . . . 8 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (D x. C) e. CC)
35		muln0bt 4213	. . . . . . . . . . . . 13 |- ((D e. CC /\ C e. CC) -> ((D =/= 0 /\ C =/= 0) <-> (D x. C) =/= 0))
36	35, 21	syl5bb 410	. . . . . . . . . . . 12 |- ((D e. CC /\ C e. CC) -> ((C =/= 0 /\ D =/= 0) <-> (D x. C) =/= 0))
37	36	ancoms 334	. . . . . . . . . . 11 |- ((C e. CC /\ D e. CC) -> ((C =/= 0 /\ D =/= 0) <-> (D x. C) =/= 0))
38	37	biimpa 324	. . . . . . . . . 10 |- (((C e. CC /\ D e. CC) /\ (C =/= 0 /\ D =/= 0)) -> (D x. C) =/= 0)
39	38	adantrl 311	. . . . . . . . 9 |- (((C e. CC /\ D e. CC) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (D x. C) =/= 0)
40	39	adantll 309	. . . . . . . 8 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (D x. C) =/= 0)
41	31, 34, 40	sylanc 361	. . . . . . 7 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> ((D x. C) / (D x. C)) = 1)
42	27, 30, 41	3eqtrd 1132	. . . . . 6 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> ((C / D) x. (D / C)) = 1)
43	42	opreq1d 3012	. . . . 5 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (((C / D) x. (D / C)) x. (A / B)) = (1 x. (A / B)))
44		axmulass 4073	. . . . . 6 |- (((C / D) e. CC /\ (D / C) e. CC /\ (A / B) e. CC) -> (((C / D) x. (D / C)) x. (A / B)) = ((C / D) x. ((D / C) x. (A / B))))
45		divclt 4223	. . . . . . . . 9 |- (((C e. CC /\ D e. CC) /\ D =/= 0) -> (C / D) e. CC)
46	45	adantrl 311	. . . . . . . 8 |- (((C e. CC /\ D e. CC) /\ (C =/= 0 /\ D =/= 0)) -> (C / D) e. CC)
47	46	adantrl 311	. . . . . . 7 |- (((C e. CC /\ D e. CC) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (C / D) e.