Step |
Hyp |
Ref |
Expression |
1 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℝ ) |
2 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℝ ) |
3 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℝ ) |
4 |
|
lesub1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐶 ↔ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐵 ) ) ) |
5 |
1 2 3 4
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 ≤ 𝐶 ↔ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐵 ) ) ) |
6 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℝ ) |
7 |
|
lesub2 |
⊢ ( ( 𝐷 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐷 ≤ 𝐵 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ) |
8 |
6 3 2 7
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐷 ≤ 𝐵 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ) |
9 |
5 8
|
anbi12d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐵 ) ∧ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ) ) |
10 |
|
resubcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ ) |
11 |
10
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ ) |
12 |
2 3
|
resubcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 − 𝐵 ) ∈ ℝ ) |
13 |
|
resubcl |
⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 − 𝐷 ) ∈ ℝ ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 − 𝐷 ) ∈ ℝ ) |
15 |
|
letr |
⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ ( 𝐶 − 𝐵 ) ∈ ℝ ∧ ( 𝐶 − 𝐷 ) ∈ ℝ ) → ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐵 ) ∧ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ) |
16 |
11 12 14 15
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐵 ) ∧ ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ) |
17 |
9 16
|
sylbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ) |