Proof of Theorem iccdil
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ 𝑋 ∈
ℝ) |
| 2 | | rpre 13043 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
| 3 | | remulcl 11240 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑋 · 𝑅) ∈ ℝ) |
| 4 | 2, 3 | sylan2 593 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 · 𝑅) ∈
ℝ) |
| 5 | 1, 4 | 2thd 265 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 ∈ ℝ
↔ (𝑋 · 𝑅) ∈
ℝ)) |
| 6 | 5 | adantl 481 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ ℝ
↔ (𝑋 · 𝑅) ∈
ℝ)) |
| 7 | | elrp 13036 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
↔ (𝑅 ∈ ℝ
∧ 0 < 𝑅)) |
| 8 | | lemul1 12119 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ (𝑅 ∈ ℝ ∧ 0 <
𝑅)) → (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
| 9 | 7, 8 | syl3an3b 1407 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
| 10 | 9 | 3expb 1121 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
| 11 | 10 | adantlr 715 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
| 12 | | iccdil.1 |
. . . . 5
⊢ (𝐴 · 𝑅) = 𝐶 |
| 13 | 12 | breq1i 5150 |
. . . 4
⊢ ((𝐴 · 𝑅) ≤ (𝑋 · 𝑅) ↔ 𝐶 ≤ (𝑋 · 𝑅)) |
| 14 | 11, 13 | bitrdi 287 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ 𝐶 ≤ (𝑋 · 𝑅))) |
| 15 | | lemul1 12119 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑅 ∈ ℝ ∧ 0 <
𝑅)) → (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
| 16 | 7, 15 | syl3an3b 1407 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
| 17 | 16 | 3expb 1121 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
| 18 | 17 | an12s 649 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
| 19 | 18 | adantll 714 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
| 20 | | iccdil.2 |
. . . . 5
⊢ (𝐵 · 𝑅) = 𝐷 |
| 21 | 20 | breq2i 5151 |
. . . 4
⊢ ((𝑋 · 𝑅) ≤ (𝐵 · 𝑅) ↔ (𝑋 · 𝑅) ≤ 𝐷) |
| 22 | 19, 21 | bitrdi 287 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ 𝐷)) |
| 23 | 6, 14, 22 | 3anbi123d 1438 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ ((𝑋 ∈ ℝ
∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
| 24 | | elicc2 13452 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) |
| 25 | 24 | adantr 480 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) |
| 26 | | remulcl 11240 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐴 · 𝑅) ∈ ℝ) |
| 27 | 12, 26 | eqeltrrid 2846 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐶 ∈
ℝ) |
| 28 | | remulcl 11240 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐵 · 𝑅) ∈ ℝ) |
| 29 | 20, 28 | eqeltrrid 2846 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐷 ∈
ℝ) |
| 30 | | elicc2 13452 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
| 31 | 27, 29, 30 | syl2an 596 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
| 32 | 31 | anandirs 679 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
| 33 | 2, 32 | sylan2 593 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑅 ∈ ℝ+)
→ ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
| 34 | 33 | adantrl 716 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
| 35 | 23, 25, 34 | 3bitr4d 311 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))) |