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 27638 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+
∧ 𝐹 ∈
ℝ+)) | 
| 8 | 7 | simp1d 1143 | . . . . . . . . . . 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 27639 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) | 
| 14 | 13 | simp1d 1143 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 15 | 8, 14 | rpmulcld 13093 | . . . . . . . . . 10
⊢ (𝜑 → (𝐿 · 𝐸) ∈
ℝ+) | 
| 16 |  | 4re 12350 | . . . . . . . . . . 11
⊢ 4 ∈
ℝ | 
| 17 |  | 4pos 12373 | . . . . . . . . . . 11
⊢ 0 <
4 | 
| 18 | 16, 17 | elrpii 13037 | . . . . . . . . . 10
⊢ 4 ∈
ℝ+ | 
| 19 |  | rpdivcl 13060 | . . . . . . . . . 10
⊢ (((𝐿 · 𝐸) ∈ ℝ+ ∧ 4 ∈
ℝ+) → ((𝐿 · 𝐸) / 4) ∈
ℝ+) | 
| 20 | 15, 18, 19 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈
ℝ+) | 
| 21 | 20 | rpred 13077 | . . . . . . . 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 27641 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 28 | 27 | simp1d 1143 | . . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈
ℝ+) | 
| 29 |  | pntlem1.v | . . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈
ℝ+) | 
| 30 | 28, 29 | rpdivcld 13094 | . . . . . . . . 9
⊢ (𝜑 → (𝑍 / 𝑉) ∈
ℝ+) | 
| 31 | 30 | rpred 13077 | . . . . . . . 8
⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ) | 
| 32 | 21, 31 | remulcld 11291 | . . . . . . 7
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ) | 
| 33 |  | pntlem1.i | . . . . . . . . . 10
⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) | 
| 34 |  | fzfid 14014 | . . . . . . . . . 10
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin) | 
| 35 | 33, 34 | eqeltrid 2845 | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ Fin) | 
| 36 |  | hashcl 14395 | . . . . . . . . 9
⊢ (𝐼 ∈ Fin →
(♯‘𝐼) ∈
ℕ0) | 
| 37 | 35, 36 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (♯‘𝐼) ∈
ℕ0) | 
| 38 | 37 | nn0red 12588 | . . . . . . 7
⊢ (𝜑 → (♯‘𝐼) ∈
ℝ) | 
| 39 | 32 | recnd 11289 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℂ) | 
| 40 |  | 1rp 13038 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ+ | 
| 41 |  | rpaddcl 13057 | . . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 +
(𝐿 · 𝐸)) ∈
ℝ+) | 
| 42 | 40, 15, 41 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈
ℝ+) | 
| 43 | 42, 29 | rpmulcld 13093 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈
ℝ+) | 
| 44 | 28, 43 | rpdivcld 13094 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈
ℝ+) | 
| 45 | 44 | rpred 13077 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ) | 
| 46 |  | reflcl 13836 | . . . . . . . . . . . . . 14
⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ →
(⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) ∈ ℝ) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ) | 
| 48 | 47 | recnd 11289 | . . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℂ) | 
| 49 |  | 1cnd 11256 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) | 
| 50 | 39, 48, 49 | add32d 11489 | . . . . . . . . . . 11
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) = (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) | 
| 51 |  | peano2re 11434 | . . . . . . . . . . . . . 14
⊢ ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ) | 
| 52 | 32, 51 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ) | 
| 53 | 52, 47 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ) | 
| 54 |  | reflcl 13836 | . . . . . . . . . . . . . 14
⊢ ((𝑍 / 𝑉) ∈ ℝ →
(⌊‘(𝑍 / 𝑉)) ∈
ℝ) | 
| 55 | 31, 54 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℝ) | 
| 56 |  | peano2re 11434 | . . . . . . . . . . . . 13
⊢
((⌊‘(𝑍 /
𝑉)) ∈ ℝ →
((⌊‘(𝑍 / 𝑉)) + 1) ∈
ℝ) | 
| 57 | 55, 56 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ) | 
| 58 | 15 | rphalfcld 13089 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈
ℝ+) | 
| 59 | 58, 30 | rpmulcld 13093 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈
ℝ+) | 
| 60 | 59 | rpred 13077 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ) | 
| 61 | 60, 45 | readdcld 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ) | 
| 62 |  | rpdivcl 13060 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((4
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (4 /
(𝐿 · 𝐸)) ∈
ℝ+) | 
| 63 | 18, 15, 62 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈
ℝ+) | 
| 64 | 63 | rpred 13077 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ) | 
| 65 | 28 | rpsqrtcld 15450 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (√‘𝑍) ∈
ℝ+) | 
| 66 | 65 | rpred 13077 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (√‘𝑍) ∈
ℝ) | 
| 67 | 27 | simp3d 1145 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 68 | 67 | simp1d 1143 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍)) | 
| 69 | 43 | rpred 13077 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ) | 
| 70 | 13 | simp2d 1144 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐾 ∈
ℝ+) | 
| 71 |  | pntlem1.j | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁)) | 
| 72 |  | elfzoelz 13699 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ) | 
| 73 | 71, 72 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 74 | 73 | peano2zd 12725 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐽 + 1) ∈ ℤ) | 
| 75 | 70, 74 | rpexpcld 14286 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈
ℝ+) | 
| 76 | 75 | rpred 13077 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ) | 
| 77 |  | pntlem1.V | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 78 | 77 | simplrd 770 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) | 
| 79 | 70 | rpcnd 13079 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐾 ∈ ℂ) | 
| 80 | 70, 73 | rpexpcld 14286 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (𝐾↑𝐽) ∈
ℝ+) | 
| 81 | 80 | rpcnd 13079 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ) | 
| 82 | 79, 81 | mulcomd 11282 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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 27642 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀))) | 
| 86 | 85 | simp1d 1143 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 87 |  | elfzouz 13703 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ≥‘𝑀)) | 
| 88 | 71, 87 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑀)) | 
| 89 |  | eluznn 12960 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈
(ℤ≥‘𝑀)) → 𝐽 ∈ ℕ) | 
| 90 | 86, 88, 89 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐽 ∈ ℕ) | 
| 91 | 90 | nnnn0d 12587 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐽 ∈
ℕ0) | 
| 92 | 79, 91 | expp1d 14187 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾)) | 
| 93 | 82, 92 | eqtr4d 2780 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1))) | 
| 94 | 78, 93 | breqtrd 5169 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1))) | 
| 95 | 69, 76, 94 | ltled 11409 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1))) | 
| 96 |  | fzofzp1 13803 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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 27643 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))) | 
| 99 | 97, 98 | mpdan 687 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))) | 
| 100 | 99 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)) | 
| 101 | 69, 76, 66, 95, 100 | letrd 11418 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍)) | 
| 102 | 69, 66, 65 | lemul2d 13121 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))) | 
| 103 | 101, 102 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))) | 
| 104 | 28 | rprege0d 13084 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍)) | 
| 105 |  | remsqsqrt 15295 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍) ·
(√‘𝑍)) = 𝑍) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍) | 
| 107 | 103, 106 | breqtrd 5169 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍) | 
| 108 | 28 | rpred 13077 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑍 ∈ ℝ) | 
| 109 | 66, 108, 43 | lemuldivd 13126 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) | 
| 110 | 107, 109 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 111 | 29 | rpcnd 13079 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑉 ∈ ℂ) | 
| 112 | 111 | mullidd 11279 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 · 𝑉) = 𝑉) | 
| 113 |  | 1red 11262 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 ∈
ℝ) | 
| 114 | 42 | rpred 13077 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ) | 
| 115 |  | 1re 11261 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℝ | 
| 116 |  | ltaddrp 13072 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℝ ∧ (𝐿
· 𝐸) ∈
ℝ+) → 1 < (1 + (𝐿 · 𝐸))) | 
| 117 | 115, 15, 116 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 < (1 + (𝐿 · 𝐸))) | 
| 118 | 113, 114,
29, 117 | ltmul1dd 13132 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 · 𝑉) < ((1 + (𝐿 · 𝐸)) · 𝑉)) | 
| 119 | 112, 118 | eqbrtrrd 5167 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉)) | 
| 120 | 29, 43, 28 | ltdiv2d 13100 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉) ↔ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉))) | 
| 121 | 119, 120 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉)) | 
| 122 | 45, 31, 121 | ltled 11409 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) | 
| 123 | 66, 45, 31, 110, 122 | letrd 11418 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑉)) | 
| 124 | 64, 66, 31, 68, 123 | letrd 11418 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (𝑍 / 𝑉)) | 
| 125 | 64, 31, 31, 124 | leadd2dd 11878 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ ((𝑍 / 𝑉) + (𝑍 / 𝑉))) | 
| 126 | 30 | rpcnd 13079 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℂ) | 
| 127 | 126 | 2timesd 12509 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (𝑍 / 𝑉)) = ((𝑍 / 𝑉) + (𝑍 / 𝑉))) | 
| 128 | 125, 127 | breqtrrd 5171 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉))) | 
| 129 | 31, 64 | readdcld 11290 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ∈ ℝ) | 
| 130 |  | 2re 12340 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ | 
| 131 |  | remulcl 11240 | . . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ (𝑍 /
𝑉) ∈ ℝ) →
(2 · (𝑍 / 𝑉)) ∈
ℝ) | 
| 132 | 130, 31, 131 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 · (𝑍 / 𝑉)) ∈ ℝ) | 
| 133 | 129, 132,
20 | lemul2d 13121 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))) | 
| 134 | 128, 133 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))) | 
| 135 | 20 | rpcnd 13079 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℂ) | 
| 136 | 63 | rpcnd 13079 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℂ) | 
| 137 | 135, 126,
136 | adddid 11285 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))))) | 
| 138 | 15 | rpcnne0d 13086 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0)) | 
| 139 |  | rpcnne0 13053 | . . . . . . . . . . . . . . . . . . 19
⊢ (4 ∈
ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0)) | 
| 140 | 18, 139 | mp1i 13 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (4 ∈ ℂ ∧ 4
≠ 0)) | 
| 141 |  | divcan6 11974 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0) ∧ (4 ∈ ℂ ∧ 4
≠ 0)) → (((𝐿
· 𝐸) / 4) ·
(4 / (𝐿 · 𝐸))) = 1) | 
| 142 | 138, 140,
141 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1) | 
| 143 | 142 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1)) | 
| 144 | 137, 143 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1)) | 
| 145 |  | 2cnd 12344 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℂ) | 
| 146 | 135, 145,
126 | mulassd 11284 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))) | 
| 147 | 15 | rpcnd 13079 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℂ) | 
| 148 |  | 2rp 13039 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ+ | 
| 149 |  | rpcnne0 13053 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0)) | 
| 150 | 148, 149 | mp1i 13 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 ∈ ℂ ∧ 2
≠ 0)) | 
| 151 |  | divdiv1 11978 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (2 ∈ ℂ
∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2))) | 
| 152 | 147, 150,
150, 151 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2))) | 
| 153 |  | 2t2e4 12430 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 2) = 4 | 
| 154 | 153 | oveq2i 7442 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 · 𝐸) / (2 · 2)) = ((𝐿 · 𝐸) / 4) | 
| 155 | 152, 154 | eqtr2di 2794 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) = (((𝐿 · 𝐸) / 2) / 2)) | 
| 156 | 155 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((((𝐿 · 𝐸) / 2) / 2) · 2)) | 
| 157 | 147 | halfcld 12511 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℂ) | 
| 158 | 150 | simprd 495 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 2 ≠ 0) | 
| 159 | 157, 145,
158 | divcan1d 12044 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) / 2) · 2) = ((𝐿 · 𝐸) / 2)) | 
| 160 | 156, 159 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((𝐿 · 𝐸) / 2)) | 
| 161 | 160 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉))) | 
| 162 | 146, 161 | eqtr3d 2779 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉))) | 
| 163 | 134, 144,
162 | 3brtr3d 5174 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ≤ (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉))) | 
| 164 |  | flle 13839 | . . . . . . . . . . . . . . 15
⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ →
(⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 165 | 45, 164 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) | 
| 166 | 52, 47, 60, 45, 163, 165 | le2addd 11882 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ≤ ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) | 
| 167 | 58 | rpred 13077 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ) | 
| 168 | 42 | rprecred 13088 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℝ) | 
| 169 | 167, 168 | readdcld 11290 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) ∈ ℝ) | 
| 170 | 15 | rpred 13077 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ) | 
| 171 | 14 | rpred 13077 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 172 | 8 | rpred 13077 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐿 ∈ ℝ) | 
| 173 |  | eliooord 13446 | . . . . . . . . . . . . . . . . . . . . . . . . 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 13132 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸)) | 
| 177 | 14 | rpcnd 13079 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 178 | 177 | mullidd 11279 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1 · 𝐸) = 𝐸) | 
| 179 | 176, 178 | breqtrd 5169 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸) | 
| 180 | 13 | simp3d 1145 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+)) | 
| 181 | 180 | simp1d 1143 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) | 
| 182 |  | eliooord 13446 | . . . . . . . . . . . . . . . . . . . . . . 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 11422 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 · 𝐸) < 1) | 
| 186 | 170, 113,
113, 185 | ltadd2dd 11420 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1)) | 
| 187 |  | df-2 12329 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 = (1 +
1) | 
| 188 | 186, 187 | breqtrrdi 5185 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2) | 
| 189 | 42 | rpregt0d 13083 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸)))) | 
| 190 | 130 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 2 ∈
ℝ) | 
| 191 |  | 2pos 12369 | . . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 | 
| 192 | 191 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 2) | 
| 193 | 15 | rpregt0d 13083 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸))) | 
| 194 |  | ltdiv2 12154 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((1 +
(𝐿 · 𝐸)) ∈ ℝ ∧ 0 <
(1 + (𝐿 · 𝐸))) ∧ (2 ∈ ℝ
∧ 0 < 2) ∧ ((𝐿
· 𝐸) ∈ ℝ
∧ 0 < (𝐿 ·
𝐸))) → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))) | 
| 195 | 189, 190,
192, 193, 194 | syl121anc 1377 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))) | 
| 196 | 188, 195 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))) | 
| 197 | 42 | rpcnd 13079 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℂ) | 
| 198 | 42 | rpcnne0d 13086 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) | 
| 199 |  | divsubdir 11961 | . . . . . . . . . . . . . . . . . . 19
⊢ (((1 +
(𝐿 · 𝐸)) ∈ ℂ ∧ 1 ∈
ℂ ∧ ((1 + (𝐿
· 𝐸)) ∈ ℂ
∧ (1 + (𝐿 ·
𝐸)) ≠ 0)) → (((1 +
(𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸))))) | 
| 200 | 197, 49, 198, 199 | syl3anc 1373 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸))))) | 
| 201 |  | ax-1cn 11213 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℂ | 
| 202 |  | pncan2 11515 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℂ ∧ (𝐿
· 𝐸) ∈ ℂ)
→ ((1 + (𝐿 ·
𝐸)) − 1) = (𝐿 · 𝐸)) | 
| 203 | 201, 147,
202 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸)) | 
| 204 | 203 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))) | 
| 205 |  | divid 11953 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((1 +
(𝐿 · 𝐸)) ∈ ℂ ∧ (1 +
(𝐿 · 𝐸)) ≠ 0) → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1) | 
| 206 | 198, 205 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1) | 
| 207 | 206 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))) = (1 − (1 / (1 + (𝐿 · 𝐸))))) | 
| 208 | 200, 204,
207 | 3eqtr3d 2785 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))) = (1 − (1 / (1 + (𝐿 · 𝐸))))) | 
| 209 | 196, 208 | breqtrd 5169 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸))))) | 
| 210 | 167, 168,
113 | ltaddsubd 11863 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1 ↔ ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸)))))) | 
| 211 | 209, 210 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1) | 
| 212 | 169, 113,
30, 211 | ltmul1dd 13132 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) < (1 · (𝑍 / 𝑉))) | 
| 213 |  | reccl 11929 | . . . . . . . . . . . . . . . . 17
⊢ (((1 +
(𝐿 · 𝐸)) ∈ ℂ ∧ (1 +
(𝐿 · 𝐸)) ≠ 0) → (1 / (1 +
(𝐿 · 𝐸))) ∈
ℂ) | 
| 214 | 198, 213 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ) | 
| 215 | 157, 214,
126 | adddird 11286 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))) | 
| 216 | 197, 111 | mulcomd 11282 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) = (𝑉 · (1 + (𝐿 · 𝐸)))) | 
| 217 | 216 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸))))) | 
| 218 | 28 | rpcnd 13079 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑍 ∈ ℂ) | 
| 219 | 29 | rpcnne0d 13086 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0)) | 
| 220 |  | divdiv1 11978 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑍 ∈ ℂ ∧ (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸))))) | 
| 221 | 218, 219,
198, 220 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸))))) | 
| 222 | 42 | rpne0d 13082 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≠ 0) | 
| 223 | 126, 197,
222 | divrec2d 12047 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))) | 
| 224 | 217, 221,
223 | 3eqtr2d 2783 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))) | 
| 225 | 224 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))) | 
| 226 | 215, 225 | eqtr4d 2780 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) | 
| 227 | 126 | mullidd 11279 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1 · (𝑍 / 𝑉)) = (𝑍 / 𝑉)) | 
| 228 | 212, 226,
227 | 3brtr3d 5174 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) < (𝑍 / 𝑉)) | 
| 229 | 53, 61, 31, 166, 228 | lelttrd 11419 | . . . . . . . . . . . 12
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (𝑍 / 𝑉)) | 
| 230 |  | fllep1 13841 | . . . . . . . . . . . . 13
⊢ ((𝑍 / 𝑉) ∈ ℝ → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1)) | 
| 231 | 31, 230 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1)) | 
| 232 | 53, 31, 57, 229, 231 | ltletrd 11421 | . . . . . . . . . . 11
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < ((⌊‘(𝑍 / 𝑉)) + 1)) | 
| 233 | 50, 232 | eqbrtrd 5165 | . . . . . . . . . 10
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1)) | 
| 234 | 32, 47 | readdcld 11290 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ) | 
| 235 | 234, 55, 113 | ltadd1d 11856 | . . . . . . . . . 10
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1))) | 
| 236 | 233, 235 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉))) | 
| 237 | 32, 47, 55 | ltaddsubd 11863 | . . . . . . . . 9
⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))) | 
| 238 | 236, 237 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) | 
| 239 | 31 | flcld 13838 | . . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ) | 
| 240 |  | fzval3 13773 | . . . . . . . . . . . 12
⊢
((⌊‘(𝑍 /
𝑉)) ∈ ℤ →
(((⌊‘(𝑍 / ((1 +
(𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) | 
| 241 | 239, 240 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) | 
| 242 | 33, 241 | eqtrid 2789 | . . . . . . . . . 10
⊢ (𝜑 → 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) | 
| 243 | 242 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝜑 → (♯‘𝐼) =
(♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))) | 
| 244 |  | flword2 13853 | . . . . . . . . . . . 12
⊢ (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) → (⌊‘(𝑍 / 𝑉)) ∈
(ℤ≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) | 
| 245 | 45, 31, 122, 244 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈
(ℤ≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) | 
| 246 |  | eluzp1p1 12906 | . . . . . . . . . . 11
⊢
((⌊‘(𝑍 /
𝑉)) ∈
(ℤ≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) → ((⌊‘(𝑍 / 𝑉)) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) | 
| 247 | 245, 246 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈
(ℤ≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1))) | 
| 248 |  | hashfzo 14468 | . . . . . . . . . 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 11289 | . . . . . . . . . 10
⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℂ) | 
| 251 | 250, 48, 49 | pnpcan2d 11658 | . . . . . . . . 9
⊢ (𝜑 → (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) | 
| 252 | 243, 249,
251 | 3eqtrd 2781 | . . . . . . . 8
⊢ (𝜑 → (♯‘𝐼) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))) | 
| 253 | 238, 252 | breqtrrd 5171 | . . . . . . 7
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < (♯‘𝐼)) | 
| 254 | 32, 38, 253 | ltled 11409 | . . . . . 6
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼)) | 
| 255 | 21, 38, 30 | lemuldivd 13126 | . . . . . 6
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼) ↔ ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)))) | 
| 256 | 254, 255 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉))) | 
| 257 | 29 | rpred 13077 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉 ∈ ℝ) | 
| 258 | 69, 76, 66, 94, 100 | ltletrd 11421 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (√‘𝑍)) | 
| 259 | 257, 69, 66, 119, 258 | lttrd 11422 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑉 < (√‘𝑍)) | 
| 260 | 257, 66, 259 | ltled 11409 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ≤ (√‘𝑍)) | 
| 261 | 29 | rprege0d 13084 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉)) | 
| 262 | 65 | rprege0d 13084 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) | 
| 263 |  | le2sq 14174 | . . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ ℝ ∧ 0 ≤
𝑉) ∧
((√‘𝑍) ∈
ℝ ∧ 0 ≤ (√‘𝑍))) → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2))) | 
| 264 | 261, 262,
263 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2))) | 
| 265 | 260, 264 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑉↑2) ≤ ((√‘𝑍)↑2)) | 
| 266 |  | resqrtth 15294 | . . . . . . . . . . . . . 14
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍)↑2)
= 𝑍) | 
| 267 | 104, 266 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍) | 
| 268 | 265, 267 | breqtrd 5169 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑉↑2) ≤ 𝑍) | 
| 269 |  | 2z 12649 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ | 
| 270 |  | rpexpcl 14121 | . . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑉↑2) ∈
ℝ+) | 
| 271 | 29, 269, 270 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑉↑2) ∈
ℝ+) | 
| 272 | 271 | rpred 13077 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑉↑2) ∈ ℝ) | 
| 273 | 272, 108,
28 | lemul2d 13121 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑉↑2) ≤ 𝑍 ↔ (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍))) | 
| 274 | 268, 273 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍)) | 
| 275 | 218 | sqvald 14183 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍↑2) = (𝑍 · 𝑍)) | 
| 276 | 274, 275 | breqtrrd 5171 | . . . . . . . . . 10
⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍↑2)) | 
| 277 | 108 | resqcld 14165 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍↑2) ∈ ℝ) | 
| 278 | 108, 277,
271 | lemuldivd 13126 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑍 · (𝑉↑2)) ≤ (𝑍↑2) ↔ 𝑍 ≤ ((𝑍↑2) / (𝑉↑2)))) | 
| 279 | 276, 278 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → 𝑍 ≤ ((𝑍↑2) / (𝑉↑2))) | 
| 280 | 29 | rpne0d 13082 | . . . . . . . . . 10
⊢ (𝜑 → 𝑉 ≠ 0) | 
| 281 | 218, 111,
280 | sqdivd 14199 | . . . . . . . . 9
⊢ (𝜑 → ((𝑍 / 𝑉)↑2) = ((𝑍↑2) / (𝑉↑2))) | 
| 282 | 279, 281 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝜑 → 𝑍 ≤ ((𝑍 / 𝑉)↑2)) | 
| 283 |  | rpexpcl 14121 | . . . . . . . . . 10
⊢ (((𝑍 / 𝑉) ∈ ℝ+ ∧ 2 ∈
ℤ) → ((𝑍 / 𝑉)↑2) ∈
ℝ+) | 
| 284 | 30, 269, 283 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → ((𝑍 / 𝑉)↑2) ∈
ℝ+) | 
| 285 | 28, 284 | logled 26669 | . . . . . . . 8
⊢ (𝜑 → (𝑍 ≤ ((𝑍 / 𝑉)↑2) ↔ (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2)))) | 
| 286 | 282, 285 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2))) | 
| 287 |  | relogexp 26638 | . . . . . . . 8
⊢ (((𝑍 / 𝑉) ∈ ℝ+ ∧ 2 ∈
ℤ) → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉)))) | 
| 288 | 30, 269, 287 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉)))) | 
| 289 | 286, 288 | breqtrd 5169 | . . . . . 6
⊢ (𝜑 → (log‘𝑍) ≤ (2 ·
(log‘(𝑍 / 𝑉)))) | 
| 290 | 28 | relogcld 26665 | . . . . . . 7
⊢ (𝜑 → (log‘𝑍) ∈
ℝ) | 
| 291 | 30 | relogcld 26665 | . . . . . . 7
⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ) | 
| 292 |  | ledivmul 12144 | . . . . . . 7
⊢
(((log‘𝑍)
∈ ℝ ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))) | 
| 293 | 290, 291,
190, 192, 292 | syl112anc 1376 | . . . . . 6
⊢ (𝜑 → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))) | 
| 294 | 289, 293 | mpbird 257 | . . . . 5
⊢ (𝜑 → ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) | 
| 295 | 20 | rprege0d 13084 | . . . . . 6
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4))) | 
| 296 | 38, 30 | rerpdivcld 13108 | . . . . . 6
⊢ (𝜑 → ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ) | 
| 297 | 27 | simp2d 1144 | . . . . . . . . . 10
⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌))) | 
| 298 | 297 | simp1d 1143 | . . . . . . . . 9
⊢ (𝜑 → 1 < 𝑍) | 
| 299 | 108, 298 | rplogcld 26671 | . . . . . . . 8
⊢ (𝜑 → (log‘𝑍) ∈
ℝ+) | 
| 300 | 299 | rphalfcld 13089 | . . . . . . 7
⊢ (𝜑 → ((log‘𝑍) / 2) ∈
ℝ+) | 
| 301 | 300 | rprege0d 13084 | . . . . . 6
⊢ (𝜑 → (((log‘𝑍) / 2) ∈ ℝ ∧ 0
≤ ((log‘𝑍) /
2))) | 
| 302 |  | lemul12a 12125 | . . . . . 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 839 | . . . . 5
⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤
(((♯‘𝐼) /
(𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))) | 
| 304 | 256, 294,
303 | mp2and 699 | . . . 4
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤
(((♯‘𝐼) /
(𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))) | 
| 305 | 299 | rpcnd 13079 | . . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℂ) | 
| 306 |  | 8nn 12361 | . . . . . . . 8
⊢ 8 ∈
ℕ | 
| 307 |  | nnrp 13046 | . . . . . . . 8
⊢ (8 ∈
ℕ → 8 ∈ ℝ+) | 
| 308 | 306, 307 | ax-mp 5 | . . . . . . 7
⊢ 8 ∈
ℝ+ | 
| 309 |  | rpcnne0 13053 | . . . . . . 7
⊢ (8 ∈
ℝ+ → (8 ∈ ℂ ∧ 8 ≠ 0)) | 
| 310 | 308, 309 | mp1i 13 | . . . . . 6
⊢ (𝜑 → (8 ∈ ℂ ∧ 8
≠ 0)) | 
| 311 |  | div23 11941 | . . . . . 6
⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ (8 ∈
ℂ ∧ 8 ≠ 0)) → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍))) | 
| 312 | 147, 305,
310, 311 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍))) | 
| 313 |  | divmuldiv 11967 | . . . . . . 7
⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ) ∧ ((4
∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) →
(((𝐿 · 𝐸) / 4) ·
((log‘𝑍) / 2)) =
(((𝐿 · 𝐸) · (log‘𝑍)) / (4 ·
2))) | 
| 314 | 147, 305,
140, 150, 313 | syl22anc 839 | . . . . . 6
⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2))) | 
| 315 |  | 4t2e8 12434 | . . . . . . 7
⊢ (4
· 2) = 8 | 
| 316 | 315 | oveq2i 7442 | . . . . . 6
⊢ (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / 8) | 
| 317 | 314, 316 | eqtr2di 2794 | . . . . 5
⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2))) | 
| 318 | 312, 317 | eqtr3d 2779 | . . . 4
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2))) | 
| 319 | 38 | recnd 11289 | . . . . 5
⊢ (𝜑 → (♯‘𝐼) ∈
ℂ) | 
| 320 | 291 | recnd 11289 | . . . . 5
⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℂ) | 
| 321 | 30 | rpcnne0d 13086 | . . . . 5
⊢ (𝜑 → ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) | 
| 322 |  | divass 11940 | . . . . . 6
⊢
(((♯‘𝐼)
∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) | 
| 323 |  | div23 11941 | . . . . . 6
⊢
(((♯‘𝐼)
∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))) | 
| 324 | 322, 323 | eqtr3d 2779 | . . . . 5
⊢
(((♯‘𝐼)
∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))) | 
| 325 | 319, 320,
321, 324 | syl3anc 1373 | . . . 4
⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))) | 
| 326 | 304, 318,
325 | 3brtr4d 5175 | . . 3
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) | 
| 327 |  | rpdivcl 13060 | . . . . . . 7
⊢ (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈
ℝ+) → ((𝐿 · 𝐸) / 8) ∈
ℝ+) | 
| 328 | 15, 308, 327 | sylancl 586 | . . . . . 6
⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈
ℝ+) | 
| 329 | 328, 299 | rpmulcld 13093 | . . . . 5
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈
ℝ+) | 
| 330 | 329 | rpred 13077 | . . . 4
⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ) | 
| 331 | 291, 30 | rerpdivcld 13108 | . . . . 5
⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ) | 
| 332 | 38, 331 | remulcld 11291 | . . . 4
⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ) | 
| 333 | 180 | simp3d 1145 | . . . 4
⊢ (𝜑 → (𝑈 − 𝐸) ∈
ℝ+) | 
| 334 | 330, 332,
333 | lemul2d 13121 | . . 3
⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ↔ ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))) | 
| 335 | 326, 334 | mpbid 232 | . 2
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) | 
| 336 | 333 | rpcnd 13079 | . . 3
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ) | 
| 337 | 331 | recnd 11289 | . . 3
⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℂ) | 
| 338 | 336, 319,
337 | mul12d 11470 | . 2
⊢ (𝜑 → ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) | 
| 339 | 335, 338 | breqtrd 5169 | 1
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))) |