Proof of Theorem ledivge1le
Step | Hyp | Ref
| Expression |
1 | | divle1le 9671 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 / 𝐵) ≤ 1 ↔ 𝐴 ≤ 𝐵)) |
2 | 1 | adantr 274 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 𝐶 ∈
ℝ+) → ((𝐴 / 𝐵) ≤ 1 ↔ 𝐴 ≤ 𝐵)) |
3 | | rerpdivcl 9630 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ) |
4 | 3 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 𝐶 ∈
ℝ+) → (𝐴 / 𝐵) ∈ ℝ) |
5 | | 1red 7924 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 𝐶 ∈
ℝ+) → 1 ∈ ℝ) |
6 | | rpre 9606 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℝ) |
7 | 6 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 𝐶 ∈
ℝ+) → 𝐶 ∈ ℝ) |
8 | | letr 7991 |
. . . . . . . . . 10
⊢ (((𝐴 / 𝐵) ∈ ℝ ∧ 1 ∈ ℝ
∧ 𝐶 ∈ ℝ)
→ (((𝐴 / 𝐵) ≤ 1 ∧ 1 ≤ 𝐶) → (𝐴 / 𝐵) ≤ 𝐶)) |
9 | 4, 5, 7, 8 | syl3anc 1233 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 𝐶 ∈
ℝ+) → (((𝐴 / 𝐵) ≤ 1 ∧ 1 ≤ 𝐶) → (𝐴 / 𝐵) ≤ 𝐶)) |
10 | 9 | expd 256 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 𝐶 ∈
ℝ+) → ((𝐴 / 𝐵) ≤ 1 → (1 ≤ 𝐶 → (𝐴 / 𝐵) ≤ 𝐶))) |
11 | 2, 10 | sylbird 169 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 𝐶 ∈
ℝ+) → (𝐴 ≤ 𝐵 → (1 ≤ 𝐶 → (𝐴 / 𝐵) ≤ 𝐶))) |
12 | 11 | com23 78 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 𝐶 ∈
ℝ+) → (1 ≤ 𝐶 → (𝐴 ≤ 𝐵 → (𝐴 / 𝐵) ≤ 𝐶))) |
13 | 12 | expimpd 361 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ ((𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶) → (𝐴 ≤ 𝐵 → (𝐴 / 𝐵) ≤ 𝐶))) |
14 | 13 | ex 114 |
. . . 4
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ+
→ ((𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶) → (𝐴 ≤ 𝐵 → (𝐴 / 𝐵) ≤ 𝐶)))) |
15 | 14 | 3imp1 1215 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 / 𝐵) ≤ 𝐶) |
16 | | simp1 992 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) → 𝐴 ∈ ℝ) |
17 | 6 | adantr 274 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ+
∧ 1 ≤ 𝐶) →
𝐶 ∈
ℝ) |
18 | | 0lt1 8035 |
. . . . . . . . . 10
⊢ 0 <
1 |
19 | | 0red 7910 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℝ+
→ 0 ∈ ℝ) |
20 | | 1red 7924 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ ℝ+
→ 1 ∈ ℝ) |
21 | | ltletr 7998 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((0 < 1 ∧ 1
≤ 𝐶) → 0 < 𝐶)) |
22 | 19, 20, 6, 21 | syl3anc 1233 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℝ+
→ ((0 < 1 ∧ 1 ≤ 𝐶) → 0 < 𝐶)) |
23 | 18, 22 | mpani 428 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ+
→ (1 ≤ 𝐶 → 0
< 𝐶)) |
24 | 23 | imp 123 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ+
∧ 1 ≤ 𝐶) → 0
< 𝐶) |
25 | 17, 24 | jca 304 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ+
∧ 1 ≤ 𝐶) →
(𝐶 ∈ ℝ ∧ 0
< 𝐶)) |
26 | 25 | 3ad2ant3 1015 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) → (𝐶 ∈ ℝ ∧ 0 < 𝐶)) |
27 | | rpregt0 9613 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ+
→ (𝐵 ∈ ℝ
∧ 0 < 𝐵)) |
28 | 27 | 3ad2ant2 1014 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) → (𝐵 ∈ ℝ ∧ 0 < 𝐵)) |
29 | 16, 26, 28 | 3jca 1172 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) → (𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵))) |
30 | 29 | adantr 274 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵))) |
31 | | lediv23 8798 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ (𝐴 / 𝐵) ≤ 𝐶)) |
32 | 30, 31 | syl 14 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ (𝐴 / 𝐵) ≤ 𝐶)) |
33 | 15, 32 | mpbird 166 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 / 𝐶) ≤ 𝐵) |
34 | 33 | ex 114 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ (𝐶 ∈
ℝ+ ∧ 1 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐴 / 𝐶) ≤ 𝐵)) |