Step |
Hyp |
Ref |
Expression |
1 |
|
iccshftr.1 |
⊢ ( 𝐴 + 𝑅 ) = 𝐶 |
2 |
|
iccshftr.2 |
⊢ ( 𝐵 + 𝑅 ) = 𝐷 |
3 |
|
simpl |
⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → 𝑋 ∈ ℝ ) |
4 |
|
readdcl |
⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑋 + 𝑅 ) ∈ ℝ ) |
5 |
3 4
|
2thd |
⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑋 ∈ ℝ ↔ ( 𝑋 + 𝑅 ) ∈ ℝ ) ) |
6 |
5
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝑋 ∈ ℝ ↔ ( 𝑋 + 𝑅 ) ∈ ℝ ) ) |
7 |
|
leadd1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝐴 ≤ 𝑋 ↔ ( 𝐴 + 𝑅 ) ≤ ( 𝑋 + 𝑅 ) ) ) |
8 |
7
|
3expb |
⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝐴 ≤ 𝑋 ↔ ( 𝐴 + 𝑅 ) ≤ ( 𝑋 + 𝑅 ) ) ) |
9 |
8
|
adantlr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝐴 ≤ 𝑋 ↔ ( 𝐴 + 𝑅 ) ≤ ( 𝑋 + 𝑅 ) ) ) |
10 |
1
|
breq1i |
⊢ ( ( 𝐴 + 𝑅 ) ≤ ( 𝑋 + 𝑅 ) ↔ 𝐶 ≤ ( 𝑋 + 𝑅 ) ) |
11 |
9 10
|
bitrdi |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝐴 ≤ 𝑋 ↔ 𝐶 ≤ ( 𝑋 + 𝑅 ) ) ) |
12 |
|
leadd1 |
⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝑋 ≤ 𝐵 ↔ ( 𝑋 + 𝑅 ) ≤ ( 𝐵 + 𝑅 ) ) ) |
13 |
12
|
3expb |
⊢ ( ( 𝑋 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝑋 ≤ 𝐵 ↔ ( 𝑋 + 𝑅 ) ≤ ( 𝐵 + 𝑅 ) ) ) |
14 |
13
|
an12s |
⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝑋 ≤ 𝐵 ↔ ( 𝑋 + 𝑅 ) ≤ ( 𝐵 + 𝑅 ) ) ) |
15 |
14
|
adantll |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝑋 ≤ 𝐵 ↔ ( 𝑋 + 𝑅 ) ≤ ( 𝐵 + 𝑅 ) ) ) |
16 |
2
|
breq2i |
⊢ ( ( 𝑋 + 𝑅 ) ≤ ( 𝐵 + 𝑅 ) ↔ ( 𝑋 + 𝑅 ) ≤ 𝐷 ) |
17 |
15 16
|
bitrdi |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝑋 ≤ 𝐵 ↔ ( 𝑋 + 𝑅 ) ≤ 𝐷 ) ) |
18 |
6 11 17
|
3anbi123d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ↔ ( ( 𝑋 + 𝑅 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑋 + 𝑅 ) ∧ ( 𝑋 + 𝑅 ) ≤ 𝐷 ) ) ) |
19 |
|
elicc2 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) ) |
20 |
19
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) ) |
21 |
|
readdcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝐴 + 𝑅 ) ∈ ℝ ) |
22 |
1 21
|
eqeltrrid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → 𝐶 ∈ ℝ ) |
23 |
|
readdcl |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 𝐵 + 𝑅 ) ∈ ℝ ) |
24 |
2 23
|
eqeltrrid |
⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → 𝐷 ∈ ℝ ) |
25 |
|
elicc2 |
⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑋 + 𝑅 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑋 + 𝑅 ) ∧ ( 𝑋 + 𝑅 ) ≤ 𝐷 ) ) ) |
26 |
22 24 25
|
syl2an |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑋 + 𝑅 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑋 + 𝑅 ) ∧ ( 𝑋 + 𝑅 ) ≤ 𝐷 ) ) ) |
27 |
26
|
anandirs |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑋 + 𝑅 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑋 + 𝑅 ) ∧ ( 𝑋 + 𝑅 ) ≤ 𝐷 ) ) ) |
28 |
27
|
adantrl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ↔ ( ( 𝑋 + 𝑅 ) ∈ ℝ ∧ 𝐶 ≤ ( 𝑋 + 𝑅 ) ∧ ( 𝑋 + 𝑅 ) ≤ 𝐷 ) ) ) |
29 |
18 20 28
|
3bitr4d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ ) ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 + 𝑅 ) ∈ ( 𝐶 [,] 𝐷 ) ) ) |