Proof of Theorem pntlemr
Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . . . . . . . . . . . 13
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
2 | | pntlem1.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
3 | | pntlem1.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
4 | | pntlem1.l |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) |
5 | | pntlem1.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (𝐴 + 1) |
6 | | pntlem1.f |
. . . . . . . . . . . . 13
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) |
7 | 1, 2, 3, 4, 5, 6 | pntlemd 26647 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+
∧ 𝐹 ∈
ℝ+)) |
8 | 7 | simp1d 1140 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈
ℝ+) |
9 | | pntlem1.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
10 | | pntlem1.u2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ≤ 𝐴) |
11 | | pntlem1.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (𝑈 / 𝐷) |
12 | | pntlem1.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) |
13 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12 | pntlemc 26648 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) |
14 | 13 | simp1d 1140 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
15 | 8, 14 | rpmulcld 12717 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 · 𝐸) ∈
ℝ+) |
16 | | 4re 11987 |
. . . . . . . . . . 11
⊢ 4 ∈
ℝ |
17 | | 4pos 12010 |
. . . . . . . . . . 11
⊢ 0 <
4 |
18 | 16, 17 | elrpii 12662 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ+ |
19 | | rpdivcl 12684 |
. . . . . . . . . 10
⊢ (((𝐿 · 𝐸) ∈ ℝ+ ∧ 4 ∈
ℝ+) → ((𝐿 · 𝐸) / 4) ∈
ℝ+) |
20 | 15, 18, 19 | sylancl 585 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈
ℝ+) |
21 | 20 | rpred 12701 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℝ) |
22 | | pntlem1.y |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) |
23 | | pntlem1.x |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) |
24 | | pntlem1.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
25 | | pntlem1.w |
. . . . . . . . . . . 12
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) |
26 | | pntlem1.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) |
27 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26 | pntlemb 26650 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) |
28 | 27 | simp1d 1140 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
29 | | pntlem1.v |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈
ℝ+) |
30 | 28, 29 | rpdivcld 12718 |
. . . . . . . . 9
⊢ (𝜑 → (𝑍 / 𝑉) ∈
ℝ+) |
31 | 30 | rpred 12701 |
. . . . . . . 8
⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ) |
32 | 21, 31 | remulcld 10936 |
. . . . . . 7
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ) |
33 | | pntlem1.i |
. . . . . . . . . 10
⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) |
34 | | fzfid 13621 |
. . . . . . . . . 10
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin) |
35 | 33, 34 | eqeltrid 2843 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ Fin) |
36 | | hashcl 13999 |
. . . . . . . . 9
⊢ (𝐼 ∈ Fin →
(♯‘𝐼) ∈
ℕ0) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐼) ∈
ℕ0) |
38 | 37 | nn0red 12224 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐼) ∈
ℝ) |
39 | 32 | recnd 10934 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℂ) |
40 | | 1rp 12663 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ+ |
41 | | rpaddcl 12681 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 +
(𝐿 · 𝐸)) ∈
ℝ+) |
42 | 40, 15, 41 | sylancr 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈
ℝ+) |
43 | 42, 29 | rpmulcld 12717 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈
ℝ+) |
44 | 28, 43 | rpdivcld 12718 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈
ℝ+) |
45 | 44 | rpred 12701 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ) |
46 | | reflcl 13444 |
. . . . . . . . . . . . . 14
⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ →
(⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) ∈ ℝ) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ) |
48 | 47 | recnd 10934 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℂ) |
49 | | 1cnd 10901 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
50 | 39, 48, 49 | add32d 11132 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) = (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) |
51 | | peano2re 11078 |
. . . . . . . . . . . . . 14
⊢ ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ) |
52 | 32, 51 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ) |
53 | 52, 47 | readdcld 10935 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ) |
54 | | reflcl 13444 |
. . . . . . . . . . . . . 14
⊢ ((𝑍 / 𝑉) ∈ ℝ →
(⌊‘(𝑍 / 𝑉)) ∈
ℝ) |
55 | 31, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℝ) |
56 | | peano2re 11078 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑍 /
𝑉)) ∈ ℝ →
((⌊‘(𝑍 / 𝑉)) + 1) ∈
ℝ) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ) |
58 | 15 | rphalfcld 12713 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈
ℝ+) |
59 | 58, 30 | rpmulcld 12717 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈
ℝ+) |
60 | 59 | rpred 12701 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ) |
61 | 60, 45 | readdcld 10935 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ) |
62 | | rpdivcl 12684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((4
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (4 /
(𝐿 · 𝐸)) ∈
ℝ+) |
63 | 18, 15, 62 | sylancr 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈
ℝ+) |
64 | 63 | rpred 12701 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ) |
65 | 28 | rpsqrtcld 15051 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (√‘𝑍) ∈
ℝ+) |
66 | 65 | rpred 12701 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (√‘𝑍) ∈
ℝ) |
67 | 27 | simp3d 1142 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) |
68 | 67 | simp1d 1140 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍)) |
69 | 43 | rpred 12701 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) |
70 | 13 | simp2d 1141 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
71 | | pntlem1.j |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁)) |
72 | | elfzoelz 13316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐽 ∈ ℤ) |
74 | 73 | peano2zd 12358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) |
75 | 70, 74 | rpexpcld 13890 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈
ℝ+) |
76 | 75 | rpred 12701 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ) |
77 | | pntlem1.V |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) |
78 | 77 | simplrd 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) |
79 | 70 | rpcnd 12703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐾 ∈ ℂ) |
80 | 70, 73 | rpexpcld 13890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (𝐾↑𝐽) ∈
ℝ+) |
81 | 80 | rpcnd 12703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ) |
82 | 79, 81 | mulcomd 10927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = ((𝐾↑𝐽) · 𝐾)) |
83 | | pntlem1.m |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 𝑀 =
((⌊‘((log‘𝑋) / (log‘𝐾))) + 1) |
84 | | pntlem1.n |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 𝑁 =
(⌊‘(((log‘𝑍) / (log‘𝐾)) / 2)) |
85 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84 | pntlemg 26651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀))) |
86 | 85 | simp1d 1140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑀 ∈ ℕ) |
87 | | elfzouz 13320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ≥‘𝑀)) |
88 | 71, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑀)) |
89 | | eluznn 12587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈
(ℤ≥‘𝑀)) → 𝐽 ∈ ℕ) |
90 | 86, 88, 89 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐽 ∈ ℕ) |
91 | 90 | nnnn0d 12223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
92 | 79, 91 | expp1d 13793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾)) |
93 | 82, 92 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1))) |
94 | 78, 93 | breqtrd 5096 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1))) |
95 | 69, 76, 94 | ltled 11053 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1))) |
96 | | fzofzp1 13412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁)) |
97 | 71, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁)) |
98 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84 | pntlemh 26652 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))) |
99 | 97, 98 | mpdan 683 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))) |
100 | 99 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)) |
101 | 69, 76, 66, 95, 100 | letrd 11062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍)) |
102 | 69, 66, 65 | lemul2d 12745 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))) |
103 | 101, 102 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))) |
104 | 28 | rprege0d 12708 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍)) |
105 | | remsqsqrt 14896 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍) ·
(√‘𝑍)) = 𝑍) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍) |
107 | 103, 106 | breqtrd 5096 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍) |
108 | 28 | rpred 12701 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑍 ∈ ℝ) |
109 | 66, 108, 43 | lemuldivd 12750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
110 | 107, 109 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) |
111 | 29 | rpcnd 12703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑉 ∈ ℂ) |
112 | 111 | mulid2d 10924 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 · 𝑉) = 𝑉) |
113 | | 1red 10907 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 ∈
ℝ) |
114 | 42 | rpred 12701 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ) |
115 | | 1re 10906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℝ |
116 | | ltaddrp 12696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℝ ∧ (𝐿
· 𝐸) ∈
ℝ+) → 1 < (1 + (𝐿 · 𝐸))) |
117 | 115, 15, 116 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 < (1 + (𝐿 · 𝐸))) |
118 | 113, 114,
29, 117 | ltmul1dd 12756 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 · 𝑉) < ((1 + (𝐿 · 𝐸)) · 𝑉)) |
119 | 112, 118 | eqbrtrrd 5094 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉)) |
120 | 29, 43, 28 | ltdiv2d 12724 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉) ↔ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉))) |
121 | 119, 120 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉)) |
122 | 45, 31, 121 | ltled 11053 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) |
123 | 66, 45, 31, 110, 122 | letrd 11062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑉)) |
124 | 64, 66, 31, 68, 123 | letrd 11062 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (𝑍 / 𝑉)) |
125 | 64, 31, 31, 124 | leadd2dd 11520 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ ((𝑍 / 𝑉) + (𝑍 / 𝑉))) |
126 | 30 | rpcnd 12703 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℂ) |
127 | 126 | 2timesd 12146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (𝑍 / 𝑉)) = ((𝑍 / 𝑉) + (𝑍 / 𝑉))) |
128 | 125, 127 | breqtrrd 5098 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉))) |
129 | 31, 64 | readdcld 10935 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ∈ ℝ) |
130 | | 2re 11977 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
131 | | remulcl 10887 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ (𝑍 /
𝑉) ∈ ℝ) →
(2 · (𝑍 / 𝑉)) ∈
ℝ) |
132 | 130, 31, 131 | sylancr 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (𝑍 / 𝑉)) ∈ ℝ) |
133 | 129, 132,
20 | lemul2d 12745 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))) |
134 | 128, 133 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))) |
135 | 20 | rpcnd 12703 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℂ) |
136 | 63 | rpcnd 12703 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℂ) |
137 | 135, 126,
136 | adddid 10930 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))))) |
138 | 15 | rpcnne0d 12710 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0)) |
139 | | rpcnne0 12677 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 ∈
ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0)) |
140 | 18, 139 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (4 ∈ ℂ ∧ 4
≠ 0)) |
141 | | divcan6 11612 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0) ∧ (4 ∈ ℂ ∧ 4
≠ 0)) → (((𝐿
· 𝐸) / 4) ·
(4 / (𝐿 · 𝐸))) = 1) |
142 | 138, 140,
141 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1) |
143 | 142 | oveq2d 7271 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1)) |
144 | 137, 143 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1)) |
145 | | 2cnd 11981 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℂ) |
146 | 135, 145,
126 | mulassd 10929 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))) |
147 | 15 | rpcnd 12703 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℂ) |
148 | | 2rp 12664 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ+ |
149 | | rpcnne0 12677 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0)) |
150 | 148, 149 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 ∈ ℂ ∧ 2
≠ 0)) |
151 | | divdiv1 11616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (2 ∈ ℂ
∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2))) |
152 | 147, 150,
150, 151 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2))) |
153 | | 2t2e4 12067 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 2) = 4 |
154 | 153 | oveq2i 7266 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 · 𝐸) / (2 · 2)) = ((𝐿 · 𝐸) / 4) |
155 | 152, 154 | eqtr2di 2796 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) = (((𝐿 · 𝐸) / 2) / 2)) |
156 | 155 | oveq1d 7270 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((((𝐿 · 𝐸) / 2) / 2) · 2)) |
157 | 147 | halfcld 12148 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℂ) |
158 | 150 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 2 ≠ 0) |
159 | 157, 145,
158 | divcan1d 11682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) / 2) · 2) = ((𝐿 · 𝐸) / 2)) |
160 | 156, 159 | eqtrd 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((𝐿 · 𝐸) / 2)) |
161 | 160 | oveq1d 7270 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉))) |
162 | 146, 161 | eqtr3d 2780 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉))) |
163 | 134, 144,
162 | 3brtr3d 5101 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ≤ (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉))) |
164 | | flle 13447 |
. . . . . . . . . . . . . . 15
⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ →
(⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) |
165 | 45, 164 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) |
166 | 52, 47, 60, 45, 163, 165 | le2addd 11524 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ≤ ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
167 | 58 | rpred 12701 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ) |
168 | 42 | rprecred 12712 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℝ) |
169 | 167, 168 | readdcld 10935 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) ∈ ℝ) |
170 | 15 | rpred 12701 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ) |
171 | 14 | rpred 12701 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸 ∈ ℝ) |
172 | 8 | rpred 12701 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐿 ∈ ℝ) |
173 | | eliooord 13067 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐿 ∈ (0(,)1) → (0 <
𝐿 ∧ 𝐿 < 1)) |
174 | 4, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1)) |
175 | 174 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐿 < 1) |
176 | 172, 113,
14, 175 | ltmul1dd 12756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸)) |
177 | 14 | rpcnd 12703 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐸 ∈ ℂ) |
178 | 177 | mulid2d 10924 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1 · 𝐸) = 𝐸) |
179 | 176, 178 | breqtrd 5096 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸) |
180 | 13 | simp3d 1142 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+)) |
181 | 180 | simp1d 1140 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
182 | | eliooord 13067 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
184 | 183 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸 < 1) |
185 | 170, 171,
113, 179, 184 | lttrd 11066 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 · 𝐸) < 1) |
186 | 170, 113,
113, 185 | ltadd2dd 11064 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1)) |
187 | | df-2 11966 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 = (1 +
1) |
188 | 186, 187 | breqtrrdi 5112 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2) |
189 | 42 | rpregt0d 12707 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸)))) |
190 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 2 ∈
ℝ) |
191 | | 2pos 12006 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 2) |
193 | 15 | rpregt0d 12707 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸))) |
194 | | ltdiv2 11791 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((1 +
(𝐿 · 𝐸)) ∈ ℝ ∧ 0 <
(1 + (𝐿 · 𝐸))) ∧ (2 ∈ ℝ
∧ 0 < 2) ∧ ((𝐿
· 𝐸) ∈ ℝ
∧ 0 < (𝐿 ·
𝐸))) → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))) |
195 | 189, 190,
192, 193, 194 | syl121anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))) |
196 | 188, 195 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))) |
197 | 42 | rpcnd 12703 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℂ) |
198 | 42 | rpcnne0d 12710 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) |
199 | | divsubdir 11599 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((1 +
(𝐿 · 𝐸)) ∈ ℂ ∧ 1 ∈
ℂ ∧ ((1 + (𝐿
· 𝐸)) ∈ ℂ
∧ (1 + (𝐿 ·
𝐸)) ≠ 0)) → (((1 +
(𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸))))) |
200 | 197, 49, 198, 199 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸))))) |
201 | | ax-1cn 10860 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℂ |
202 | | pncan2 11158 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℂ ∧ (𝐿
· 𝐸) ∈ ℂ)
→ ((1 + (𝐿 ·
𝐸)) − 1) = (𝐿 · 𝐸)) |
203 | 201, 147,
202 | sylancr 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸)) |
204 | 203 | oveq1d 7270 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))) |
205 | | divid 11592 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((1 +
(𝐿 · 𝐸)) ∈ ℂ ∧ (1 +
(𝐿 · 𝐸)) ≠ 0) → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1) |
206 | 198, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1) |
207 | 206 | oveq1d 7270 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))) = (1 − (1 / (1 + (𝐿 · 𝐸))))) |
208 | 200, 204,
207 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))) = (1 − (1 / (1 + (𝐿 · 𝐸))))) |
209 | 196, 208 | breqtrd 5096 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸))))) |
210 | 167, 168,
113 | ltaddsubd 11505 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1 ↔ ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸)))))) |
211 | 209, 210 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1) |
212 | 169, 113,
30, 211 | ltmul1dd 12756 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) < (1 · (𝑍 / 𝑉))) |
213 | | reccl 11570 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 +
(𝐿 · 𝐸)) ∈ ℂ ∧ (1 +
(𝐿 · 𝐸)) ≠ 0) → (1 / (1 +
(𝐿 · 𝐸))) ∈
ℂ) |
214 | 198, 213 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ) |
215 | 157, 214,
126 | adddird 10931 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))) |
216 | 197, 111 | mulcomd 10927 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) = (𝑉 · (1 + (𝐿 · 𝐸)))) |
217 | 216 | oveq2d 7271 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸))))) |
218 | 28 | rpcnd 12703 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑍 ∈ ℂ) |
219 | 29 | rpcnne0d 12710 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0)) |
220 | | divdiv1 11616 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑍 ∈ ℂ ∧ (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸))))) |
221 | 218, 219,
198, 220 | syl3anc 1369 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸))))) |
222 | 42 | rpne0d 12706 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≠ 0) |
223 | 126, 197,
222 | divrec2d 11685 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))) |
224 | 217, 221,
223 | 3eqtr2d 2784 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))) |
225 | 224 | oveq2d 7271 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))) |
226 | 215, 225 | eqtr4d 2781 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) |
227 | 126 | mulid2d 10924 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 · (𝑍 / 𝑉)) = (𝑍 / 𝑉)) |
228 | 212, 226,
227 | 3brtr3d 5101 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) < (𝑍 / 𝑉)) |
229 | 53, 61, 31, 166, 228 | lelttrd 11063 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (𝑍 / 𝑉)) |
230 | | fllep1 13449 |
. . . . . . . . . . . . 13
⊢ ((𝑍 / 𝑉) ∈ ℝ → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1)) |
231 | 31, 230 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1)) |
232 | 53, 31, 57, 229, 231 | ltletrd 11065 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < ((⌊‘(𝑍 / 𝑉)) + 1)) |
233 | 50, 232 | eqbrtrd 5092 |
. . . . . . . . . 10
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1)) |
234 | 32, 47 | readdcld 10935 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ) |
235 | 234, 55, 113 | ltadd1d 11498 |
. . . . . . . . . 10
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1))) |
236 | 233, 235 | mpbird 256 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉))) |
237 | 32, 47, 55 | ltaddsubd 11505 |
. . . . . . . . 9
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))) |
238 | 236, 237 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) |
239 | 31 | flcld 13446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ) |
240 | | fzval3 13384 |
. . . . . . . . . . . 12
⊢
((⌊‘(𝑍 /
𝑉)) ∈ ℤ →
(((⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) |
242 | 33, 241 | syl5eq 2791 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) |
243 | 242 | fveq2d 6760 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐼) =
(♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))) |
244 | | flword2 13461 |
. . . . . . . . . . . 12
⊢ (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) → (⌊‘(𝑍 / 𝑉)) ∈
(ℤ≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) |
245 | 45, 31, 122, 244 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈
(ℤ≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) |
246 | | eluzp1p1 12539 |
. . . . . . . . . . 11
⊢
((⌊‘(𝑍 /
𝑉)) ∈
(ℤ≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) → ((⌊‘(𝑍 / 𝑉)) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) |
247 | 245, 246 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) |
248 | | hashfzo 14072 |
. . . . . . . . . 10
⊢
(((⌊‘(𝑍
/ 𝑉)) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) →
(♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) |
249 | 247, 248 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) |
250 | 55 | recnd 10934 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℂ) |
251 | 250, 48, 49 | pnpcan2d 11300 |
. . . . . . . . 9
⊢ (𝜑 → (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) |
252 | 243, 249,
251 | 3eqtrd 2782 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐼) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) |
253 | 238, 252 | breqtrrd 5098 |
. . . . . . 7
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < (♯‘𝐼)) |
254 | 32, 38, 253 | ltled 11053 |
. . . . . 6
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼)) |
255 | 21, 38, 30 | lemuldivd 12750 |
. . . . . 6
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼) ↔ ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)))) |
256 | 254, 255 | mpbid 231 |
. . . . 5
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉))) |
257 | 29 | rpred 12701 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉 ∈ ℝ) |
258 | 69, 76, 66, 94, 100 | ltletrd 11065 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (√‘𝑍)) |
259 | 257, 69, 66, 119, 258 | lttrd 11066 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉 < (√‘𝑍)) |
260 | 257, 66, 259 | ltled 11053 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ≤ (√‘𝑍)) |
261 | 29 | rprege0d 12708 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉)) |
262 | 65 | rprege0d 12708 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) |
263 | | le2sq 13781 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ ℝ ∧ 0 ≤
𝑉) ∧
((√‘𝑍) ∈
ℝ ∧ 0 ≤ (√‘𝑍))) → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2))) |
264 | 261, 262,
263 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2))) |
265 | 260, 264 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑉↑2) ≤ ((√‘𝑍)↑2)) |
266 | | resqrtth 14895 |
. . . . . . . . . . . . . 14
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍)↑2)
= 𝑍) |
267 | 104, 266 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍) |
268 | 265, 267 | breqtrd 5096 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑉↑2) ≤ 𝑍) |
269 | | 2z 12282 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
270 | | rpexpcl 13729 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑉↑2) ∈
ℝ+) |
271 | 29, 269, 270 | sylancl 585 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑉↑2) ∈
ℝ+) |
272 | 271 | rpred 12701 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑉↑2) ∈ ℝ) |
273 | 272, 108,
28 | lemul2d 12745 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑉↑2) ≤ 𝑍 ↔ (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍))) |
274 | 268, 273 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍)) |
275 | 218 | sqvald 13789 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑍↑2) = (𝑍 · 𝑍)) |
276 | 274, 275 | breqtrrd 5098 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍↑2)) |
277 | 108 | resqcld 13893 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑍↑2) ∈ ℝ) |
278 | 108, 277,
271 | lemuldivd 12750 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑍 · (𝑉↑2)) ≤ (𝑍↑2) ↔ 𝑍 ≤ ((𝑍↑2) / (𝑉↑2)))) |
279 | 276, 278 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ≤ ((𝑍↑2) / (𝑉↑2))) |
280 | 29 | rpne0d 12706 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ≠ 0) |
281 | 218, 111,
280 | sqdivd 13805 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑍 / 𝑉)↑2) = ((𝑍↑2) / (𝑉↑2))) |
282 | 279, 281 | breqtrrd 5098 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ≤ ((𝑍 / 𝑉)↑2)) |
283 | | rpexpcl 13729 |
. . . . . . . . . 10
⊢ (((𝑍 / 𝑉) ∈ ℝ+ ∧ 2 ∈
ℤ) → ((𝑍 / 𝑉)↑2) ∈
ℝ+) |
284 | 30, 269, 283 | sylancl 585 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑍 / 𝑉)↑2) ∈
ℝ+) |
285 | 28, 284 | logled 25687 |
. . . . . . . 8
⊢ (𝜑 → (𝑍 ≤ ((𝑍 / 𝑉)↑2) ↔ (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2)))) |
286 | 282, 285 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2))) |
287 | | relogexp 25656 |
. . . . . . . 8
⊢ (((𝑍 / 𝑉) ∈ ℝ+ ∧ 2 ∈
ℤ) → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉)))) |
288 | 30, 269, 287 | sylancl 585 |
. . . . . . 7
⊢ (𝜑 → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉)))) |
289 | 286, 288 | breqtrd 5096 |
. . . . . 6
⊢ (𝜑 → (log‘𝑍) ≤ (2 ·
(log‘(𝑍 / 𝑉)))) |
290 | 28 | relogcld 25683 |
. . . . . . 7
⊢ (𝜑 → (log‘𝑍) ∈
ℝ) |
291 | 30 | relogcld 25683 |
. . . . . . 7
⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ) |
292 | | ledivmul 11781 |
. . . . . . 7
⊢
(((log‘𝑍)
∈ ℝ ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))) |
293 | 290, 291,
190, 192, 292 | syl112anc 1372 |
. . . . . 6
⊢ (𝜑 → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))) |
294 | 289, 293 | mpbird 256 |
. . . . 5
⊢ (𝜑 → ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) |
295 | 20 | rprege0d 12708 |
. . . . . 6
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4))) |
296 | 38, 30 | rerpdivcld 12732 |
. . . . . 6
⊢ (𝜑 → ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ) |
297 | 27 | simp2d 1141 |
. . . . . . . . . 10
⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌))) |
298 | 297 | simp1d 1140 |
. . . . . . . . 9
⊢ (𝜑 → 1 < 𝑍) |
299 | 108, 298 | rplogcld 25689 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝑍) ∈
ℝ+) |
300 | 299 | rphalfcld 12713 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝑍) / 2) ∈
ℝ+) |
301 | 300 | rprege0d 12708 |
. . . . . 6
⊢ (𝜑 → (((log‘𝑍) / 2) ∈ ℝ ∧ 0
≤ ((log‘𝑍) /
2))) |
302 | | lemul12a 11763 |
. . . . . 6
⊢
((((((𝐿 ·
𝐸) / 4) ∈ ℝ
∧ 0 ≤ ((𝐿 ·
𝐸) / 4)) ∧
((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ) ∧ ((((log‘𝑍) / 2) ∈ ℝ ∧ 0
≤ ((log‘𝑍) / 2))
∧ (log‘(𝑍 / 𝑉)) ∈ ℝ)) →
((((𝐿 · 𝐸) / 4) ≤
((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤
(((♯‘𝐼) /
(𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))) |
303 | 295, 296,
301, 291, 302 | syl22anc 835 |
. . . . 5
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤
(((♯‘𝐼) /
(𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))) |
304 | 256, 294,
303 | mp2and 695 |
. . . 4
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤
(((♯‘𝐼) /
(𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))) |
305 | 299 | rpcnd 12703 |
. . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℂ) |
306 | | 8nn 11998 |
. . . . . . . 8
⊢ 8 ∈
ℕ |
307 | | nnrp 12670 |
. . . . . . . 8
⊢ (8 ∈
ℕ → 8 ∈ ℝ+) |
308 | 306, 307 | ax-mp 5 |
. . . . . . 7
⊢ 8 ∈
ℝ+ |
309 | | rpcnne0 12677 |
. . . . . . 7
⊢ (8 ∈
ℝ+ → (8 ∈ ℂ ∧ 8 ≠ 0)) |
310 | 308, 309 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (8 ∈ ℂ ∧ 8
≠ 0)) |
311 | | div23 11582 |
. . . . . 6
⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ (8 ∈
ℂ ∧ 8 ≠ 0)) → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍))) |
312 | 147, 305,
310, 311 | syl3anc 1369 |
. . . . 5
⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍))) |
313 | | divmuldiv 11605 |
. . . . . . 7
⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ) ∧ ((4
∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) →
(((𝐿 · 𝐸) / 4) ·
((log‘𝑍) / 2)) =
(((𝐿 · 𝐸) · (log‘𝑍)) / (4 ·
2))) |
314 | 147, 305,
140, 150, 313 | syl22anc 835 |
. . . . . 6
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2))) |
315 | | 4t2e8 12071 |
. . . . . . 7
⊢ (4
· 2) = 8 |
316 | 315 | oveq2i 7266 |
. . . . . 6
⊢ (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / 8) |
317 | 314, 316 | eqtr2di 2796 |
. . . . 5
⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2))) |
318 | 312, 317 | eqtr3d 2780 |
. . . 4
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2))) |
319 | 38 | recnd 10934 |
. . . . 5
⊢ (𝜑 → (♯‘𝐼) ∈
ℂ) |
320 | 291 | recnd 10934 |
. . . . 5
⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℂ) |
321 | 30 | rpcnne0d 12710 |
. . . . 5
⊢ (𝜑 → ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) |
322 | | divass 11581 |
. . . . . 6
⊢
(((♯‘𝐼)
∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) |
323 | | div23 11582 |
. . . . . 6
⊢
(((♯‘𝐼)
∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))) |
324 | 322, 323 | eqtr3d 2780 |
. . . . 5
⊢
(((♯‘𝐼)
∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))) |
325 | 319, 320,
321, 324 | syl3anc 1369 |
. . . 4
⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))) |
326 | 304, 318,
325 | 3brtr4d 5102 |
. . 3
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) |
327 | | rpdivcl 12684 |
. . . . . . 7
⊢ (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈
ℝ+) → ((𝐿 · 𝐸) / 8) ∈
ℝ+) |
328 | 15, 308, 327 | sylancl 585 |
. . . . . 6
⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈
ℝ+) |
329 | 328, 299 | rpmulcld 12717 |
. . . . 5
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈
ℝ+) |
330 | 329 | rpred 12701 |
. . . 4
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ) |
331 | 291, 30 | rerpdivcld 12732 |
. . . . 5
⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ) |
332 | 38, 331 | remulcld 10936 |
. . . 4
⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ) |
333 | 180 | simp3d 1142 |
. . . 4
⊢ (𝜑 → (𝑈 − 𝐸) ∈
ℝ+) |
334 | 330, 332,
333 | lemul2d 12745 |
. . 3
⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ↔ ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))) |
335 | 326, 334 | mpbid 231 |
. 2
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) |
336 | 333 | rpcnd 12703 |
. . 3
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ) |
337 | 331 | recnd 10934 |
. . 3
⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℂ) |
338 | 336, 319,
337 | mul12d 11114 |
. 2
⊢ (𝜑 → ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) |
339 | 335, 338 | breqtrd 5096 |
1
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) |