Proof of Theorem iccdil
Step | Hyp | Ref
| Expression |
1 | | simpl 476 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ 𝑋 ∈
ℝ) |
2 | | rpre 12145 |
. . . . . 6
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ) |
3 | | remulcl 10357 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝑋 · 𝑅) ∈ ℝ) |
4 | 2, 3 | sylan2 586 |
. . . . 5
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 · 𝑅) ∈
ℝ) |
5 | 1, 4 | 2thd 257 |
. . . 4
⊢ ((𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 ∈ ℝ
↔ (𝑋 · 𝑅) ∈
ℝ)) |
6 | 5 | adantl 475 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ ℝ
↔ (𝑋 · 𝑅) ∈
ℝ)) |
7 | | elrp 12139 |
. . . . . . 7
⊢ (𝑅 ∈ ℝ+
↔ (𝑅 ∈ ℝ
∧ 0 < 𝑅)) |
8 | | lemul1 11229 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ (𝑅 ∈ ℝ ∧ 0 <
𝑅)) → (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
9 | 7, 8 | syl3an3b 1473 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
10 | 9 | 3expb 1110 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
11 | 10 | adantlr 705 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ (𝐴 · 𝑅) ≤ (𝑋 · 𝑅))) |
12 | | iccdil.1 |
. . . . 5
⊢ (𝐴 · 𝑅) = 𝐶 |
13 | 12 | breq1i 4893 |
. . . 4
⊢ ((𝐴 · 𝑅) ≤ (𝑋 · 𝑅) ↔ 𝐶 ≤ (𝑋 · 𝑅)) |
14 | 11, 13 | syl6bb 279 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝐴 ≤ 𝑋 ↔ 𝐶 ≤ (𝑋 · 𝑅))) |
15 | | lemul1 11229 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑅 ∈ ℝ ∧ 0 <
𝑅)) → (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
16 | 7, 15 | syl3an3b 1473 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ+)
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
17 | 16 | 3expb 1110 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
18 | 17 | an12s 639 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
19 | 18 | adantll 704 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ (𝐵 · 𝑅))) |
20 | | iccdil.2 |
. . . . 5
⊢ (𝐵 · 𝑅) = 𝐷 |
21 | 20 | breq2i 4894 |
. . . 4
⊢ ((𝑋 · 𝑅) ≤ (𝐵 · 𝑅) ↔ (𝑋 · 𝑅) ≤ 𝐷) |
22 | 19, 21 | syl6bb 279 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ≤ 𝐵 ↔ (𝑋 · 𝑅) ≤ 𝐷)) |
23 | 6, 14, 22 | 3anbi123d 1509 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ ((𝑋 ∈ ℝ
∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
24 | | elicc2 12550 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) |
25 | 24 | adantr 474 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) |
26 | | remulcl 10357 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐴 · 𝑅) ∈ ℝ) |
27 | 12, 26 | syl5eqelr 2864 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐶 ∈
ℝ) |
28 | | remulcl 10357 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (𝐵 · 𝑅) ∈ ℝ) |
29 | 20, 28 | syl5eqelr 2864 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ) → 𝐷 ∈
ℝ) |
30 | | elicc2 12550 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
31 | 27, 29, 30 | syl2an 589 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑅 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 𝑅 ∈ ℝ)) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
32 | 31 | anandirs 669 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑅 ∈ ℝ) → ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
33 | 2, 32 | sylan2 586 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑅 ∈ ℝ+)
→ ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
34 | 33 | adantrl 706 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ ((𝑋 · 𝑅) ∈ (𝐶[,]𝐷) ↔ ((𝑋 · 𝑅) ∈ ℝ ∧ 𝐶 ≤ (𝑋 · 𝑅) ∧ (𝑋 · 𝑅) ≤ 𝐷))) |
35 | 23, 25, 34 | 3bitr4d 303 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑋 ∈ ℝ ∧ 𝑅 ∈ ℝ+))
→ (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 · 𝑅) ∈ (𝐶[,]𝐷))) |