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