Proof of Theorem iccdil
Step | Hyp | Ref
| Expression |
1 | | simpl 108 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ 𝑋 ∈
ℝ) |
2 | | rpre 9617 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
3 | | remulcl 7902 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑋 · 𝑅) ∈ ℝ) |
4 | 2, 3 | sylan2 284 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 · 𝑅) ∈
ℝ) |
5 | 1, 4 | 2thd 174 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 ∈ ℝ
↔ (𝑋 · 𝑅) ∈
ℝ)) |
6 | 5 | adantl 275 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ ℝ
↔ (𝑋 · 𝑅) ∈
ℝ)) |
7 | | elrp 9612 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
↔ (𝑅 ∈ ℝ
∧ 0 < 𝑅)) |
8 | | lemul1 8512 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ (𝑅 ∈ ℝ ∧ 0 <
𝑅)) → (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
9 | 7, 8 | syl3an3b 1271 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
10 | 9 | 3expb 1199 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
11 | 10 | adantlr 474 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
12 | | iccdil.1 |
. . . . 5
⊢ (𝐴 · 𝑅) = 𝐶 |
13 | 12 | breq1i 3996 |
. . . 4
⊢ ((𝐴 · 𝑅) ≤ (𝑋 · 𝑅) ↔ 𝐶 ≤ (𝑋 · 𝑅)) |
14 | 11, 13 | bitrdi 195 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ 𝐶 ≤ (𝑋 · 𝑅))) |
15 | | lemul1 8512 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑅 ∈ ℝ ∧ 0 <
𝑅)) → (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
16 | 7, 15 | syl3an3b 1271 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
17 | 16 | 3expb 1199 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
18 | 17 | an12s 560 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
19 | 18 | adantll 473 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
20 | | iccdil.2 |
. . . . 5
⊢ (𝐵 · 𝑅) = 𝐷 |
21 | 20 | breq2i 3997 |
. . . 4
⊢ ((𝑋 · 𝑅) ≤ (𝐵 · 𝑅) ↔ (𝑋 · 𝑅) ≤ 𝐷) |
22 | 19, 21 | bitrdi 195 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ 𝐷)) |
23 | 6, 14, 22 | 3anbi123d 1307 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ ((𝑋 ∈ ℝ
∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
24 | | elicc2 9895 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) |
25 | 24 | adantr 274 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) |
26 | | remulcl 7902 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐴 · 𝑅) ∈ ℝ) |
27 | 12, 26 | eqeltrrid 2258 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐶 ∈
ℝ) |
28 | | remulcl 7902 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐵 · 𝑅) ∈ ℝ) |
29 | 20, 28 | eqeltrrid 2258 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐷 ∈
ℝ) |
30 | | elicc2 9895 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
31 | 27, 29, 30 | syl2an 287 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
32 | 31 | anandirs 588 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
33 | 2, 32 | sylan2 284 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑅 ∈ ℝ+)
→ ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
34 | 33 | adantrl 475 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
35 | 23, 25, 34 | 3bitr4d 219 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))) |