Step |
Hyp |
Ref |
Expression |
1 |
|
xrleid |
⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴 ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐴 ≤ 𝐴 ) |
3 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐴 ∈ ℝ* ) |
4 |
|
0xr |
⊢ 0 ∈ ℝ* |
5 |
3 4
|
jctir |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ) ) |
6 |
|
xle2add |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ) ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ) → ( ( 𝐴 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ) ) |
7 |
5 6
|
mpancom |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ) ) |
8 |
2 7
|
mpand |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 → ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ) ) |
9 |
|
xaddid1 |
⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 0 ) = 𝐴 ) |
10 |
9
|
breq1d |
⊢ ( 𝐴 ∈ ℝ* → ( ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ↔ 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) ) ) |
11 |
10
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ↔ 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) ) ) |
12 |
8 11
|
sylibd |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) ) ) |