Metamath Proof Explorer


Theorem ltsubrpd

Description: Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpgecld.1 φA
rpgecld.2 φB+
Assertion ltsubrpd φAB<A

Proof

Step Hyp Ref Expression
1 rpgecld.1 φA
2 rpgecld.2 φB+
3 ltsubrp AB+AB<A
4 1 2 3 syl2anc φAB<A