Metamath Proof Explorer


Theorem subreci

Description: Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017)

Ref Expression
Hypotheses subreci.1 A
subreci.2 B
subreci.3 A 0
subreci.4 B 0
Assertion subreci 1 A 1 B = B A A B

Proof

Step Hyp Ref Expression
1 subreci.1 A
2 subreci.2 B
3 subreci.3 A 0
4 subreci.4 B 0
5 subrec A A 0 B B 0 1 A 1 B = B A A B
6 1 3 2 4 5 mp4an 1 A 1 B = B A A B