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\in 𝑷\to \left(A{+}_{𝑷}B=C\to A{<}_{𝑷}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢A{+}_{𝑷}B=C\to \left(A{+}_{𝑷}B\in 𝑷\leftrightarrow C\in 𝑷\right)$$
2		dmplp	$$⊢\mathrm{dom}{+}_{𝑷}=𝑷\times 𝑷$$
3		0npr	$$⊢\neg \varnothing \in 𝑷$$
4	2 3	ndmovrcl	$$⊢A{+}_{𝑷}B\in 𝑷\to \left(A\in 𝑷\wedge B\in 𝑷\right)$$
5	1 4	biimtrrdi	$$⊢A{+}_{𝑷}B=C\to \left(C\in 𝑷\to \left(A\in 𝑷\wedge B\in 𝑷\right)\right)$$
6		ltaddpr	$$⊢\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{<}_{𝑷}\left(A{+}_{𝑷}B\right)$$
7		breq2	$$⊢A{+}_{𝑷}B=C\to \left(A{<}_{𝑷}\left(A{+}_{𝑷}B\right)\leftrightarrow A{<}_{𝑷}C\right)$$
8	6 7	imbitrid	$$⊢A{+}_{𝑷}B=C\to \left(\left(A\in 𝑷\wedge B\in 𝑷\right)\to A{<}_{𝑷}C\right)$$
9	5 8	syldc	$$⊢C\in 𝑷\to \left(A{+}_{𝑷}B=C\to A{<}_{𝑷}C\right)$$