Step |
Hyp |
Ref |
Expression |
1 |
|
rlimle.1 |
⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ ) |
2 |
|
rlimle.2 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 ) |
3 |
|
rlimle.3 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 ) |
4 |
|
rlimle.4 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) |
5 |
|
rlimle.5 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ ) |
6 |
|
rlimle.6 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 ) |
7 |
5 4 3 2
|
rlimsub |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐵 ) ) ⇝𝑟 ( 𝐸 − 𝐷 ) ) |
8 |
5 4
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 − 𝐵 ) ∈ ℝ ) |
9 |
5 4
|
subge0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ ( 𝐶 − 𝐵 ) ↔ 𝐵 ≤ 𝐶 ) ) |
10 |
6 9
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( 𝐶 − 𝐵 ) ) |
11 |
1 7 8 10
|
rlimge0 |
⊢ ( 𝜑 → 0 ≤ ( 𝐸 − 𝐷 ) ) |
12 |
1 3 5
|
rlimrecl |
⊢ ( 𝜑 → 𝐸 ∈ ℝ ) |
13 |
1 2 4
|
rlimrecl |
⊢ ( 𝜑 → 𝐷 ∈ ℝ ) |
14 |
12 13
|
subge0d |
⊢ ( 𝜑 → ( 0 ≤ ( 𝐸 − 𝐷 ) ↔ 𝐷 ≤ 𝐸 ) ) |
15 |
11 14
|
mpbid |
⊢ ( 𝜑 → 𝐷 ≤ 𝐸 ) |