Metamath Proof Explorer


Theorem divrec2

Description: Relationship between division and reciprocal. (Contributed by NM, 7-Feb-2006)

Ref Expression
Assertion divrec2 A B B 0 A B = 1 B A

Proof

Step Hyp Ref Expression
1 divrec A B B 0 A B = A 1 B
2 simp1 A B B 0 A
3 reccl B B 0 1 B
4 3 3adant1 A B B 0 1 B
5 2 4 mulcomd A B B 0 A 1 B = 1 B A
6 1 5 eqtrd A B B 0 A B = 1 B A