Proof of Theorem ltdifltdiv
| Step | Hyp | Ref
| Expression |
| 1 | | refldivcl 13863 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐵)) ∈
ℝ) |
| 2 | | peano2re 11434 |
. . . . . 6
⊢
((⌊‘(𝐴 /
𝐵)) ∈ ℝ →
((⌊‘(𝐴 / 𝐵)) + 1) ∈
ℝ) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ ((⌊‘(𝐴 /
𝐵)) + 1) ∈
ℝ) |
| 4 | 3 | 3adant3 1133 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((⌊‘(𝐴 /
𝐵)) + 1) ∈
ℝ) |
| 5 | 4 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((⌊‘(𝐴 / 𝐵)) + 1) ∈ ℝ) |
| 6 | | rerpdivcl 13065 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ) |
| 7 | | peano2re 11434 |
. . . . . 6
⊢ ((𝐴 / 𝐵) ∈ ℝ → ((𝐴 / 𝐵) + 1) ∈ ℝ) |
| 8 | 6, 7 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 / 𝐵) + 1) ∈
ℝ) |
| 9 | 8 | 3adant3 1133 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐴 / 𝐵) + 1) ∈
ℝ) |
| 10 | 9 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((𝐴 / 𝐵) + 1) ∈ ℝ) |
| 11 | | rerpdivcl 13065 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐶 / 𝐵) ∈
ℝ) |
| 12 | 11 | ancoms 458 |
. . . . 5
⊢ ((𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐶 / 𝐵) ∈
ℝ) |
| 13 | 12 | 3adant1 1131 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐶 / 𝐵) ∈
ℝ) |
| 14 | 13 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (𝐶 / 𝐵) ∈ ℝ) |
| 15 | 1 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (⌊‘(𝐴 /
𝐵)) ∈
ℝ) |
| 16 | 15 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (⌊‘(𝐴 / 𝐵)) ∈ ℝ) |
| 17 | 6 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐴 / 𝐵) ∈
ℝ) |
| 18 | 17 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (𝐴 / 𝐵) ∈ ℝ) |
| 19 | | 1red 11262 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → 1 ∈ ℝ) |
| 20 | | 3simpa 1149 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐴 ∈ ℝ
∧ 𝐵 ∈
ℝ+)) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (𝐴 ∈ ℝ ∧ 𝐵 ∈
ℝ+)) |
| 22 | | fldivle 13871 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐵)) ≤ (𝐴 / 𝐵)) |
| 23 | 21, 22 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (⌊‘(𝐴 / 𝐵)) ≤ (𝐴 / 𝐵)) |
| 24 | 16, 18, 19, 23 | leadd1dd 11877 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((⌊‘(𝐴 / 𝐵)) + 1) ≤ ((𝐴 / 𝐵) + 1)) |
| 25 | | rpre 13043 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ) |
| 26 | | ltaddsub 11737 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) |
| 27 | 25, 26 | syl3an2 1165 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) |
| 28 | 27 | biimpar 477 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (𝐴 + 𝐵) < 𝐶) |
| 29 | | recn 11245 |
. . . . . . . . . 10
⊢ ((𝐴 / 𝐵) ∈ ℝ → (𝐴 / 𝐵) ∈ ℂ) |
| 30 | 6, 29 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℂ) |
| 31 | 30 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐴 / 𝐵) ∈
ℂ) |
| 32 | | rpcn 13045 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℂ) |
| 33 | 32 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐵 ∈
ℂ) |
| 34 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 1 ∈ ℂ) |
| 35 | | recn 11245 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 36 | 35 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐴 ∈
ℂ) |
| 37 | | rpne0 13051 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ≠
0) |
| 38 | 37 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐵 ≠
0) |
| 39 | 36, 33, 38 | divcan1d 12044 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐴 / 𝐵) · 𝐵) = 𝐴) |
| 40 | 32 | mullidd 11279 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ+
→ (1 · 𝐵) =
𝐵) |
| 41 | 40 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (1 · 𝐵) =
𝐵) |
| 42 | 39, 41 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (((𝐴 / 𝐵) · 𝐵) + (1 · 𝐵)) = (𝐴 + 𝐵)) |
| 43 | 31, 33, 34, 42 | joinlmuladdmuld 11288 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (((𝐴 / 𝐵) + 1) · 𝐵) = (𝐴 + 𝐵)) |
| 44 | | recn 11245 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
| 45 | 44 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐶 ∈
ℂ) |
| 46 | 45, 33, 38 | divcan1d 12044 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐶 / 𝐵) · 𝐵) = 𝐶) |
| 47 | 43, 46 | breq12d 5156 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵) ↔ (𝐴 + 𝐵) < 𝐶)) |
| 48 | 47 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵) ↔ (𝐴 + 𝐵) < 𝐶)) |
| 49 | 28, 48 | mpbird 257 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵)) |
| 50 | 17, 7 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐴 / 𝐵) + 1) ∈
ℝ) |
| 51 | | simp2 1138 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐵 ∈
ℝ+) |
| 52 | 50, 13, 51 | ltmul1d 13118 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (((𝐴 / 𝐵) + 1) < (𝐶 / 𝐵) ↔ (((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵))) |
| 53 | 52 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (((𝐴 / 𝐵) + 1) < (𝐶 / 𝐵) ↔ (((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵))) |
| 54 | 49, 53 | mpbird 257 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((𝐴 / 𝐵) + 1) < (𝐶 / 𝐵)) |
| 55 | 5, 10, 14, 24, 54 | lelttrd 11419 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((⌊‘(𝐴 / 𝐵)) + 1) < (𝐶 / 𝐵)) |
| 56 | 55 | ex 412 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐴 < (𝐶 − 𝐵) → ((⌊‘(𝐴 / 𝐵)) + 1) < (𝐶 / 𝐵))) |