Metamath Proof Explorer


Theorem divdiv32

Description: Swap denominators in a division. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion divdiv32 ABB0CC0ABC=ACB

Proof

Step Hyp Ref Expression
1 reccl BB01B
2 div23 A1BCC0A1BC=AC1B
3 1 2 syl3an2 ABB0CC0A1BC=AC1B
4 divrec ABB0AB=A1B
5 4 3expb ABB0AB=A1B
6 5 3adant3 ABB0CC0AB=A1B
7 6 oveq1d ABB0CC0ABC=A1BC
8 divcl ACC0AC
9 8 3expb ACC0AC
10 divrec ACBB0ACB=AC1B
11 9 10 syl3an1 ACC0BB0ACB=AC1B
12 11 3expb ACC0BB0ACB=AC1B
13 12 3impa ACC0BB0ACB=AC1B
14 13 3com23 ABB0CC0ACB=AC1B
15 3 7 14 3eqtr4d ABB0CC0ABC=ACB