Proof of Theorem pntibndlem1
Step | Hyp | Ref
| Expression |
1 | | pntibndlem1.l |
. . . 4
⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) |
2 | | 4nn 11187 |
. . . . . 6
⊢ 4 ∈
ℕ |
3 | | nnrp 11842 |
. . . . . 6
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
4 | | rpreccl 11857 |
. . . . . 6
⊢ (4 ∈
ℝ+ → (1 / 4) ∈ ℝ+) |
5 | 2, 3, 4 | mp2b 10 |
. . . . 5
⊢ (1 / 4)
∈ ℝ+ |
6 | | pntibndlem1.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
7 | | 3nn 11186 |
. . . . . . 7
⊢ 3 ∈
ℕ |
8 | | nnrp 11842 |
. . . . . . 7
⊢ (3 ∈
ℕ → 3 ∈ ℝ+) |
9 | 7, 8 | ax-mp 5 |
. . . . . 6
⊢ 3 ∈
ℝ+ |
10 | | rpaddcl 11854 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 3 ∈ ℝ+) → (𝐴 + 3) ∈
ℝ+) |
11 | 6, 9, 10 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (𝐴 + 3) ∈
ℝ+) |
12 | | rpdivcl 11856 |
. . . . 5
⊢ (((1 / 4)
∈ ℝ+ ∧ (𝐴 + 3) ∈ ℝ+) → ((1
/ 4) / (𝐴 + 3)) ∈
ℝ+) |
13 | 5, 11, 12 | sylancr 695 |
. . . 4
⊢ (𝜑 → ((1 / 4) / (𝐴 + 3)) ∈
ℝ+) |
14 | 1, 13 | syl5eqel 2705 |
. . 3
⊢ (𝜑 → 𝐿 ∈
ℝ+) |
15 | 14 | rpred 11872 |
. 2
⊢ (𝜑 → 𝐿 ∈ ℝ) |
16 | 14 | rpgt0d 11875 |
. 2
⊢ (𝜑 → 0 < 𝐿) |
17 | | rpcn 11841 |
. . . . . . 7
⊢ ((1 / 4)
∈ ℝ+ → (1 / 4) ∈ ℂ) |
18 | 5, 17 | ax-mp 5 |
. . . . . 6
⊢ (1 / 4)
∈ ℂ |
19 | 18 | div1i 10753 |
. . . . 5
⊢ ((1 / 4)
/ 1) = (1 / 4) |
20 | | rpre 11839 |
. . . . . . 7
⊢ ((1 / 4)
∈ ℝ+ → (1 / 4) ∈ ℝ) |
21 | 5, 20 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (1 / 4) ∈
ℝ) |
22 | | 3re 11094 |
. . . . . . 7
⊢ 3 ∈
ℝ |
23 | 22 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 3 ∈
ℝ) |
24 | 11 | rpred 11872 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 3) ∈ ℝ) |
25 | | 1lt4 11199 |
. . . . . . . . 9
⊢ 1 <
4 |
26 | | 4re 11097 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
27 | | 4pos 11116 |
. . . . . . . . . 10
⊢ 0 <
4 |
28 | | recgt1 10919 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ ∧ 0 < 4) → (1 < 4 ↔ (1 / 4) <
1)) |
29 | 26, 27, 28 | mp2an 708 |
. . . . . . . . 9
⊢ (1 < 4
↔ (1 / 4) < 1) |
30 | 25, 29 | mpbi 220 |
. . . . . . . 8
⊢ (1 / 4)
< 1 |
31 | | 1lt3 11196 |
. . . . . . . 8
⊢ 1 <
3 |
32 | 5, 20 | ax-mp 5 |
. . . . . . . . 9
⊢ (1 / 4)
∈ ℝ |
33 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
34 | 32, 33, 22 | lttri 10163 |
. . . . . . . 8
⊢ (((1 / 4)
< 1 ∧ 1 < 3) → (1 / 4) < 3) |
35 | 30, 31, 34 | mp2an 708 |
. . . . . . 7
⊢ (1 / 4)
< 3 |
36 | 35 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1 / 4) <
3) |
37 | | ltaddrp 11867 |
. . . . . . . 8
⊢ ((3
∈ ℝ ∧ 𝐴
∈ ℝ+) → 3 < (3 + 𝐴)) |
38 | 22, 6, 37 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → 3 < (3 + 𝐴)) |
39 | | 3cn 11095 |
. . . . . . . 8
⊢ 3 ∈
ℂ |
40 | 6 | rpcnd 11874 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
41 | | addcom 10222 |
. . . . . . . 8
⊢ ((3
∈ ℂ ∧ 𝐴
∈ ℂ) → (3 + 𝐴) = (𝐴 + 3)) |
42 | 39, 40, 41 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → (3 + 𝐴) = (𝐴 + 3)) |
43 | 38, 42 | breqtrd 4679 |
. . . . . 6
⊢ (𝜑 → 3 < (𝐴 + 3)) |
44 | 21, 23, 24, 36, 43 | lttrd 10198 |
. . . . 5
⊢ (𝜑 → (1 / 4) < (𝐴 + 3)) |
45 | 19, 44 | syl5eqbr 4688 |
. . . 4
⊢ (𝜑 → ((1 / 4) / 1) < (𝐴 + 3)) |
46 | 33 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
47 | | 0lt1 10550 |
. . . . . 6
⊢ 0 <
1 |
48 | 47 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 < 1) |
49 | 11 | rpregt0d 11878 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 3) ∈ ℝ ∧ 0 < (𝐴 + 3))) |
50 | | ltdiv23 10914 |
. . . . 5
⊢ (((1 / 4)
∈ ℝ ∧ (1 ∈ ℝ ∧ 0 < 1) ∧ ((𝐴 + 3) ∈ ℝ ∧ 0
< (𝐴 + 3))) → (((1
/ 4) / 1) < (𝐴 + 3)
↔ ((1 / 4) / (𝐴 + 3))
< 1)) |
51 | 21, 46, 48, 49, 50 | syl121anc 1331 |
. . . 4
⊢ (𝜑 → (((1 / 4) / 1) < (𝐴 + 3) ↔ ((1 / 4) / (𝐴 + 3)) < 1)) |
52 | 45, 51 | mpbid 222 |
. . 3
⊢ (𝜑 → ((1 / 4) / (𝐴 + 3)) < 1) |
53 | 1, 52 | syl5eqbr 4688 |
. 2
⊢ (𝜑 → 𝐿 < 1) |
54 | | 0xr 10086 |
. . 3
⊢ 0 ∈
ℝ* |
55 | 33 | rexri 10097 |
. . 3
⊢ 1 ∈
ℝ* |
56 | | elioo2 12216 |
. . 3
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → (𝐿 ∈ (0(,)1) ↔ (𝐿 ∈ ℝ ∧ 0 <
𝐿 ∧ 𝐿 < 1))) |
57 | 54, 55, 56 | mp2an 708 |
. 2
⊢ (𝐿 ∈ (0(,)1) ↔ (𝐿 ∈ ℝ ∧ 0 <
𝐿 ∧ 𝐿 < 1)) |
58 | 15, 16, 53, 57 | syl3anbrc 1246 |
1
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) |