Step |
Hyp |
Ref |
Expression |
1 |
|
rpgt0 |
⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 ) |
2 |
1
|
3ad2ant3 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 0 < 𝐴 ) |
3 |
|
rpre |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ ) |
4 |
3
|
3ad2ant3 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ ) |
5 |
|
simp1 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 𝑀 ∈ ℝ ) |
6 |
4 5
|
ltaddposd |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → ( 0 < 𝐴 ↔ 𝑀 < ( 𝑀 + 𝐴 ) ) ) |
7 |
2 6
|
mpbid |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 𝑀 < ( 𝑀 + 𝐴 ) ) |
8 |
|
simpl |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 𝑀 ∈ ℝ ) |
9 |
3
|
adantl |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ ) |
10 |
8 9
|
readdcld |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 + 𝐴 ) ∈ ℝ ) |
11 |
10
|
3adant2 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → ( 𝑀 + 𝐴 ) ∈ ℝ ) |
12 |
|
simp2 |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 𝑁 ∈ ℝ ) |
13 |
|
ltletr |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑀 + 𝐴 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 < ( 𝑀 + 𝐴 ) ∧ ( 𝑀 + 𝐴 ) ≤ 𝑁 ) → 𝑀 < 𝑁 ) ) |
14 |
5 11 12 13
|
syl3anc |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑀 < ( 𝑀 + 𝐴 ) ∧ ( 𝑀 + 𝐴 ) ≤ 𝑁 ) → 𝑀 < 𝑁 ) ) |
15 |
7 14
|
mpand |
⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → ( ( 𝑀 + 𝐴 ) ≤ 𝑁 → 𝑀 < 𝑁 ) ) |