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 A0
subreci.4 B0
Assertion subreci 1A1B=BAAB

Proof

Step Hyp Ref Expression
1 subreci.1 A
2 subreci.2 B
3 subreci.3 A0
4 subreci.4 B0
5 subrec AA0BB01A1B=BAAB
6 1 3 2 4 5 mp4an 1A1B=BAAB