Metamath Proof Explorer

Theorem addlelt

Description: If the sum of a real number and a positive real number is less than or equal to a third real number, the first real number is less than the third real number. (Contributed by AV, 1-Jul-2021)

		Ref	Expression
	Assertion	addlelt	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to (M + A \leq N \to M < N)$

Proof

Step	Hyp	Ref	Expression
1		rpgt0	$⊢ A \in ℝ^{+} \to 0 < A$
2	1	3ad2ant3	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to 0 < A$
3		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
4	3	3ad2ant3	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to A \in ℝ$
5		simp1	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to M \in ℝ$
6	4 5	ltaddposd	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to (0 < A \leftrightarrow M < M + A)$
7	2 6	mpbid	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to M < M + A$
8		simpl	$⊢ (M \in ℝ \land A \in ℝ^{+}) \to M \in ℝ$
9	3	adantl	$⊢ (M \in ℝ \land A \in ℝ^{+}) \to A \in ℝ$
10	8 9	readdcld	$⊢ (M \in ℝ \land A \in ℝ^{+}) \to M + A \in ℝ$
11	10	3adant2	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to M + A \in ℝ$
12		simp2	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to N \in ℝ$
13		ltletr	$⊢ (M \in ℝ \land M + A \in ℝ \land N \in ℝ) \to ((M < M + A \land M + A \leq N) \to M < N)$
14	5 11 12 13	syl3anc	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to ((M < M + A \land M + A \leq N) \to M < N)$
15	7 14	mpand	$⊢ (M \in ℝ \land N \in ℝ \land A \in ℝ^{+}) \to (M + A \leq N \to M < N)$