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 e. P. -> ( ( A +P. B ) = C -> A

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( ( A +P. B ) = C -> ( ( A +P. B ) e. P. <-> C e. P. ) )
2		dmplp	|- dom +P. = ( P. X. P. )
3		0npr	|- -. (/) e. P.
4	2 3	ndmovrcl	|- ( ( A +P. B ) e. P. -> ( A e. P. /\ B e. P. ) )
5	1 4	biimtrrdi	|- ( ( A +P. B ) = C -> ( C e. P. -> ( A e. P. /\ B e. P. ) ) )
6		ltaddpr	|- ( ( A e. P. /\ B e. P. ) -> A
7		breq2	|- ( ( A +P. B ) = C -> ( A A
8	6 7	imbitrid	|- ( ( A +P. B ) = C -> ( ( A e. P. /\ B e. P. ) -> A
9	5 8	syldc	|- ( C e. P. -> ( ( A +P. B ) = C -> A