Metamath Proof Explorer


Theorem subrecd

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

Ref Expression
Hypotheses subrecd.1 φA
subrecd.2 φB
subrecd.3 φA0
subrecd.4 φB0
Assertion subrecd φ1A1B=BAAB

Proof

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