Proof of Theorem pntlemb
Step | Hyp | Ref
| Expression |
1 | | pntlem1.z |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) |
2 | | pntlem1.r |
. . . . . . . 8
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
3 | | pntlem1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
4 | | pntlem1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
5 | | pntlem1.l |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) |
6 | | pntlem1.d |
. . . . . . . 8
⊢ 𝐷 = (𝐴 + 1) |
7 | | pntlem1.f |
. . . . . . . 8
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) |
8 | | pntlem1.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈
ℝ+) |
9 | | pntlem1.u2 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ≤ 𝐴) |
10 | | pntlem1.e |
. . . . . . . 8
⊢ 𝐸 = (𝑈 / 𝐷) |
11 | | pntlem1.k |
. . . . . . . 8
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) |
12 | | pntlem1.y |
. . . . . . . 8
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) |
13 | | pntlem1.x |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) |
14 | | pntlem1.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
15 | | pntlem1.w |
. . . . . . . 8
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) |
16 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | pntlema 25285 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈
ℝ+) |
17 | 16 | rpred 11872 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ ℝ) |
18 | | pnfxr 10092 |
. . . . . 6
⊢ +∞
∈ ℝ* |
19 | | elico2 12237 |
. . . . . 6
⊢ ((𝑊 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑍 ∈ (𝑊[,)+∞) ↔ (𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞))) |
20 | 17, 18, 19 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (𝑍 ∈ (𝑊[,)+∞) ↔ (𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞))) |
21 | 1, 20 | mpbid 222 |
. . . 4
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞)) |
22 | 21 | simp1d 1073 |
. . 3
⊢ (𝜑 → 𝑍 ∈ ℝ) |
23 | 21 | simp2d 1074 |
. . 3
⊢ (𝜑 → 𝑊 ≤ 𝑍) |
24 | 22, 16, 23 | rpgecld 11911 |
. 2
⊢ (𝜑 → 𝑍 ∈
ℝ+) |
25 | | 1re 10039 |
. . . . . . 7
⊢ 1 ∈
ℝ |
26 | 25 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
27 | | ere 14819 |
. . . . . . 7
⊢ e ∈
ℝ |
28 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → e ∈
ℝ) |
29 | 24 | rpsqrtcld 14150 |
. . . . . . 7
⊢ (𝜑 → (√‘𝑍) ∈
ℝ+) |
30 | 29 | rpred 11872 |
. . . . . 6
⊢ (𝜑 → (√‘𝑍) ∈
ℝ) |
31 | | 1lt2 11194 |
. . . . . . . 8
⊢ 1 <
2 |
32 | | egt2lt3 14934 |
. . . . . . . . 9
⊢ (2 < e
∧ e < 3) |
33 | 32 | simpli 474 |
. . . . . . . 8
⊢ 2 <
e |
34 | | 2re 11090 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
35 | 25, 34, 27 | lttri 10163 |
. . . . . . . 8
⊢ ((1 <
2 ∧ 2 < e) → 1 < e) |
36 | 31, 33, 35 | mp2an 708 |
. . . . . . 7
⊢ 1 <
e |
37 | 36 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 < e) |
38 | | 4re 11097 |
. . . . . . . 8
⊢ 4 ∈
ℝ |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 4 ∈
ℝ) |
40 | 32 | simpri 478 |
. . . . . . . . 9
⊢ e <
3 |
41 | | 3lt4 11197 |
. . . . . . . . 9
⊢ 3 <
4 |
42 | | 3re 11094 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
43 | 27, 42, 38 | lttri 10163 |
. . . . . . . . 9
⊢ ((e <
3 ∧ 3 < 4) → e < 4) |
44 | 40, 41, 43 | mp2an 708 |
. . . . . . . 8
⊢ e <
4 |
45 | 44 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → e < 4) |
46 | | 4nn 11187 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ |
47 | | nnrp 11842 |
. . . . . . . . . . 11
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ+ |
49 | 2, 3, 4, 5, 6, 7 | pntlemd 25283 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+
∧ 𝐹 ∈
ℝ+)) |
50 | 49 | simp1d 1073 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈
ℝ+) |
51 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | pntlemc 25284 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) |
52 | 51 | simp1d 1073 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
53 | 50, 52 | rpmulcld 11888 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 · 𝐸) ∈
ℝ+) |
54 | | rpdivcl 11856 |
. . . . . . . . . 10
⊢ ((4
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (4 /
(𝐿 · 𝐸)) ∈
ℝ+) |
55 | 48, 53, 54 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈
ℝ+) |
56 | 55 | rpred 11872 |
. . . . . . . 8
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ) |
57 | 53 | rpred 11872 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ) |
58 | 52 | rpred 11872 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℝ) |
59 | 50 | rpred 11872 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ ℝ) |
60 | | eliooord 12233 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 ∈ (0(,)1) → (0 <
𝐿 ∧ 𝐿 < 1)) |
61 | 5, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1)) |
62 | 61 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 < 1) |
63 | 59, 26, 52, 62 | ltmul1dd 11927 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸)) |
64 | 52 | rpcnd 11874 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℂ) |
65 | 64 | mulid2d 10058 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 · 𝐸) = 𝐸) |
66 | 63, 65 | breqtrd 4679 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸) |
67 | 51 | simp3d 1075 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+)) |
68 | 67 | simp1d 1073 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
69 | | eliooord 12233 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
71 | 70 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 < 1) |
72 | 57, 58, 26, 66, 71 | lttrd 10198 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿 · 𝐸) < 1) |
73 | | 4pos 11116 |
. . . . . . . . . . . . 13
⊢ 0 <
4 |
74 | 39, 73 | jctir 561 |
. . . . . . . . . . . 12
⊢ (𝜑 → (4 ∈ ℝ ∧ 0
< 4)) |
75 | | ltmul2 10874 |
. . . . . . . . . . . 12
⊢ (((𝐿 · 𝐸) ∈ ℝ ∧ 1 ∈ ℝ
∧ (4 ∈ ℝ ∧ 0 < 4)) → ((𝐿 · 𝐸) < 1 ↔ (4 · (𝐿 · 𝐸)) < (4 · 1))) |
76 | 57, 26, 74, 75 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 · 𝐸) < 1 ↔ (4 · (𝐿 · 𝐸)) < (4 · 1))) |
77 | 72, 76 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (4 · (𝐿 · 𝐸)) < (4 · 1)) |
78 | | 4cn 11098 |
. . . . . . . . . . 11
⊢ 4 ∈
ℂ |
79 | 78 | mulid1i 10042 |
. . . . . . . . . 10
⊢ (4
· 1) = 4 |
80 | 77, 79 | syl6breq 4694 |
. . . . . . . . 9
⊢ (𝜑 → (4 · (𝐿 · 𝐸)) < 4) |
81 | 39, 39, 53 | ltmuldivd 11919 |
. . . . . . . . 9
⊢ (𝜑 → ((4 · (𝐿 · 𝐸)) < 4 ↔ 4 < (4 / (𝐿 · 𝐸)))) |
82 | 80, 81 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → 4 < (4 / (𝐿 · 𝐸))) |
83 | 12 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℝ+) |
84 | 83, 55 | rpaddcld 11887 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 + (4 / (𝐿 · 𝐸))) ∈
ℝ+) |
85 | 84 | rpred 11872 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 + (4 / (𝐿 · 𝐸))) ∈ ℝ) |
86 | 56, 83 | ltaddrp2d 11906 |
. . . . . . . . 9
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) < (𝑌 + (4 / (𝐿 · 𝐸)))) |
87 | 85 | resqcld 13035 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) ∈ ℝ) |
88 | 13 | simpld 475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈
ℝ+) |
89 | 51 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈
ℝ+) |
90 | | 2z 11409 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℤ |
91 | | rpexpcl 12879 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝐾↑2) ∈
ℝ+) |
92 | 89, 90, 91 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾↑2) ∈
ℝ+) |
93 | 88, 92 | rpmulcld 11888 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 · (𝐾↑2)) ∈
ℝ+) |
94 | | 4z 11411 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℤ |
95 | | rpexpcl 12879 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 · (𝐾↑2)) ∈ ℝ+ ∧ 4
∈ ℤ) → ((𝑋
· (𝐾↑2))↑4) ∈
ℝ+) |
96 | 93, 94, 95 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑋 · (𝐾↑2))↑4) ∈
ℝ+) |
97 | | 3nn0 11310 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℕ0 |
98 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℕ |
99 | 97, 98 | decnncl 11518 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ;32 ∈ ℕ |
100 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (;32 ∈ ℕ → ;32 ∈
ℝ+) |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ;32 ∈
ℝ+ |
102 | | rpmulcl 11855 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((;32 ∈ ℝ+ ∧
𝐵 ∈
ℝ+) → (;32
· 𝐵) ∈
ℝ+) |
103 | 101, 4, 102 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (;32 · 𝐵) ∈
ℝ+) |
104 | 67 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 − 𝐸) ∈
ℝ+) |
105 | | rpexpcl 12879 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝐸↑2) ∈
ℝ+) |
106 | 52, 90, 105 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸↑2) ∈
ℝ+) |
107 | 50, 106 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 · (𝐸↑2)) ∈
ℝ+) |
108 | 104, 107 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ∈
ℝ+) |
109 | 103, 108 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) ∈
ℝ+) |
110 | | 3nn 11186 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 3 ∈
ℕ |
111 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (3 ∈
ℕ → 3 ∈ ℝ+) |
112 | 110, 111 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
ℝ+ |
113 | | rpmulcl 11855 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ ℝ+
∧ 3 ∈ ℝ+) → (𝑈 · 3) ∈
ℝ+) |
114 | 8, 112, 113 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 · 3) ∈
ℝ+) |
115 | 114, 14 | rpaddcld 11887 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ∈
ℝ+) |
116 | 109, 115 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) ∈
ℝ+) |
117 | 116 | rpred 11872 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) ∈ ℝ) |
118 | 117 | rpefcld 14835 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) ∈
ℝ+) |
119 | 96, 118 | rpaddcld 11887 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) ∈
ℝ+) |
120 | 87, 119 | ltaddrpd 11905 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))) |
121 | 120, 15 | syl6breqr 4695 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < 𝑊) |
122 | 87, 17, 22, 121, 23 | ltletrd 10197 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < 𝑍) |
123 | 24 | rprege0d 11879 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍)) |
124 | | resqrtth 13996 |
. . . . . . . . . . . 12
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍)↑2)
= 𝑍) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍) |
126 | 122, 125 | breqtrrd 4681 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < ((√‘𝑍)↑2)) |
127 | 84 | rprege0d 11879 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸))) ∈ ℝ ∧ 0 ≤ (𝑌 + (4 / (𝐿 · 𝐸))))) |
128 | 29 | rprege0d 11879 |
. . . . . . . . . . 11
⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) |
129 | | lt2sq 12937 |
. . . . . . . . . . 11
⊢ ((((𝑌 + (4 / (𝐿 · 𝐸))) ∈ ℝ ∧ 0 ≤ (𝑌 + (4 / (𝐿 · 𝐸)))) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) →
((𝑌 + (4 / (𝐿 · 𝐸))) < (√‘𝑍) ↔ ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < ((√‘𝑍)↑2))) |
130 | 127, 128,
129 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸))) < (√‘𝑍) ↔ ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < ((√‘𝑍)↑2))) |
131 | 126, 130 | mpbird 247 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 + (4 / (𝐿 · 𝐸))) < (√‘𝑍)) |
132 | 56, 85, 30, 86, 131 | lttrd 10198 |
. . . . . . . 8
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) < (√‘𝑍)) |
133 | 39, 56, 30, 82, 132 | lttrd 10198 |
. . . . . . 7
⊢ (𝜑 → 4 <
(√‘𝑍)) |
134 | 28, 39, 30, 45, 133 | lttrd 10198 |
. . . . . 6
⊢ (𝜑 → e <
(√‘𝑍)) |
135 | 26, 28, 30, 37, 134 | lttrd 10198 |
. . . . 5
⊢ (𝜑 → 1 <
(√‘𝑍)) |
136 | | 0le1 10551 |
. . . . . . 7
⊢ 0 ≤
1 |
137 | 136 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 1) |
138 | | lt2sq 12937 |
. . . . . 6
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) →
(1 < (√‘𝑍)
↔ (1↑2) < ((√‘𝑍)↑2))) |
139 | 26, 137, 128, 138 | syl21anc 1325 |
. . . . 5
⊢ (𝜑 → (1 <
(√‘𝑍) ↔
(1↑2) < ((√‘𝑍)↑2))) |
140 | 135, 139 | mpbid 222 |
. . . 4
⊢ (𝜑 → (1↑2) <
((√‘𝑍)↑2)) |
141 | | sq1 12958 |
. . . . 5
⊢
(1↑2) = 1 |
142 | 141 | a1i 11 |
. . . 4
⊢ (𝜑 → (1↑2) =
1) |
143 | 140, 142,
125 | 3brtr3d 4684 |
. . 3
⊢ (𝜑 → 1 < 𝑍) |
144 | 28, 30, 134 | ltled 10185 |
. . 3
⊢ (𝜑 → e ≤
(√‘𝑍)) |
145 | 22, 83 | rerpdivcld 11903 |
. . . 4
⊢ (𝜑 → (𝑍 / 𝑌) ∈ ℝ) |
146 | 83 | rpred 11872 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) |
147 | 146, 55 | ltaddrpd 11905 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 < (𝑌 + (4 / (𝐿 · 𝐸)))) |
148 | 146, 85, 30, 147, 131 | lttrd 10198 |
. . . . . . 7
⊢ (𝜑 → 𝑌 < (√‘𝑍)) |
149 | 146, 30, 29, 148 | ltmul2dd 11928 |
. . . . . 6
⊢ (𝜑 → ((√‘𝑍) · 𝑌) < ((√‘𝑍) · (√‘𝑍))) |
150 | | remsqsqrt 13997 |
. . . . . . 7
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍) ·
(√‘𝑍)) = 𝑍) |
151 | 123, 150 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍) |
152 | 149, 151 | breqtrd 4679 |
. . . . 5
⊢ (𝜑 → ((√‘𝑍) · 𝑌) < 𝑍) |
153 | 30, 22, 83 | ltmuldivd 11919 |
. . . . 5
⊢ (𝜑 → (((√‘𝑍) · 𝑌) < 𝑍 ↔ (√‘𝑍) < (𝑍 / 𝑌))) |
154 | 152, 153 | mpbid 222 |
. . . 4
⊢ (𝜑 → (√‘𝑍) < (𝑍 / 𝑌)) |
155 | 30, 145, 154 | ltled 10185 |
. . 3
⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑌)) |
156 | 143, 144,
155 | 3jca 1242 |
. 2
⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌))) |
157 | 56, 30, 132 | ltled 10185 |
. . 3
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍)) |
158 | 88 | relogcld 24369 |
. . . . . 6
⊢ (𝜑 → (log‘𝑋) ∈
ℝ) |
159 | 89 | rpred 11872 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℝ) |
160 | 67 | simp2d 1074 |
. . . . . . 7
⊢ (𝜑 → 1 < 𝐾) |
161 | 159, 160 | rplogcld 24375 |
. . . . . 6
⊢ (𝜑 → (log‘𝐾) ∈
ℝ+) |
162 | 158, 161 | rerpdivcld 11903 |
. . . . 5
⊢ (𝜑 → ((log‘𝑋) / (log‘𝐾)) ∈ ℝ) |
163 | | readdcl 10019 |
. . . . 5
⊢
((((log‘𝑋) /
(log‘𝐾)) ∈
ℝ ∧ 2 ∈ ℝ) → (((log‘𝑋) / (log‘𝐾)) + 2) ∈ ℝ) |
164 | 162, 34, 163 | sylancl 694 |
. . . 4
⊢ (𝜑 → (((log‘𝑋) / (log‘𝐾)) + 2) ∈ ℝ) |
165 | 24 | relogcld 24369 |
. . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℝ) |
166 | 165, 161 | rerpdivcld 11903 |
. . . . 5
⊢ (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ) |
167 | | nndivre 11056 |
. . . . 5
⊢
((((log‘𝑍) /
(log‘𝐾)) ∈
ℝ ∧ 4 ∈ ℕ) → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ) |
168 | 166, 46, 167 | sylancl 694 |
. . . 4
⊢ (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ) |
169 | 93 | relogcld 24369 |
. . . . . 6
⊢ (𝜑 → (log‘(𝑋 · (𝐾↑2))) ∈ ℝ) |
170 | | nndivre 11056 |
. . . . . . 7
⊢
(((log‘𝑍)
∈ ℝ ∧ 4 ∈ ℕ) → ((log‘𝑍) / 4) ∈ ℝ) |
171 | 165, 46, 170 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → ((log‘𝑍) / 4) ∈
ℝ) |
172 | | relogexp 24342 |
. . . . . . . . 9
⊢ (((𝑋 · (𝐾↑2)) ∈ ℝ+ ∧ 4
∈ ℤ) → (log‘((𝑋 · (𝐾↑2))↑4)) = (4 ·
(log‘(𝑋 ·
(𝐾↑2))))) |
173 | 93, 94, 172 | sylancl 694 |
. . . . . . . 8
⊢ (𝜑 → (log‘((𝑋 · (𝐾↑2))↑4)) = (4 ·
(log‘(𝑋 ·
(𝐾↑2))))) |
174 | 96 | rpred 11872 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 · (𝐾↑2))↑4) ∈
ℝ) |
175 | 119 | rpred 11872 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) ∈ ℝ) |
176 | 174, 118 | ltaddrpd 11905 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 · (𝐾↑2))↑4) < (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) |
177 | | rpexpcl 12879 |
. . . . . . . . . . . . . 14
⊢ (((𝑌 + (4 / (𝐿 · 𝐸))) ∈ ℝ+ ∧ 2
∈ ℤ) → ((𝑌
+ (4 / (𝐿 · 𝐸)))↑2) ∈
ℝ+) |
178 | 84, 90, 177 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) ∈
ℝ+) |
179 | 175, 178 | ltaddrpd 11905 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) < ((((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) + ((𝑌 + (4 / (𝐿 · 𝐸)))↑2))) |
180 | 87 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) ∈ ℂ) |
181 | 119 | rpcnd 11874 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) ∈ ℂ) |
182 | 180, 181 | addcomd 10238 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) = ((((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) + ((𝑌 + (4 / (𝐿 · 𝐸)))↑2))) |
183 | 15, 182 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 = ((((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) + ((𝑌 + (4 / (𝐿 · 𝐸)))↑2))) |
184 | 179, 183 | breqtrrd 4681 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) < 𝑊) |
185 | 175, 17, 22, 184, 23 | ltletrd 10197 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) < 𝑍) |
186 | 174, 175,
22, 176, 185 | lttrd 10198 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 · (𝐾↑2))↑4) < 𝑍) |
187 | | logltb 24346 |
. . . . . . . . . 10
⊢ ((((𝑋 · (𝐾↑2))↑4) ∈ ℝ+
∧ 𝑍 ∈
ℝ+) → (((𝑋 · (𝐾↑2))↑4) < 𝑍 ↔ (log‘((𝑋 · (𝐾↑2))↑4)) < (log‘𝑍))) |
188 | 96, 24, 187 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) < 𝑍 ↔ (log‘((𝑋 · (𝐾↑2))↑4)) < (log‘𝑍))) |
189 | 186, 188 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → (log‘((𝑋 · (𝐾↑2))↑4)) < (log‘𝑍)) |
190 | 173, 189 | eqbrtrrd 4677 |
. . . . . . 7
⊢ (𝜑 → (4 ·
(log‘(𝑋 ·
(𝐾↑2)))) <
(log‘𝑍)) |
191 | | ltmuldiv2 10897 |
. . . . . . . 8
⊢
(((log‘(𝑋
· (𝐾↑2)))
∈ ℝ ∧ (log‘𝑍) ∈ ℝ ∧ (4 ∈ ℝ
∧ 0 < 4)) → ((4 · (log‘(𝑋 · (𝐾↑2)))) < (log‘𝑍) ↔ (log‘(𝑋 · (𝐾↑2))) < ((log‘𝑍) / 4))) |
192 | 169, 165,
74, 191 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → ((4 ·
(log‘(𝑋 ·
(𝐾↑2)))) <
(log‘𝑍) ↔
(log‘(𝑋 ·
(𝐾↑2))) <
((log‘𝑍) /
4))) |
193 | 190, 192 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → (log‘(𝑋 · (𝐾↑2))) < ((log‘𝑍) / 4)) |
194 | 169, 171,
161, 193 | ltdiv1dd 11929 |
. . . . 5
⊢ (𝜑 → ((log‘(𝑋 · (𝐾↑2))) / (log‘𝐾)) < (((log‘𝑍) / 4) / (log‘𝐾))) |
195 | 88, 92 | relogmuld 24371 |
. . . . . . . 8
⊢ (𝜑 → (log‘(𝑋 · (𝐾↑2))) = ((log‘𝑋) + (log‘(𝐾↑2)))) |
196 | | relogexp 24342 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℝ+
∧ 2 ∈ ℤ) → (log‘(𝐾↑2)) = (2 · (log‘𝐾))) |
197 | 89, 90, 196 | sylancl 694 |
. . . . . . . . 9
⊢ (𝜑 → (log‘(𝐾↑2)) = (2 ·
(log‘𝐾))) |
198 | 197 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝜑 → ((log‘𝑋) + (log‘(𝐾↑2))) = ((log‘𝑋) + (2 · (log‘𝐾)))) |
199 | 195, 198 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (log‘(𝑋 · (𝐾↑2))) = ((log‘𝑋) + (2 · (log‘𝐾)))) |
200 | 199 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((log‘(𝑋 · (𝐾↑2))) / (log‘𝐾)) = (((log‘𝑋) + (2 · (log‘𝐾))) / (log‘𝐾))) |
201 | 158 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (log‘𝑋) ∈
ℂ) |
202 | | 2cnd 11093 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) |
203 | 161 | rpcnd 11874 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝐾) ∈
ℂ) |
204 | 202, 203 | mulcld 10060 |
. . . . . . 7
⊢ (𝜑 → (2 ·
(log‘𝐾)) ∈
ℂ) |
205 | 161 | rpcnne0d 11881 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝐾) ∈ ℂ ∧
(log‘𝐾) ≠
0)) |
206 | | divdir 10710 |
. . . . . . 7
⊢
(((log‘𝑋)
∈ ℂ ∧ (2 · (log‘𝐾)) ∈ ℂ ∧ ((log‘𝐾) ∈ ℂ ∧
(log‘𝐾) ≠ 0))
→ (((log‘𝑋) + (2
· (log‘𝐾))) /
(log‘𝐾)) =
(((log‘𝑋) /
(log‘𝐾)) + ((2
· (log‘𝐾)) /
(log‘𝐾)))) |
207 | 201, 204,
205, 206 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (((log‘𝑋) + (2 · (log‘𝐾))) / (log‘𝐾)) = (((log‘𝑋) / (log‘𝐾)) + ((2 · (log‘𝐾)) / (log‘𝐾)))) |
208 | 205 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝐾) ≠ 0) |
209 | 202, 203,
208 | divcan4d 10807 |
. . . . . . 7
⊢ (𝜑 → ((2 ·
(log‘𝐾)) /
(log‘𝐾)) =
2) |
210 | 209 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (((log‘𝑋) / (log‘𝐾)) + ((2 · (log‘𝐾)) / (log‘𝐾))) = (((log‘𝑋) / (log‘𝐾)) + 2)) |
211 | 200, 207,
210 | 3eqtrd 2660 |
. . . . 5
⊢ (𝜑 → ((log‘(𝑋 · (𝐾↑2))) / (log‘𝐾)) = (((log‘𝑋) / (log‘𝐾)) + 2)) |
212 | 165 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℂ) |
213 | | rpcnne0 11850 |
. . . . . . 7
⊢ (4 ∈
ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0)) |
214 | 48, 213 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (4 ∈ ℂ ∧ 4
≠ 0)) |
215 | | divdiv32 10733 |
. . . . . 6
⊢
(((log‘𝑍)
∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((log‘𝐾) ∈ ℂ ∧
(log‘𝐾) ≠ 0))
→ (((log‘𝑍) / 4)
/ (log‘𝐾)) =
(((log‘𝑍) /
(log‘𝐾)) /
4)) |
216 | 212, 214,
205, 215 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (((log‘𝑍) / 4) / (log‘𝐾)) = (((log‘𝑍) / (log‘𝐾)) / 4)) |
217 | 194, 211,
216 | 3brtr3d 4684 |
. . . 4
⊢ (𝜑 → (((log‘𝑋) / (log‘𝐾)) + 2) < (((log‘𝑍) / (log‘𝐾)) / 4)) |
218 | 164, 168,
217 | ltled 10185 |
. . 3
⊢ (𝜑 → (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4)) |
219 | 115 | rpred 11872 |
. . . . 5
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ∈ ℝ) |
220 | 108, 103 | rpdivcld 11889 |
. . . . . . 7
⊢ (𝜑 → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) ∈
ℝ+) |
221 | 220 | rpred 11872 |
. . . . . 6
⊢ (𝜑 → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) ∈ ℝ) |
222 | 221, 165 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍)) ∈ ℝ) |
223 | 115 | rpcnd 11874 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ∈ ℂ) |
224 | 108 | rpcnne0d 11881 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ∈ ℂ ∧ ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ≠ 0)) |
225 | 103 | rpcnne0d 11881 |
. . . . . . . . 9
⊢ (𝜑 → ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) |
226 | | divdiv2 10737 |
. . . . . . . . 9
⊢ ((((𝑈 · 3) + 𝐶) ∈ ℂ ∧ (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ∈ ℂ ∧ ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ≠ 0) ∧ ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) → (((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) = ((((𝑈 · 3) + 𝐶) · (;32 · 𝐵)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))))) |
227 | 223, 224,
225, 226 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) = ((((𝑈 · 3) + 𝐶) · (;32 · 𝐵)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))))) |
228 | 103 | rpcnd 11874 |
. . . . . . . . . 10
⊢ (𝜑 → (;32 · 𝐵) ∈ ℂ) |
229 | 223, 228 | mulcomd 10061 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑈 · 3) + 𝐶) · (;32 · 𝐵)) = ((;32 · 𝐵) · ((𝑈 · 3) + 𝐶))) |
230 | 229 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑈 · 3) + 𝐶) · (;32 · 𝐵)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) = (((;32 · 𝐵) · ((𝑈 · 3) + 𝐶)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))))) |
231 | | div23 10704 |
. . . . . . . . 9
⊢ (((;32 · 𝐵) ∈ ℂ ∧ ((𝑈 · 3) + 𝐶) ∈ ℂ ∧ (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ∈ ℂ ∧ ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ≠ 0)) → (((;32 · 𝐵) · ((𝑈 · 3) + 𝐶)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) = (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) |
232 | 228, 223,
224, 231 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (((;32 · 𝐵) · ((𝑈 · 3) + 𝐶)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) = (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) |
233 | 227, 230,
232 | 3eqtrd 2660 |
. . . . . . 7
⊢ (𝜑 → (((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) = (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) |
234 | 117 | reefcld 14818 |
. . . . . . . . . 10
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) ∈ ℝ) |
235 | 234, 96 | ltaddrp2d 11906 |
. . . . . . . . . 10
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) |
236 | 234, 175,
22, 235, 185 | lttrd 10198 |
. . . . . . . . 9
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < 𝑍) |
237 | 24 | reeflogd 24370 |
. . . . . . . . 9
⊢ (𝜑 →
(exp‘(log‘𝑍)) =
𝑍) |
238 | 236, 237 | breqtrrd 4681 |
. . . . . . . 8
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < (exp‘(log‘𝑍))) |
239 | | eflt 14847 |
. . . . . . . . 9
⊢
(((((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) ∈ ℝ ∧ (log‘𝑍) ∈ ℝ) →
((((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) < (log‘𝑍) ↔ (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < (exp‘(log‘𝑍)))) |
240 | 117, 165,
239 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) < (log‘𝑍) ↔ (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < (exp‘(log‘𝑍)))) |
241 | 238, 240 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) < (log‘𝑍)) |
242 | 233, 241 | eqbrtrd 4675 |
. . . . . 6
⊢ (𝜑 → (((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) < (log‘𝑍)) |
243 | 219, 165,
220 | ltdivmuld 11923 |
. . . . . 6
⊢ (𝜑 → ((((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) < (log‘𝑍) ↔ ((𝑈 · 3) + 𝐶) < ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍)))) |
244 | 242, 243 | mpbid 222 |
. . . . 5
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) < ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍))) |
245 | 219, 222,
244 | ltled 10185 |
. . . 4
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ≤ ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍))) |
246 | 104 | rpcnd 11874 |
. . . . . 6
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ) |
247 | 107 | rpcnd 11874 |
. . . . . 6
⊢ (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℂ) |
248 | | divass 10703 |
. . . . . 6
⊢ (((𝑈 − 𝐸) ∈ ℂ ∧ (𝐿 · (𝐸↑2)) ∈ ℂ ∧ ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) = ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)))) |
249 | 246, 247,
225, 248 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) = ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)))) |
250 | 249 | oveq1d 6665 |
. . . 4
⊢ (𝜑 → ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍)) = (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) |
251 | 245, 250 | breqtrd 4679 |
. . 3
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) |
252 | 157, 218,
251 | 3jca 1242 |
. 2
⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) |
253 | 24, 156, 252 | 3jca 1242 |
1
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) |