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	⊢ ( 𝐶 ∈ P → ( ( 𝐴 +P 𝐵 ) = 𝐶 → 𝐴 <P 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( ( 𝐴 +P 𝐵 ) = 𝐶 → ( ( 𝐴 +P 𝐵 ) ∈ P ↔ 𝐶 ∈ P ) )
2		dmplp	⊢ dom +P = ( P × P )
3		0npr	⊢ ¬ ∅ ∈ P
4	2 3	ndmovrcl	⊢ ( ( 𝐴 +P 𝐵 ) ∈ P → ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) )
5	1 4	biimtrrdi	⊢ ( ( 𝐴 +P 𝐵 ) = 𝐶 → ( 𝐶 ∈ P → ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ) )
6		ltaddpr	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → 𝐴 <P ( 𝐴 +P 𝐵 ) )
7		breq2	⊢ ( ( 𝐴 +P 𝐵 ) = 𝐶 → ( 𝐴 <P ( 𝐴 +P 𝐵 ) ↔ 𝐴 <P 𝐶 ) )
8	6 7	imbitrid	⊢ ( ( 𝐴 +P 𝐵 ) = 𝐶 → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → 𝐴 <P 𝐶 ) )
9	5 8	syldc	⊢ ( 𝐶 ∈ P → ( ( 𝐴 +P 𝐵 ) = 𝐶 → 𝐴 <P 𝐶 ) )