Metamath Proof Explorer


Theorem ltaddpr2

Description: The sum of two positive reals is greater than one of them. (Contributed by NM, 13-May-1996) (New usage is discouraged.)

Ref Expression
Assertion ltaddpr2 C𝑷A+𝑷B=CA<𝑷C

Proof

Step Hyp Ref Expression
1 eleq1 A+𝑷B=CA+𝑷B𝑷C𝑷
2 dmplp dom+𝑷=𝑷×𝑷
3 0npr ¬𝑷
4 2 3 ndmovrcl A+𝑷B𝑷A𝑷B𝑷
5 1 4 syl6bir A+𝑷B=CC𝑷A𝑷B𝑷
6 ltaddpr A𝑷B𝑷A<𝑷A+𝑷B
7 breq2 A+𝑷B=CA<𝑷A+𝑷BA<𝑷C
8 6 7 syl5ib A+𝑷B=CA𝑷B𝑷A<𝑷C
9 5 8 syldc C𝑷A+𝑷B=CA<𝑷C