Proof of Theorem ltdifltdiv
Step | Hyp | Ref
| Expression |
1 | | refldivcl 12486 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐵)) ∈
ℝ) |
2 | | peano2re 10088 |
. . . . . 6
⊢
((⌊‘(𝐴 /
𝐵)) ∈ ℝ →
((⌊‘(𝐴 / 𝐵)) + 1) ∈
ℝ) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ ((⌊‘(𝐴 /
𝐵)) + 1) ∈
ℝ) |
4 | 3 | 3adant3 1074 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((⌊‘(𝐴 /
𝐵)) + 1) ∈
ℝ) |
5 | 4 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((⌊‘(𝐴 / 𝐵)) + 1) ∈ ℝ) |
6 | | rerpdivcl 11737 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ) |
7 | | peano2re 10088 |
. . . . . 6
⊢ ((𝐴 / 𝐵) ∈ ℝ → ((𝐴 / 𝐵) + 1) ∈ ℝ) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 / 𝐵) + 1) ∈
ℝ) |
9 | 8 | 3adant3 1074 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐴 / 𝐵) + 1) ∈
ℝ) |
10 | 9 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((𝐴 / 𝐵) + 1) ∈ ℝ) |
11 | | rerpdivcl 11737 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐶 / 𝐵) ∈
ℝ) |
12 | 11 | ancoms 468 |
. . . . 5
⊢ ((𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐶 / 𝐵) ∈
ℝ) |
13 | 12 | 3adant1 1072 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐶 / 𝐵) ∈
ℝ) |
14 | 13 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (𝐶 / 𝐵) ∈ ℝ) |
15 | 1 | 3adant3 1074 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (⌊‘(𝐴 /
𝐵)) ∈
ℝ) |
16 | 15 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (⌊‘(𝐴 / 𝐵)) ∈ ℝ) |
17 | 6 | 3adant3 1074 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐴 / 𝐵) ∈
ℝ) |
18 | 17 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (𝐴 / 𝐵) ∈ ℝ) |
19 | | 1red 9934 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → 1 ∈ ℝ) |
20 | | 3simpa 1051 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐴 ∈ ℝ
∧ 𝐵 ∈
ℝ+)) |
21 | 20 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (𝐴 ∈ ℝ ∧ 𝐵 ∈
ℝ+)) |
22 | | fldivle 12494 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐵)) ≤ (𝐴 / 𝐵)) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (⌊‘(𝐴 / 𝐵)) ≤ (𝐴 / 𝐵)) |
24 | 16, 18, 19, 23 | leadd1dd 10520 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((⌊‘(𝐴 / 𝐵)) + 1) ≤ ((𝐴 / 𝐵) + 1)) |
25 | | rpre 11715 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ) |
26 | | ltaddsub 10381 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) |
27 | 25, 26 | syl3an2 1352 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) |
28 | 27 | biimpar 501 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (𝐴 + 𝐵) < 𝐶) |
29 | | recn 9905 |
. . . . . . . . . . 11
⊢ ((𝐴 / 𝐵) ∈ ℝ → (𝐴 / 𝐵) ∈ ℂ) |
30 | 6, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℂ) |
31 | 30 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐴 / 𝐵) ∈
ℂ) |
32 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 1 ∈ ℂ) |
33 | | rpcn 11717 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℂ) |
34 | 33 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐵 ∈
ℂ) |
35 | 31, 32, 34 | adddird 9944 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (((𝐴 / 𝐵) + 1) · 𝐵) = (((𝐴 / 𝐵) · 𝐵) + (1 · 𝐵))) |
36 | | recn 9905 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
37 | 36 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐴 ∈
ℂ) |
38 | | rpne0 11724 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ≠
0) |
39 | 38 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐵 ≠
0) |
40 | 37, 34, 39 | divcan1d 10681 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐴 / 𝐵) · 𝐵) = 𝐴) |
41 | 33 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ+
→ (1 · 𝐵) =
𝐵) |
42 | 41 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (1 · 𝐵) =
𝐵) |
43 | 40, 42 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (((𝐴 / 𝐵) · 𝐵) + (1 · 𝐵)) = (𝐴 + 𝐵)) |
44 | 35, 43 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (((𝐴 / 𝐵) + 1) · 𝐵) = (𝐴 + 𝐵)) |
45 | | recn 9905 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
46 | 45 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐶 ∈
ℂ) |
47 | 46, 34, 39 | divcan1d 10681 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐶 / 𝐵) · 𝐵) = 𝐶) |
48 | 44, 47 | breq12d 4596 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵) ↔ (𝐴 + 𝐵) < 𝐶)) |
49 | 48 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵) ↔ (𝐴 + 𝐵) < 𝐶)) |
50 | 28, 49 | mpbird 246 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵)) |
51 | 17, 7 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ ((𝐴 / 𝐵) + 1) ∈
ℝ) |
52 | | simp2 1055 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ 𝐵 ∈
ℝ+) |
53 | 51, 13, 52 | ltmul1d 11789 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (((𝐴 / 𝐵) + 1) < (𝐶 / 𝐵) ↔ (((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵))) |
54 | 53 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → (((𝐴 / 𝐵) + 1) < (𝐶 / 𝐵) ↔ (((𝐴 / 𝐵) + 1) · 𝐵) < ((𝐶 / 𝐵) · 𝐵))) |
55 | 50, 54 | mpbird 246 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((𝐴 / 𝐵) + 1) < (𝐶 / 𝐵)) |
56 | 5, 10, 14, 24, 55 | lelttrd 10074 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
∧ 𝐴 < (𝐶 − 𝐵)) → ((⌊‘(𝐴 / 𝐵)) + 1) < (𝐶 / 𝐵)) |
57 | 56 | ex 449 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝐶 ∈ ℝ)
→ (𝐴 < (𝐶 − 𝐵) → ((⌊‘(𝐴 / 𝐵)) + 1) < (𝐶 / 𝐵))) |