Metamath Proof Explorer


Theorem divmuleq

Description: Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion divmuleq ABCC0DD0AC=BDAD=BC

Proof

Step Hyp Ref Expression
1 divcl ACC0AC
2 1 3expb ACC0AC
3 2 ad2ant2r ABCC0DD0AC
4 divcl BDD0BD
5 4 3expb BDD0BD
6 5 ad2ant2l ABCC0DD0BD
7 mulcl CDCD
8 7 ad2ant2r CC0DD0CD
9 mulne0 CC0DD0CD0
10 8 9 jca CC0DD0CDCD0
11 10 adantl ABCC0DD0CDCD0
12 mulcan2 ACBDCDCD0ACCD=BDCDAC=BD
13 3 6 11 12 syl3anc ABCC0DD0ACCD=BDCDAC=BD
14 simprll ABCC0DD0C
15 simprrl ABCC0DD0D
16 3 14 15 mulassd ABCC0DD0ACCD=ACCD
17 divcan1 ACC0ACC=A
18 17 3expb ACC0ACC=A
19 18 ad2ant2r ABCC0DD0ACC=A
20 19 oveq1d ABCC0DD0ACCD=AD
21 16 20 eqtr3d ABCC0DD0ACCD=AD
22 14 15 mulcomd ABCC0DD0CD=DC
23 22 oveq2d ABCC0DD0BDCD=BDDC
24 6 15 14 mulassd ABCC0DD0BDDC=BDDC
25 divcan1 BDD0BDD=B
26 25 3expb BDD0BDD=B
27 26 ad2ant2l ABCC0DD0BDD=B
28 27 oveq1d ABCC0DD0BDDC=BC
29 23 24 28 3eqtr2d ABCC0DD0BDCD=BC
30 21 29 eqeq12d ABCC0DD0ACCD=BDCDAD=BC
31 13 30 bitr3d ABCC0DD0AC=BDAD=BC