Theorem divdivdivt 5785

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 5276	. . . . . . 7 |- (((D / C) e. CC /\ (A / B) e. CC) -> ((D / C) x. (A / B)) = ((A / B) x. (D / C)))
2		divclt 5712	. . . . . . . . . . 11 |- ((D e. CC /\ C e. CC /\ C =/= 0) -> (D / C) e. CC)
3	2	3com12 837	. . . . . . . . . 10 |- ((C e. CC /\ D e. CC /\ C =/= 0) -> (D / C) e. CC)
4	3	3expa 833	. . . . . . . . 9 |- (((C e. CC /\ D e. CC) /\ C =/= 0) -> (D / C) e. CC)
5	4	adantrr 395	. . . . . . . 8 |- (((C e. CC /\ D e. CC) /\ (C =/= 0 /\ D =/= 0)) -> (D / C) e. CC)
6	5	ad2ant2l 408	. . . . . . 7 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (D / C) e. CC)
7		divclt 5712	. . . . . . . . 9 |- ((A e. CC /\ B e. CC /\ B =/= 0) -> (A / B) e. CC)
8	7	3expa 833	. . . . . . . 8 |- (((A e. CC /\ B e. CC) /\ B =/= 0) -> (A / B) e. CC)
9	8	ad2ant2r 409	. . . . . . 7 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (A / B) e. CC)
10	1, 6, 9	sylanc 471	. . . . . 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)))
11		divmuldivt 5780	. . . . . . 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)))
12		pm3.22 438	. . . . . . . 8 |- ((C e. CC /\ D e. CC) -> (D e. CC /\ C e. CC))
13	12	anim2i 335	. . . . . . 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)))
14		pm3.26 319	. . . . . . . 8 |- ((C =/= 0 /\ D =/= 0) -> C =/= 0)
15	14	anim2i 335	. . . . . . 7 |- ((B =/= 0 /\ (C =/= 0 /\ D =/= 0)) -> (B =/= 0 /\ C =/= 0))
16	11, 13, 15	syl2an 454	. . . . . 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)))
17	10, 16	eqtrd 1507	. . . . 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)))
18	17	opreq2d 3976	. . . 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))))
19	12	ancli 296	. . . . . . . . . 10 |- ((C e. CC /\ D e. CC) -> ((C e. CC /\ D e. CC) /\ (D e. CC /\ C e. CC)))
20		pm3.22 438	. . . . . . . . . . 11 |- ((C =/= 0 /\ D =/= 0) -> (D =/= 0 /\ C =/= 0))
21	20	adantl 388	. . . . . . . . . 10 |- ((B =/= 0 /\ (C =/= 0 /\ D =/= 0)) -> (D =/= 0 /\ C =/= 0))
22	19, 21	anim12i 333	. . . . . . . . 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)))
23	22	adantll 392	. . . . . . . 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)))
24		divmuldivt 5780	. . . . . . . 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)))
25	23, 24	syl 10	. . . . . . 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)))
26		axmulcom 5276	. . . . . . . . 9 |- ((C e. CC /\ D e. CC) -> (C x. D) = (D x. C))
27	26	ad2antlr 405	. . . . . . . 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))
28	27	opreq1d 3975	. . . . . . 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)))
29		dividt 5766	. . . . . . . 8 |- (((D x. C) e. CC /\ (D x. C) =/= 0) -> ((D x. C) / (D x. C)) = 1)
30		axmulcl 5273	. . . . . . . . . 10 |- ((D e. CC /\ C e. CC) -> (D x. C) e. CC)
31	30	ancoms 436	. . . . . . . . 9 |- ((C e. CC /\ D e. CC) -> (D x. C) e. CC)
32	31	ad2antlr 405	. . . . . . . 8 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (D x. C) e. CC)
33		muln0bt 5697	. . . . . . . . . . . 12 |- ((D e. CC /\ C e. CC) -> ((D =/= 0 /\ C =/= 0) <-> (D x. C) =/= 0))
34		ancom 435	. . . . . . . . . . . 12 |- ((C =/= 0 /\ D =/= 0) <-> (D =/= 0 /\ C =/= 0))
35	33, 34	syl5bb 532	. . . . . . . . . . 11 |- ((D e. CC /\ C e. CC) -> ((C =/= 0 /\ D =/= 0) <-> (D x. C) =/= 0))
36	35	ancoms 436	. . . . . . . . . 10 |- ((C e. CC /\ D e. CC) -> ((C =/= 0 /\ D =/= 0) <-> (D x. C) =/= 0))
37	36	biimpa 416	. . . . . . . . 9 |- (((C e. CC /\ D e. CC) /\ (C =/= 0 /\ D =/= 0)) -> (D x. C) =/= 0)
38	37	ad2ant2l 408	. . . . . . . 8 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (D x. C) =/= 0)
39	29, 32, 38	sylanc 471	. . . . . . 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)
40	25, 28, 39	3eqtrd 1511	. . . . . 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)
41	40	opreq1d 3975	. . . . 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)))
42		axmulass 5278	. . . . . 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))))
43		divclt 5712	. . . . . . . . 9 |- ((C e. CC /\ D e. CC /\ D =/= 0) -> (C / D) e. CC)
44	43	3expa 833	. . . . . . . 8 |- (((C e. CC /\ D e. CC) /\ D =/= 0) -> (C / D) e. CC)
45	44	adantrl 394	. . . . . . 7 |- (((C e. CC /\ D e. CC) /\ (C =/= 0 /\ D =/= 0)) -> (C / D) e. CC)
46	45	ad2ant2l 408	. . . . . 6 |- ((((A e. CC /\ B e. CC) /\ (C e. CC /\ D e. CC)) /\ (B =/= 0 /\ (C =/= 0 /\ D =/= 0))) -> (C / D) e. CC)
47	42, 46, 6, 9	syl3anc 858	. . . . 5 |-