Step | Hyp | Ref
| Expression |
1 | | pntibndlem2.10 |
. . 3
β’ (π β π β β) |
2 | 1 | nnrpd 12962 |
. 2
β’ (π β π β
β+) |
3 | | pntibndlem2.11 |
. . . . 5
β’ (π β ((π < π β§ π β€ ((π / 2) Β· π)) β§ (absβ((π
βπ) / π)) β€ (πΈ / 2))) |
4 | 3 | simpld 496 |
. . . 4
β’ (π β (π < π β§ π β€ ((π / 2) Β· π))) |
5 | 4 | simpld 496 |
. . 3
β’ (π β π < π) |
6 | | 1red 11163 |
. . . . . 6
β’ (π β 1 β
β) |
7 | | ioossre 13332 |
. . . . . . . 8
β’ (0(,)1)
β β |
8 | | pntibnd.r |
. . . . . . . . 9
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
9 | | pntibndlem1.1 |
. . . . . . . . 9
β’ (π β π΄ β
β+) |
10 | | pntibndlem1.l |
. . . . . . . . 9
β’ πΏ = ((1 / 4) / (π΄ + 3)) |
11 | 8, 9, 10 | pntibndlem1 26953 |
. . . . . . . 8
β’ (π β πΏ β (0(,)1)) |
12 | 7, 11 | sselid 3947 |
. . . . . . 7
β’ (π β πΏ β β) |
13 | | pntibndlem3.4 |
. . . . . . . 8
β’ (π β πΈ β (0(,)1)) |
14 | 7, 13 | sselid 3947 |
. . . . . . 7
β’ (π β πΈ β β) |
15 | 12, 14 | remulcld 11192 |
. . . . . 6
β’ (π β (πΏ Β· πΈ) β β) |
16 | 6, 15 | readdcld 11191 |
. . . . 5
β’ (π β (1 + (πΏ Β· πΈ)) β β) |
17 | 1 | nnred 12175 |
. . . . 5
β’ (π β π β β) |
18 | 16, 17 | remulcld 11192 |
. . . 4
β’ (π β ((1 + (πΏ Β· πΈ)) Β· π) β β) |
19 | | 2re 12234 |
. . . . 5
β’ 2 β
β |
20 | | remulcl 11143 |
. . . . 5
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
21 | 19, 17, 20 | sylancr 588 |
. . . 4
β’ (π β (2 Β· π) β
β) |
22 | | pntibndlem3.c |
. . . . . . . . . 10
β’ πΆ = ((2 Β· π΅) +
(logβ2)) |
23 | | pntibndlem3.3 |
. . . . . . . . . . . . 13
β’ (π β π΅ β
β+) |
24 | 23 | rpred 12964 |
. . . . . . . . . . . 12
β’ (π β π΅ β β) |
25 | | remulcl 11143 |
. . . . . . . . . . . 12
β’ ((2
β β β§ π΅
β β) β (2 Β· π΅) β β) |
26 | 19, 24, 25 | sylancr 588 |
. . . . . . . . . . 11
β’ (π β (2 Β· π΅) β
β) |
27 | | 2rp 12927 |
. . . . . . . . . . . . 13
β’ 2 β
β+ |
28 | 27 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 2 β
β+) |
29 | 28 | relogcld 25994 |
. . . . . . . . . . 11
β’ (π β (logβ2) β
β) |
30 | 26, 29 | readdcld 11191 |
. . . . . . . . . 10
β’ (π β ((2 Β· π΅) + (logβ2)) β
β) |
31 | 22, 30 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π β πΆ β β) |
32 | | eliooord 13330 |
. . . . . . . . . . . 12
β’ (πΈ β (0(,)1) β (0 <
πΈ β§ πΈ < 1)) |
33 | 13, 32 | syl 17 |
. . . . . . . . . . 11
β’ (π β (0 < πΈ β§ πΈ < 1)) |
34 | 33 | simpld 496 |
. . . . . . . . . 10
β’ (π β 0 < πΈ) |
35 | 14, 34 | elrpd 12961 |
. . . . . . . . 9
β’ (π β πΈ β
β+) |
36 | 31, 35 | rerpdivcld 12995 |
. . . . . . . 8
β’ (π β (πΆ / πΈ) β β) |
37 | 36 | reefcld 15977 |
. . . . . . 7
β’ (π β (expβ(πΆ / πΈ)) β β) |
38 | | pnfxr 11216 |
. . . . . . 7
β’ +β
β β* |
39 | | icossre 13352 |
. . . . . . 7
β’
(((expβ(πΆ /
πΈ)) β β β§
+β β β*) β ((expβ(πΆ / πΈ))[,)+β) β
β) |
40 | 37, 38, 39 | sylancl 587 |
. . . . . 6
β’ (π β ((expβ(πΆ / πΈ))[,)+β) β
β) |
41 | | pntibndlem2.8 |
. . . . . 6
β’ (π β π β ((expβ(πΆ / πΈ))[,)+β)) |
42 | 40, 41 | sseldd 3950 |
. . . . 5
β’ (π β π β β) |
43 | | ioossre 13332 |
. . . . . 6
β’ (π(,)+β) β
β |
44 | | pntibndlem2.9 |
. . . . . 6
β’ (π β π β (π(,)+β)) |
45 | 43, 44 | sselid 3947 |
. . . . 5
β’ (π β π β β) |
46 | 42, 45 | remulcld 11192 |
. . . 4
β’ (π β (π Β· π) β β) |
47 | 19 | a1i 11 |
. . . . 5
β’ (π β 2 β
β) |
48 | | eliooord 13330 |
. . . . . . . . . . . . 13
β’ (πΏ β (0(,)1) β (0 <
πΏ β§ πΏ < 1)) |
49 | 11, 48 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (0 < πΏ β§ πΏ < 1)) |
50 | 49 | simpld 496 |
. . . . . . . . . . 11
β’ (π β 0 < πΏ) |
51 | 12, 50 | elrpd 12961 |
. . . . . . . . . 10
β’ (π β πΏ β
β+) |
52 | 51 | rpge0d 12968 |
. . . . . . . . 9
β’ (π β 0 β€ πΏ) |
53 | 49 | simprd 497 |
. . . . . . . . 9
β’ (π β πΏ < 1) |
54 | 35 | rpge0d 12968 |
. . . . . . . . 9
β’ (π β 0 β€ πΈ) |
55 | 33 | simprd 497 |
. . . . . . . . 9
β’ (π β πΈ < 1) |
56 | 12, 6, 14, 6, 52, 53, 54, 55 | ltmul12ad 12103 |
. . . . . . . 8
β’ (π β (πΏ Β· πΈ) < (1 Β· 1)) |
57 | | 1t1e1 12322 |
. . . . . . . 8
β’ (1
Β· 1) = 1 |
58 | 56, 57 | breqtrdi 5151 |
. . . . . . 7
β’ (π β (πΏ Β· πΈ) < 1) |
59 | 15, 6, 6, 58 | ltadd2dd 11321 |
. . . . . 6
β’ (π β (1 + (πΏ Β· πΈ)) < (1 + 1)) |
60 | | df-2 12223 |
. . . . . 6
β’ 2 = (1 +
1) |
61 | 59, 60 | breqtrrdi 5152 |
. . . . 5
β’ (π β (1 + (πΏ Β· πΈ)) < 2) |
62 | 16, 47, 2, 61 | ltmul1dd 13019 |
. . . 4
β’ (π β ((1 + (πΏ Β· πΈ)) Β· π) < (2 Β· π)) |
63 | 4 | simprd 497 |
. . . . . 6
β’ (π β π β€ ((π / 2) Β· π)) |
64 | 42 | recnd 11190 |
. . . . . . 7
β’ (π β π β β) |
65 | 45 | recnd 11190 |
. . . . . . 7
β’ (π β π β β) |
66 | | rpcnne0 12940 |
. . . . . . . 8
β’ (2 β
β+ β (2 β β β§ 2 β 0)) |
67 | 27, 66 | mp1i 13 |
. . . . . . 7
β’ (π β (2 β β β§ 2
β 0)) |
68 | | div23 11839 |
. . . . . . 7
β’ ((π β β β§ π β β β§ (2 β
β β§ 2 β 0)) β ((π Β· π) / 2) = ((π / 2) Β· π)) |
69 | 64, 65, 67, 68 | syl3anc 1372 |
. . . . . 6
β’ (π β ((π Β· π) / 2) = ((π / 2) Β· π)) |
70 | 63, 69 | breqtrrd 5138 |
. . . . 5
β’ (π β π β€ ((π Β· π) / 2)) |
71 | 17, 46, 28 | lemuldiv2d 13014 |
. . . . 5
β’ (π β ((2 Β· π) β€ (π Β· π) β π β€ ((π Β· π) / 2))) |
72 | 70, 71 | mpbird 257 |
. . . 4
β’ (π β (2 Β· π) β€ (π Β· π)) |
73 | 18, 21, 46, 62, 72 | ltletrd 11322 |
. . 3
β’ (π β ((1 + (πΏ Β· πΈ)) Β· π) < (π Β· π)) |
74 | | pntibndlem3.2 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β β+
(absβ((π
βπ₯) / π₯)) β€ π΄) |
75 | | pntibndlem3.k |
. . . . . . . . . . . 12
β’ πΎ = (expβ(π΅ / (πΈ / 2))) |
76 | 8, 9, 10, 74, 23, 75, 22, 13, 9, 1 | pntibndlem2a 26954 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ β β β§ π β€ π’ β§ π’ β€ ((1 + (πΏ Β· πΈ)) Β· π))) |
77 | 76 | simp1d 1143 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π’ β β) |
78 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β
β+) |
79 | 76 | simp2d 1144 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β€ π’) |
80 | 77, 78, 79 | rpgecld 13003 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π’ β β+) |
81 | 8 | pntrf 26927 |
. . . . . . . . . 10
β’ π
:β+βΆβ |
82 | 81 | ffvelcdmi 7039 |
. . . . . . . . 9
β’ (π’ β β+
β (π
βπ’) β
β) |
83 | 80, 82 | syl 17 |
. . . . . . . 8
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π
βπ’) β β) |
84 | 83, 80 | rerpdivcld 12995 |
. . . . . . 7
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ’) / π’) β β) |
85 | 84 | recnd 11190 |
. . . . . 6
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ’) / π’) β β) |
86 | 85 | abscld 15328 |
. . . . 5
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ’) / π’)) β β) |
87 | 81 | ffvelcdmi 7039 |
. . . . . . . . . . . 12
β’ (π β β+
β (π
βπ) β
β) |
88 | 2, 87 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π
βπ) β β) |
89 | 88, 1 | nndivred 12214 |
. . . . . . . . . 10
β’ (π β ((π
βπ) / π) β β) |
90 | 89 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ) / π) β β) |
91 | 90 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ) / π) β β) |
92 | 85, 91 | subcld 11519 |
. . . . . . 7
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π
βπ’) / π’) β ((π
βπ) / π)) β β) |
93 | 92 | abscld 15328 |
. . . . . 6
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((π
βπ’) / π’) β ((π
βπ) / π))) β β) |
94 | 91 | abscld 15328 |
. . . . . 6
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ) / π)) β β) |
95 | 93, 94 | readdcld 11191 |
. . . . 5
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ(((π
βπ’) / π’) β ((π
βπ) / π))) + (absβ((π
βπ) / π))) β β) |
96 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β πΈ β β) |
97 | 85, 91 | abs2difd 15349 |
. . . . . 6
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π
βπ’) / π’)) β (absβ((π
βπ) / π))) β€ (absβ(((π
βπ’) / π’) β ((π
βπ) / π)))) |
98 | 86, 94, 93 | lesubaddd 11759 |
. . . . . 6
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((absβ((π
βπ’) / π’)) β (absβ((π
βπ) / π))) β€ (absβ(((π
βπ’) / π’) β ((π
βπ) / π))) β (absβ((π
βπ’) / π’)) β€ ((absβ(((π
βπ’) / π’) β ((π
βπ) / π))) + (absβ((π
βπ) / π))))) |
99 | 97, 98 | mpbid 231 |
. . . . 5
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ’) / π’)) β€ ((absβ(((π
βπ’) / π’) β ((π
βπ) / π))) + (absβ((π
βπ) / π)))) |
100 | 96 | rehalfcld 12407 |
. . . . . . 7
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (πΈ / 2) β β) |
101 | 17 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β β) |
102 | 77, 101 | resubcld 11590 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ β π) β β) |
103 | 102, 78 | rerpdivcld 12995 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ β π) / π) β β) |
104 | | 3re 12240 |
. . . . . . . . . . . 12
β’ 3 β
β |
105 | 104 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 3 β
β) |
106 | 86, 105 | readdcld 11191 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π
βπ’) / π’)) + 3) β β) |
107 | 103, 106 | remulcld 11192 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) β β) |
108 | | pntibndlem2.5 |
. . . . . . . . . . . 12
β’ (π β π β
β+) |
109 | 108 | rpred 12964 |
. . . . . . . . . . 11
β’ (π β π β β) |
110 | 109 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β β) |
111 | | 1red 11163 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 1 β
β) |
112 | | 4nn 12243 |
. . . . . . . . . . . . . . . . . 18
β’ 4 β
β |
113 | | nnrp 12933 |
. . . . . . . . . . . . . . . . . 18
β’ (4 β
β β 4 β β+) |
114 | 112, 113 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
β’ (π β 4 β
β+) |
115 | 35, 114 | rpdivcld 12981 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΈ / 4) β
β+) |
116 | 108, 115 | rpdivcld 12981 |
. . . . . . . . . . . . . . 15
β’ (π β (π / (πΈ / 4)) β
β+) |
117 | 116 | rpred 12964 |
. . . . . . . . . . . . . 14
β’ (π β (π / (πΈ / 4)) β β) |
118 | 117 | reefcld 15977 |
. . . . . . . . . . . . 13
β’ (π β (expβ(π / (πΈ / 4))) β β) |
119 | 118 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (expβ(π / (πΈ / 4))) β β) |
120 | | efgt1 16005 |
. . . . . . . . . . . . . 14
β’ ((π / (πΈ / 4)) β β+ β 1
< (expβ(π / (πΈ / 4)))) |
121 | 116, 120 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 1 < (expβ(π / (πΈ / 4)))) |
122 | 121 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 1 < (expβ(π / (πΈ / 4)))) |
123 | | pntibndlem2.7 |
. . . . . . . . . . . . . . . 16
β’ π = ((expβ(π / (πΈ / 4))) + π) |
124 | | pntibndlem3.6 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β
β+) |
125 | 124 | rpred 12964 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
126 | 118, 125 | readdcld 11191 |
. . . . . . . . . . . . . . . 16
β’ (π β ((expβ(π / (πΈ / 4))) + π) β β) |
127 | 123, 126 | eqeltrid 2842 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
128 | 118, 124 | ltaddrpd 12997 |
. . . . . . . . . . . . . . . 16
β’ (π β (expβ(π / (πΈ / 4))) < ((expβ(π / (πΈ / 4))) + π)) |
129 | 128, 123 | breqtrrdi 5152 |
. . . . . . . . . . . . . . 15
β’ (π β (expβ(π / (πΈ / 4))) < π) |
130 | | eliooord 13330 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π(,)+β) β (π < π β§ π < +β)) |
131 | 44, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (π < π β§ π < +β)) |
132 | 131 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (π β π < π) |
133 | 118, 127,
45, 129, 132 | lttrd 11323 |
. . . . . . . . . . . . . 14
β’ (π β (expβ(π / (πΈ / 4))) < π) |
134 | 118, 45, 17, 133, 5 | lttrd 11323 |
. . . . . . . . . . . . 13
β’ (π β (expβ(π / (πΈ / 4))) < π) |
135 | 134 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (expβ(π / (πΈ / 4))) < π) |
136 | 111, 119,
101, 122, 135 | lttrd 11323 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 1 < π) |
137 | 101, 136 | rplogcld 26000 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (logβπ) β
β+) |
138 | 110, 137 | rerpdivcld 12995 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (logβπ)) β β) |
139 | 107, 138 | readdcld 11191 |
. . . . . . . 8
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) + (π / (logβπ))) β β) |
140 | | peano2re 11335 |
. . . . . . . . . . . 12
β’
((absβ((π
βπ’) / π’)) β β β ((absβ((π
βπ’) / π’)) + 1) β β) |
141 | 86, 140 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π
βπ’) / π’)) + 1) β β) |
142 | 103, 141 | remulcld 11192 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) β β) |
143 | | chpcl 26489 |
. . . . . . . . . . . . 13
β’ (π’ β β β
(Οβπ’) β
β) |
144 | 77, 143 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (Οβπ’) β β) |
145 | | chpcl 26489 |
. . . . . . . . . . . . 13
β’ (π β β β
(Οβπ) β
β) |
146 | 101, 145 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (Οβπ) β β) |
147 | 144, 146 | resubcld 11590 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((Οβπ’) β (Οβπ)) β β) |
148 | 147, 78 | rerpdivcld 12995 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((Οβπ’) β (Οβπ)) / π) β β) |
149 | 142, 148 | readdcld 11191 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((Οβπ’) β (Οβπ)) / π)) β β) |
150 | 103, 86 | remulcld 11192 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) β β) |
151 | 88 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π
βπ) β β) |
152 | 83, 151 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ’) β (π
βπ)) β β) |
153 | 152 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ’) β (π
βπ)) β β) |
154 | 153 | abscld 15328 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ’) β (π
βπ))) β β) |
155 | 154, 78 | rerpdivcld 12995 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π
βπ’) β (π
βπ))) / π) β β) |
156 | 150, 155 | readdcld 11191 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((absβ((π
βπ’) β (π
βπ))) / π)) β β) |
157 | 103, 84 | remulcld 11192 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((π
βπ’) / π’)) β β) |
158 | 157 | renegcld 11589 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β -(((π’ β π) / π) Β· ((π
βπ’) / π’)) β β) |
159 | 158 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β -(((π’ β π) / π) Β· ((π
βπ’) / π’)) β β) |
160 | 152, 78 | rerpdivcld 12995 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π
βπ’) β (π
βπ)) / π) β β) |
161 | 160 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π
βπ’) β (π
βπ)) / π) β β) |
162 | 159, 161 | abstrid 15348 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(-(((π’ β π) / π) Β· ((π
βπ’) / π’)) + (((π
βπ’) β (π
βπ)) / π))) β€ ((absβ-(((π’ β π) / π) Β· ((π
βπ’) / π’))) + (absβ(((π
βπ’) β (π
βπ)) / π)))) |
163 | 77 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π’ β β) |
164 | 101 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β β) |
165 | 78 | rpne0d 12969 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β 0) |
166 | 163, 164,
164, 165 | divsubdird 11977 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ β π) / π) = ((π’ / π) β (π / π))) |
167 | 164, 165 | dividd 11936 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / π) = 1) |
168 | 167 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ / π) β (π / π)) = ((π’ / π) β 1)) |
169 | 166, 168 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ β π) / π) = ((π’ / π) β 1)) |
170 | 169 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((π
βπ’) / π’)) = (((π’ / π) β 1) Β· ((π
βπ’) / π’))) |
171 | 77, 78 | rerpdivcld 12995 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ / π) β β) |
172 | 171 | recnd 11190 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ / π) β β) |
173 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 1 β
β) |
174 | 172, 173,
85 | subdird 11619 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ / π) β 1) Β· ((π
βπ’) / π’)) = (((π’ / π) Β· ((π
βπ’) / π’)) β (1 Β· ((π
βπ’) / π’)))) |
175 | 80 | rpcnne0d 12973 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ β β β§ π’ β 0)) |
176 | 78 | rpcnne0d 12973 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π β β β§ π β 0)) |
177 | 83 | recnd 11190 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π
βπ’) β β) |
178 | | dmdcan 11872 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π’ β β β§ π’ β 0) β§ (π β β β§ π β 0) β§ (π
βπ’) β β) β ((π’ / π) Β· ((π
βπ’) / π’)) = ((π
βπ’) / π)) |
179 | 175, 176,
177, 178 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ / π) Β· ((π
βπ’) / π’)) = ((π
βπ’) / π)) |
180 | 85 | mulid2d 11180 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (1 Β· ((π
βπ’) / π’)) = ((π
βπ’) / π’)) |
181 | 179, 180 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ / π) Β· ((π
βπ’) / π’)) β (1 Β· ((π
βπ’) / π’))) = (((π
βπ’) / π) β ((π
βπ’) / π’))) |
182 | 170, 174,
181 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((π
βπ’) / π’)) = (((π
βπ’) / π) β ((π
βπ’) / π’))) |
183 | 182 | negeqd 11402 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β -(((π’ β π) / π) Β· ((π
βπ’) / π’)) = -(((π
βπ’) / π) β ((π
βπ’) / π’))) |
184 | 83, 78 | rerpdivcld 12995 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ’) / π) β β) |
185 | 184 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ’) / π) β β) |
186 | 185, 85 | negsubdi2d 11535 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β -(((π
βπ’) / π) β ((π
βπ’) / π’)) = (((π
βπ’) / π’) β ((π
βπ’) / π))) |
187 | 183, 186 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β -(((π’ β π) / π) Β· ((π
βπ’) / π’)) = (((π
βπ’) / π’) β ((π
βπ’) / π))) |
188 | 151 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π
βπ) β β) |
189 | 177, 188,
164, 165 | divsubdird 11977 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π
βπ’) β (π
βπ)) / π) = (((π
βπ’) / π) β ((π
βπ) / π))) |
190 | 187, 189 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (-(((π’ β π) / π) Β· ((π
βπ’) / π’)) + (((π
βπ’) β (π
βπ)) / π)) = ((((π
βπ’) / π’) β ((π
βπ’) / π)) + (((π
βπ’) / π) β ((π
βπ) / π)))) |
191 | 85, 185, 91 | npncand 11543 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π
βπ’) / π’) β ((π
βπ’) / π)) + (((π
βπ’) / π) β ((π
βπ) / π))) = (((π
βπ’) / π’) β ((π
βπ) / π))) |
192 | 190, 191 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (-(((π’ β π) / π) Β· ((π
βπ’) / π’)) + (((π
βπ’) β (π
βπ)) / π)) = (((π
βπ’) / π’) β ((π
βπ) / π))) |
193 | 192 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(-(((π’ β π) / π) Β· ((π
βπ’) / π’)) + (((π
βπ’) β (π
βπ)) / π))) = (absβ(((π
βπ’) / π’) β ((π
βπ) / π)))) |
194 | 157 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((π
βπ’) / π’)) β β) |
195 | 194 | absnegd 15341 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ-(((π’ β π) / π) Β· ((π
βπ’) / π’))) = (absβ(((π’ β π) / π) Β· ((π
βπ’) / π’)))) |
196 | 103 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ β π) / π) β β) |
197 | 196, 85 | absmuld 15346 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((π’ β π) / π) Β· ((π
βπ’) / π’))) = ((absβ((π’ β π) / π)) Β· (absβ((π
βπ’) / π’)))) |
198 | 77, 101 | subge0d 11752 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (0 β€ (π’ β π) β π β€ π’)) |
199 | 79, 198 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 0 β€ (π’ β π)) |
200 | 102, 78, 199 | divge0d 13004 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 0 β€ ((π’ β π) / π)) |
201 | 103, 200 | absidd 15314 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π’ β π) / π)) = ((π’ β π) / π)) |
202 | 201 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π’ β π) / π)) Β· (absβ((π
βπ’) / π’))) = (((π’ β π) / π) Β· (absβ((π
βπ’) / π’)))) |
203 | 195, 197,
202 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ-(((π’ β π) / π) Β· ((π
βπ’) / π’))) = (((π’ β π) / π) Β· (absβ((π
βπ’) / π’)))) |
204 | 153, 164,
165 | absdivd 15347 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((π
βπ’) β (π
βπ)) / π)) = ((absβ((π
βπ’) β (π
βπ))) / (absβπ))) |
205 | 78 | rprege0d 12971 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π β β β§ 0 β€ π)) |
206 | | absid 15188 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ 0 β€
π) β (absβπ) = π) |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβπ) = π) |
208 | 207 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π
βπ’) β (π
βπ))) / (absβπ)) = ((absβ((π
βπ’) β (π
βπ))) / π)) |
209 | 204, 208 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((π
βπ’) β (π
βπ)) / π)) = ((absβ((π
βπ’) β (π
βπ))) / π)) |
210 | 203, 209 | oveq12d 7380 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ-(((π’ β π) / π) Β· ((π
βπ’) / π’))) + (absβ(((π
βπ’) β (π
βπ)) / π))) = ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((absβ((π
βπ’) β (π
βπ))) / π))) |
211 | 162, 193,
210 | 3brtr3d 5141 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((π
βπ’) / π’) β ((π
βπ) / π))) β€ ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((absβ((π
βπ’) β (π
βπ))) / π))) |
212 | 102, 147 | readdcld 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ β π) + ((Οβπ’) β (Οβπ))) β β) |
213 | 212, 78 | rerpdivcld 12995 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) + ((Οβπ’) β (Οβπ))) / π) β β) |
214 | 147 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((Οβπ’) β (Οβπ)) β β) |
215 | 164, 163 | subcld 11519 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π β π’) β β) |
216 | 214, 215 | abstrid 15348 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((Οβπ’) β (Οβπ)) + (π β π’))) β€ ((absβ((Οβπ’) β (Οβπ))) + (absβ(π β π’)))) |
217 | 8 | pntrval 26926 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β β+
β (π
βπ’) = ((Οβπ’) β π’)) |
218 | 80, 217 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π
βπ’) = ((Οβπ’) β π’)) |
219 | 8 | pntrval 26926 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β+
β (π
βπ) = ((Οβπ) β π)) |
220 | 78, 219 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π
βπ) = ((Οβπ) β π)) |
221 | 218, 220 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π
βπ’) β (π
βπ)) = (((Οβπ’) β π’) β ((Οβπ) β π))) |
222 | 144 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (Οβπ’) β β) |
223 | 146 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (Οβπ) β β) |
224 | | subadd4 11452 |
. . . . . . . . . . . . . . . . . 18
β’
((((Οβπ’)
β β β§ (Οβπ) β β) β§ (π’ β β β§ π β β)) β
(((Οβπ’) β
(Οβπ)) β
(π’ β π)) = (((Οβπ’) + π) β ((Οβπ) + π’))) |
225 | | sub4 11453 |
. . . . . . . . . . . . . . . . . 18
β’
((((Οβπ’)
β β β§ (Οβπ) β β) β§ (π’ β β β§ π β β)) β
(((Οβπ’) β
(Οβπ)) β
(π’ β π)) = (((Οβπ’) β π’) β ((Οβπ) β π))) |
226 | | addsub4 11451 |
. . . . . . . . . . . . . . . . . . 19
β’
((((Οβπ’)
β β β§ π
β β) β§ ((Οβπ) β β β§ π’ β β)) β (((Οβπ’) + π) β ((Οβπ) + π’)) = (((Οβπ’) β (Οβπ)) + (π β π’))) |
227 | 226 | an42s 660 |
. . . . . . . . . . . . . . . . . 18
β’
((((Οβπ’)
β β β§ (Οβπ) β β) β§ (π’ β β β§ π β β)) β
(((Οβπ’) + π) β ((Οβπ) + π’)) = (((Οβπ’) β (Οβπ)) + (π β π’))) |
228 | 224, 225,
227 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
β’
((((Οβπ’)
β β β§ (Οβπ) β β) β§ (π’ β β β§ π β β)) β
(((Οβπ’) β
π’) β
((Οβπ) β
π)) = (((Οβπ’) β (Οβπ)) + (π β π’))) |
229 | 222, 223,
163, 164, 228 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((Οβπ’) β π’) β ((Οβπ) β π)) = (((Οβπ’) β (Οβπ)) + (π β π’))) |
230 | 221, 229 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((Οβπ’) β (Οβπ)) + (π β π’)) = ((π
βπ’) β (π
βπ))) |
231 | 230 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((Οβπ’) β (Οβπ)) + (π β π’))) = (absβ((π
βπ’) β (π
βπ)))) |
232 | 102 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ β π) β β) |
233 | | chpwordi 26522 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π’ β β β§ π β€ π’) β (Οβπ) β€ (Οβπ’)) |
234 | 101, 77, 79, 233 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (Οβπ) β€ (Οβπ’)) |
235 | 146, 144,
234 | abssubge0d 15323 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((Οβπ’) β (Οβπ))) = ((Οβπ’) β (Οβπ))) |
236 | 101, 77, 79 | abssuble0d 15324 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(π β π’)) = (π’ β π)) |
237 | 235, 236 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((Οβπ’) β (Οβπ))) + (absβ(π β π’))) = (((Οβπ’) β (Οβπ)) + (π’ β π))) |
238 | 214, 232,
237 | comraddd 11376 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((Οβπ’) β (Οβπ))) + (absβ(π β π’))) = ((π’ β π) + ((Οβπ’) β (Οβπ)))) |
239 | 216, 231,
238 | 3brtr3d 5141 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ’) β (π
βπ))) β€ ((π’ β π) + ((Οβπ’) β (Οβπ)))) |
240 | 154, 212,
78, 239 | lediv1dd 13022 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π
βπ’) β (π
βπ))) / π) β€ (((π’ β π) + ((Οβπ’) β (Οβπ))) / π)) |
241 | 155, 213,
150, 240 | leadd2dd 11777 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((absβ((π
βπ’) β (π
βπ))) / π)) β€ ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + (((π’ β π) + ((Οβπ’) β (Οβπ))) / π))) |
242 | 150 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) β β) |
243 | 148 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((Οβπ’) β (Οβπ)) / π) β β) |
244 | 242, 196,
243 | addassd 11184 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((π’ β π) / π)) + (((Οβπ’) β (Οβπ)) / π)) = ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + (((π’ β π) / π) + (((Οβπ’) β (Οβπ)) / π)))) |
245 | 86 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ’) / π’)) β β) |
246 | 196, 245,
173 | adddid 11186 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) = ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + (((π’ β π) / π) Β· 1))) |
247 | 196 | mulid1d 11179 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· 1) = ((π’ β π) / π)) |
248 | 247 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + (((π’ β π) / π) Β· 1)) = ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((π’ β π) / π))) |
249 | 246, 248 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) = ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((π’ β π) / π))) |
250 | 249 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((Οβπ’) β (Οβπ)) / π)) = (((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((π’ β π) / π)) + (((Οβπ’) β (Οβπ)) / π))) |
251 | 232, 214,
164, 165 | divdird 11976 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) + ((Οβπ’) β (Οβπ))) / π) = (((π’ β π) / π) + (((Οβπ’) β (Οβπ)) / π))) |
252 | 251 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + (((π’ β π) + ((Οβπ’) β (Οβπ))) / π)) = ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + (((π’ β π) / π) + (((Οβπ’) β (Οβπ)) / π)))) |
253 | 244, 250,
252 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((Οβπ’) β (Οβπ)) / π)) = ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + (((π’ β π) + ((Οβπ’) β (Οβπ))) / π))) |
254 | 241, 253 | breqtrrd 5138 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· (absβ((π
βπ’) / π’))) + ((absβ((π
βπ’) β (π
βπ))) / π)) β€ ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((Οβπ’) β (Οβπ)) / π))) |
255 | 93, 156, 149, 211, 254 | letrd 11319 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((π
βπ’) / π’) β ((π
βπ) / π))) β€ ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((Οβπ’) β (Οβπ)) / π))) |
256 | | remulcl 11143 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ ((π’
β π) / π) β β) β (2
Β· ((π’ β π) / π)) β β) |
257 | 19, 103, 256 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (2 Β· ((π’ β π) / π)) β β) |
258 | 257, 138 | readdcld 11191 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((2 Β· ((π’ β π) / π)) + (π / (logβπ))) β β) |
259 | | remulcl 11143 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ (π’
β π) β β)
β (2 Β· (π’
β π)) β
β) |
260 | 19, 102, 259 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (2 Β· (π’ β π)) β β) |
261 | 101, 137 | rerpdivcld 12995 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (logβπ)) β β) |
262 | 110, 261 | remulcld 11192 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π Β· (π / (logβπ))) β β) |
263 | 260, 262 | readdcld 11191 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((2 Β· (π’ β π)) + (π Β· (π / (logβπ)))) β β) |
264 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π’ β (Οβπ¦) = (Οβπ’)) |
265 | 264 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π’ β ((Οβπ¦) β (Οβπ)) = ((Οβπ’) β (Οβπ))) |
266 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π’ β (π¦ β π) = (π’ β π)) |
267 | 266 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π’ β (2 Β· (π¦ β π)) = (2 Β· (π’ β π))) |
268 | 267 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π’ β ((2 Β· (π¦ β π)) + (π Β· (π / (logβπ)))) = ((2 Β· (π’ β π)) + (π Β· (π / (logβπ))))) |
269 | 265, 268 | breq12d 5123 |
. . . . . . . . . . . . . 14
β’ (π¦ = π’ β (((Οβπ¦) β (Οβπ)) β€ ((2 Β· (π¦ β π)) + (π Β· (π / (logβπ)))) β ((Οβπ’) β (Οβπ)) β€ ((2 Β· (π’ β π)) + (π Β· (π / (logβπ)))))) |
270 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β π₯ = π) |
271 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (2 Β· π₯) = (2 Β· π)) |
272 | 270, 271 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π₯[,](2 Β· π₯)) = (π[,](2 Β· π))) |
273 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (Οβπ₯) = (Οβπ)) |
274 | 273 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β ((Οβπ¦) β (Οβπ₯)) = ((Οβπ¦) β (Οβπ))) |
275 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (π¦ β π₯) = (π¦ β π)) |
276 | 275 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (2 Β· (π¦ β π₯)) = (2 Β· (π¦ β π))) |
277 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β (logβπ₯) = (logβπ)) |
278 | 270, 277 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (π₯ / (logβπ₯)) = (π / (logβπ))) |
279 | 278 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (π Β· (π₯ / (logβπ₯))) = (π Β· (π / (logβπ)))) |
280 | 276, 279 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β ((2 Β· (π¦ β π₯)) + (π Β· (π₯ / (logβπ₯)))) = ((2 Β· (π¦ β π)) + (π Β· (π / (logβπ))))) |
281 | 274, 280 | breq12d 5123 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (((Οβπ¦) β (Οβπ₯)) β€ ((2 Β· (π¦ β π₯)) + (π Β· (π₯ / (logβπ₯)))) β ((Οβπ¦) β (Οβπ)) β€ ((2 Β· (π¦ β π)) + (π Β· (π / (logβπ)))))) |
282 | 272, 281 | raleqbidv 3322 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (βπ¦ β (π₯[,](2 Β· π₯))((Οβπ¦) β (Οβπ₯)) β€ ((2 Β· (π¦ β π₯)) + (π Β· (π₯ / (logβπ₯)))) β βπ¦ β (π[,](2 Β· π))((Οβπ¦) β (Οβπ)) β€ ((2 Β· (π¦ β π)) + (π Β· (π / (logβπ)))))) |
283 | | pntibndlem2.6 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ₯ β (1(,)+β)βπ¦ β (π₯[,](2 Β· π₯))((Οβπ¦) β (Οβπ₯)) β€ ((2 Β· (π¦ β π₯)) + (π Β· (π₯ / (logβπ₯))))) |
284 | 283 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β βπ₯ β (1(,)+β)βπ¦ β (π₯[,](2 Β· π₯))((Οβπ¦) β (Οβπ₯)) β€ ((2 Β· (π¦ β π₯)) + (π Β· (π₯ / (logβπ₯))))) |
285 | | 1xr 11221 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β* |
286 | | elioopnf 13367 |
. . . . . . . . . . . . . . . . 17
β’ (1 β
β* β (π β (1(,)+β) β (π β β β§ 1 <
π))) |
287 | 285, 286 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (π β (1(,)+β) β
(π β β β§ 1
< π)) |
288 | 101, 136,
287 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β (1(,)+β)) |
289 | 282, 284,
288 | rspcdva 3585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β βπ¦ β (π[,](2 Β· π))((Οβπ¦) β (Οβπ)) β€ ((2 Β· (π¦ β π)) + (π Β· (π / (logβπ))))) |
290 | 18 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((1 + (πΏ Β· πΈ)) Β· π) β β) |
291 | 21 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (2 Β· π) β β) |
292 | 76 | simp3d 1145 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π’ β€ ((1 + (πΏ Β· πΈ)) Β· π)) |
293 | | ltle 11250 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((1 +
(πΏ Β· πΈ)) β β β§ 2 β
β) β ((1 + (πΏ
Β· πΈ)) < 2 β
(1 + (πΏ Β· πΈ)) β€ 2)) |
294 | 16, 19, 293 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((1 + (πΏ Β· πΈ)) < 2 β (1 + (πΏ Β· πΈ)) β€ 2)) |
295 | 61, 294 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1 + (πΏ Β· πΈ)) β€ 2) |
296 | 295 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (1 + (πΏ Β· πΈ)) β€ 2) |
297 | 16 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (1 + (πΏ Β· πΈ)) β β) |
298 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 2 β
β) |
299 | 297, 298,
78 | lemul1d 13007 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((1 + (πΏ Β· πΈ)) β€ 2 β ((1 + (πΏ Β· πΈ)) Β· π) β€ (2 Β· π))) |
300 | 296, 299 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((1 + (πΏ Β· πΈ)) Β· π) β€ (2 Β· π)) |
301 | 77, 290, 291, 292, 300 | letrd 11319 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π’ β€ (2 Β· π)) |
302 | | elicc2 13336 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (2
Β· π) β β)
β (π’ β (π[,](2 Β· π)) β (π’ β β β§ π β€ π’ β§ π’ β€ (2 Β· π)))) |
303 | 101, 291,
302 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ β (π[,](2 Β· π)) β (π’ β β β§ π β€ π’ β§ π’ β€ (2 Β· π)))) |
304 | 77, 79, 301, 303 | mpbir3and 1343 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π’ β (π[,](2 Β· π))) |
305 | 269, 289,
304 | rspcdva 3585 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((Οβπ’) β (Οβπ)) β€ ((2 Β· (π’ β π)) + (π Β· (π / (logβπ))))) |
306 | 147, 263,
78, 305 | lediv1dd 13022 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((Οβπ’) β (Οβπ)) / π) β€ (((2 Β· (π’ β π)) + (π Β· (π / (logβπ)))) / π)) |
307 | 260 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (2 Β· (π’ β π)) β β) |
308 | 108 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β
β+) |
309 | 308 | rpred 12964 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β β) |
310 | 309, 261 | remulcld 11192 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π Β· (π / (logβπ))) β β) |
311 | 310 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π Β· (π / (logβπ))) β β) |
312 | | divdir 11845 |
. . . . . . . . . . . . . 14
β’ (((2
Β· (π’ β π)) β β β§ (π Β· (π / (logβπ))) β β β§ (π β β β§ π β 0)) β (((2 Β· (π’ β π)) + (π Β· (π / (logβπ)))) / π) = (((2 Β· (π’ β π)) / π) + ((π Β· (π / (logβπ))) / π))) |
313 | 307, 311,
176, 312 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((2 Β· (π’ β π)) + (π Β· (π / (logβπ)))) / π) = (((2 Β· (π’ β π)) / π) + ((π Β· (π / (logβπ))) / π))) |
314 | | 2cnd 12238 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 2 β
β) |
315 | 314, 232,
164, 165 | divassd 11973 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((2 Β· (π’ β π)) / π) = (2 Β· ((π’ β π) / π))) |
316 | 110 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π β β) |
317 | 137 | rpcnne0d 12973 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((logβπ) β β β§ (logβπ) β 0)) |
318 | | div12 11842 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β β§
((logβπ) β
β β§ (logβπ)
β 0)) β (π Β·
(π / (logβπ))) = (π Β· (π / (logβπ)))) |
319 | 316, 164,
317, 318 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π Β· (π / (logβπ))) = (π Β· (π / (logβπ)))) |
320 | 319 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π Β· (π / (logβπ))) / π) = ((π Β· (π / (logβπ))) / π)) |
321 | 308, 137 | rpdivcld 12981 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (logβπ)) β
β+) |
322 | 321 | rpcnd 12966 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (logβπ)) β β) |
323 | 322, 164,
165 | divcan3d 11943 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π Β· (π / (logβπ))) / π) = (π / (logβπ))) |
324 | 320, 323 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π Β· (π / (logβπ))) / π) = (π / (logβπ))) |
325 | 315, 324 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((2 Β· (π’ β π)) / π) + ((π Β· (π / (logβπ))) / π)) = ((2 Β· ((π’ β π) / π)) + (π / (logβπ)))) |
326 | 313, 325 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((2 Β· (π’ β π)) + (π Β· (π / (logβπ)))) / π) = ((2 Β· ((π’ β π) / π)) + (π / (logβπ)))) |
327 | 306, 326 | breqtrd 5136 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((Οβπ’) β (Οβπ)) / π) β€ ((2 Β· ((π’ β π) / π)) + (π / (logβπ)))) |
328 | 148, 258,
142, 327 | leadd2dd 11777 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((Οβπ’) β (Οβπ)) / π)) β€ ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + ((2 Β· ((π’ β π) / π)) + (π / (logβπ))))) |
329 | 142 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) β β) |
330 | 257 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (2 Β· ((π’ β π) / π)) β β) |
331 | 138 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (logβπ)) β β) |
332 | 329, 330,
331 | addassd 11184 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (2 Β· ((π’ β π) / π))) + (π / (logβπ))) = ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + ((2 Β· ((π’ β π) / π)) + (π / (logβπ))))) |
333 | | 2cn 12235 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
334 | | mulcom 11144 |
. . . . . . . . . . . . . . 15
β’ ((2
β β β§ ((π’
β π) / π) β β) β (2
Β· ((π’ β π) / π)) = (((π’ β π) / π) Β· 2)) |
335 | 333, 196,
334 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (2 Β· ((π’ β π) / π)) = (((π’ β π) / π) Β· 2)) |
336 | 335 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (2 Β· ((π’ β π) / π))) = ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((π’ β π) / π) Β· 2))) |
337 | 141 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π
βπ’) / π’)) + 1) β β) |
338 | 196, 337,
314 | adddid 11186 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· (((absβ((π
βπ’) / π’)) + 1) + 2)) = ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((π’ β π) / π) Β· 2))) |
339 | 245, 173,
314 | addassd 11184 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((absβ((π
βπ’) / π’)) + 1) + 2) = ((absβ((π
βπ’) / π’)) + (1 + 2))) |
340 | | 1p2e3 12303 |
. . . . . . . . . . . . . . . 16
β’ (1 + 2) =
3 |
341 | 340 | oveq2i 7373 |
. . . . . . . . . . . . . . 15
β’
((absβ((π
βπ’) / π’)) + (1 + 2)) = ((absβ((π
βπ’) / π’)) + 3) |
342 | 339, 341 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((absβ((π
βπ’) / π’)) + 1) + 2) = ((absβ((π
βπ’) / π’)) + 3)) |
343 | 342 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· (((absβ((π
βπ’) / π’)) + 1) + 2)) = (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3))) |
344 | 336, 338,
343 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (2 Β· ((π’ β π) / π))) = (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3))) |
345 | 344 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (2 Β· ((π’ β π) / π))) + (π / (logβπ))) = ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) + (π / (logβπ)))) |
346 | 332, 345 | eqtr3d 2779 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + ((2 Β· ((π’ β π) / π)) + (π / (logβπ)))) = ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) + (π / (logβπ)))) |
347 | 328, 346 | breqtrd 5136 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 1)) + (((Οβπ’) β (Οβπ)) / π)) β€ ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) + (π / (logβπ)))) |
348 | 93, 149, 139, 255, 347 | letrd 11319 |
. . . . . . . 8
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((π
βπ’) / π’) β ((π
βπ) / π))) β€ ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) + (π / (logβπ)))) |
349 | 100 | rehalfcld 12407 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((πΈ / 2) / 2) β β) |
350 | 77, 297, 78 | ledivmul2d 13018 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ / π) β€ (1 + (πΏ Β· πΈ)) β π’ β€ ((1 + (πΏ Β· πΈ)) Β· π))) |
351 | 292, 350 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ / π) β€ (1 + (πΏ Β· πΈ))) |
352 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
353 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (πΏ Β· πΈ) β β) |
354 | 353 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (πΏ Β· πΈ) β β) |
355 | | addcom 11348 |
. . . . . . . . . . . . . . . 16
β’ ((1
β β β§ (πΏ
Β· πΈ) β β)
β (1 + (πΏ Β·
πΈ)) = ((πΏ Β· πΈ) + 1)) |
356 | 352, 354,
355 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (1 + (πΏ Β· πΈ)) = ((πΏ Β· πΈ) + 1)) |
357 | 351, 356 | breqtrd 5136 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π’ / π) β€ ((πΏ Β· πΈ) + 1)) |
358 | 171, 111,
353 | lesubaddd 11759 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ / π) β 1) β€ (πΏ Β· πΈ) β (π’ / π) β€ ((πΏ Β· πΈ) + 1))) |
359 | 357, 358 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ / π) β 1) β€ (πΏ Β· πΈ)) |
360 | 169, 359 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π’ β π) / π) β€ (πΏ Β· πΈ)) |
361 | 9 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π΄ β
β+) |
362 | 361 | rpred 12964 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β π΄ β β) |
363 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π’ β (π
βπ₯) = (π
βπ’)) |
364 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π’ β π₯ = π’) |
365 | 363, 364 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π’ β ((π
βπ₯) / π₯) = ((π
βπ’) / π’)) |
366 | 365 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π’ β (absβ((π
βπ₯) / π₯)) = (absβ((π
βπ’) / π’))) |
367 | 366 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’ (π₯ = π’ β ((absβ((π
βπ₯) / π₯)) β€ π΄ β (absβ((π
βπ’) / π’)) β€ π΄)) |
368 | 74 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β βπ₯ β β+
(absβ((π
βπ₯) / π₯)) β€ π΄) |
369 | 367, 368,
80 | rspcdva 3585 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ’) / π’)) β€ π΄) |
370 | 86, 362, 105, 369 | leadd1dd 11776 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ((π
βπ’) / π’)) + 3) β€ (π΄ + 3)) |
371 | 103, 200 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) β β β§ 0 β€ ((π’ β π) / π))) |
372 | | 3rp 12928 |
. . . . . . . . . . . . . . 15
β’ 3 β
β+ |
373 | | rpaddcl 12944 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β+
β§ 3 β β+) β (π΄ + 3) β
β+) |
374 | 361, 372,
373 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π΄ + 3) β
β+) |
375 | 374 | rprege0d 12971 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π΄ + 3) β β β§ 0 β€ (π΄ + 3))) |
376 | | lemul12b 12019 |
. . . . . . . . . . . . 13
β’
((((((π’ β
π) / π) β β β§ 0 β€ ((π’ β π) / π)) β§ (πΏ Β· πΈ) β β) β§ (((absβ((π
βπ’) / π’)) + 3) β β β§ ((π΄ + 3) β β β§ 0
β€ (π΄ + 3)))) β
((((π’ β π) / π) β€ (πΏ Β· πΈ) β§ ((absβ((π
βπ’) / π’)) + 3) β€ (π΄ + 3)) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) β€ ((πΏ Β· πΈ) Β· (π΄ + 3)))) |
377 | 371, 353,
106, 375, 376 | syl22anc 838 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) β€ (πΏ Β· πΈ) β§ ((absβ((π
βπ’) / π’)) + 3) β€ (π΄ + 3)) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) β€ ((πΏ Β· πΈ) Β· (π΄ + 3)))) |
378 | 360, 370,
377 | mp2and 698 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) β€ ((πΏ Β· πΈ) Β· (π΄ + 3))) |
379 | 35 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β πΈ β
β+) |
380 | 112, 113 | mp1i 13 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 4 β
β+) |
381 | 379, 380 | rpdivcld 12981 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (πΈ / 4) β
β+) |
382 | 381 | rpcnd 12966 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (πΈ / 4) β β) |
383 | 374 | rpcnd 12966 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π΄ + 3) β β) |
384 | 374 | rpne0d 12969 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π΄ + 3) β 0) |
385 | 382, 383,
384 | divcan1d 11939 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((πΈ / 4) / (π΄ + 3)) Β· (π΄ + 3)) = (πΈ / 4)) |
386 | 14 | recnd 11190 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΈ β β) |
387 | 386 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β πΈ β β) |
388 | 380 | rpcnd 12966 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 4 β
β) |
389 | 380 | rpne0d 12969 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 4 β 0) |
390 | 387, 388,
389 | divrec2d 11942 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (πΈ / 4) = ((1 / 4) Β· πΈ)) |
391 | 390 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((πΈ / 4) / (π΄ + 3)) = (((1 / 4) Β· πΈ) / (π΄ + 3))) |
392 | | 4cn 12245 |
. . . . . . . . . . . . . . . . . 18
β’ 4 β
β |
393 | | 4ne0 12268 |
. . . . . . . . . . . . . . . . . 18
β’ 4 β
0 |
394 | 392, 393 | reccli 11892 |
. . . . . . . . . . . . . . . . 17
β’ (1 / 4)
β β |
395 | 394 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (1 / 4) β
β) |
396 | 395, 387,
383, 384 | div23d 11975 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((1 / 4) Β· πΈ) / (π΄ + 3)) = (((1 / 4) / (π΄ + 3)) Β· πΈ)) |
397 | 10 | oveq1i 7372 |
. . . . . . . . . . . . . . 15
β’ (πΏ Β· πΈ) = (((1 / 4) / (π΄ + 3)) Β· πΈ) |
398 | 396, 397 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((1 / 4) Β· πΈ) / (π΄ + 3)) = (πΏ Β· πΈ)) |
399 | 391, 398 | eqtr2d 2778 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (πΏ Β· πΈ) = ((πΈ / 4) / (π΄ + 3))) |
400 | 399 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((πΏ Β· πΈ) Β· (π΄ + 3)) = (((πΈ / 4) / (π΄ + 3)) Β· (π΄ + 3))) |
401 | | 2ne0 12264 |
. . . . . . . . . . . . . . 15
β’ 2 β
0 |
402 | 401 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β 2 β 0) |
403 | 387, 314,
314, 402, 402 | divdiv1d 11969 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((πΈ / 2) / 2) = (πΈ / (2 Β· 2))) |
404 | | 2t2e4 12324 |
. . . . . . . . . . . . . 14
β’ (2
Β· 2) = 4 |
405 | 404 | oveq2i 7373 |
. . . . . . . . . . . . 13
β’ (πΈ / (2 Β· 2)) = (πΈ / 4) |
406 | 403, 405 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((πΈ / 2) / 2) = (πΈ / 4)) |
407 | 385, 400,
406 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((πΏ Β· πΈ) Β· (π΄ + 3)) = ((πΈ / 2) / 2)) |
408 | 378, 407 | breqtrd 5136 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) β€ ((πΈ / 2) / 2)) |
409 | 117 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (πΈ / 4)) β β) |
410 | 137 | rpred 12964 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (logβπ) β β) |
411 | 78 | reeflogd 25995 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (expβ(logβπ)) = π) |
412 | 135, 411 | breqtrrd 5138 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (expβ(π / (πΈ / 4))) < (expβ(logβπ))) |
413 | | eflt 16006 |
. . . . . . . . . . . . . . 15
β’ (((π / (πΈ / 4)) β β β§ (logβπ) β β) β ((π / (πΈ / 4)) < (logβπ) β (expβ(π / (πΈ / 4))) < (expβ(logβπ)))) |
414 | 409, 410,
413 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((π / (πΈ / 4)) < (logβπ) β (expβ(π / (πΈ / 4))) < (expβ(logβπ)))) |
415 | 412, 414 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (πΈ / 4)) < (logβπ)) |
416 | 409, 410,
415 | ltled 11310 |
. . . . . . . . . . . 12
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (πΈ / 4)) β€ (logβπ)) |
417 | 110, 381,
137, 416 | lediv23d 13032 |
. . . . . . . . . . 11
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (logβπ)) β€ (πΈ / 4)) |
418 | 417, 406 | breqtrrd 5138 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (π / (logβπ)) β€ ((πΈ / 2) / 2)) |
419 | 107, 138,
349, 349, 408, 418 | le2addd 11781 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) + (π / (logβπ))) β€ (((πΈ / 2) / 2) + ((πΈ / 2) / 2))) |
420 | 100 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (πΈ / 2) β β) |
421 | 420 | 2halvesd 12406 |
. . . . . . . . 9
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (((πΈ / 2) / 2) + ((πΈ / 2) / 2)) = (πΈ / 2)) |
422 | 419, 421 | breqtrd 5136 |
. . . . . . . 8
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((((π’ β π) / π) Β· ((absβ((π
βπ’) / π’)) + 3)) + (π / (logβπ))) β€ (πΈ / 2)) |
423 | 93, 139, 100, 348, 422 | letrd 11319 |
. . . . . . 7
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ(((π
βπ’) / π’) β ((π
βπ) / π))) β€ (πΈ / 2)) |
424 | 3 | simprd 497 |
. . . . . . . 8
β’ (π β (absβ((π
βπ) / π)) β€ (πΈ / 2)) |
425 | 424 | adantr 482 |
. . . . . . 7
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ) / π)) β€ (πΈ / 2)) |
426 | 93, 94, 100, 100, 423, 425 | le2addd 11781 |
. . . . . 6
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ(((π
βπ’) / π’) β ((π
βπ) / π))) + (absβ((π
βπ) / π))) β€ ((πΈ / 2) + (πΈ / 2))) |
427 | 387 | 2halvesd 12406 |
. . . . . 6
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((πΈ / 2) + (πΈ / 2)) = πΈ) |
428 | 426, 427 | breqtrd 5136 |
. . . . 5
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β ((absβ(((π
βπ’) / π’) β ((π
βπ) / π))) + (absβ((π
βπ) / π))) β€ πΈ) |
429 | 86, 95, 96, 99, 428 | letrd 11319 |
. . . 4
β’ ((π β§ π’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))) β (absβ((π
βπ’) / π’)) β€ πΈ) |
430 | 429 | ralrimiva 3144 |
. . 3
β’ (π β βπ’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))(absβ((π
βπ’) / π’)) β€ πΈ) |
431 | 5, 73, 430 | jca31 516 |
. 2
β’ (π β ((π < π β§ ((1 + (πΏ Β· πΈ)) Β· π) < (π Β· π)) β§ βπ’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))(absβ((π
βπ’) / π’)) β€ πΈ)) |
432 | | breq2 5114 |
. . . . 5
β’ (π§ = π β (π < π§ β π < π)) |
433 | | oveq2 7370 |
. . . . . 6
β’ (π§ = π β ((1 + (πΏ Β· πΈ)) Β· π§) = ((1 + (πΏ Β· πΈ)) Β· π)) |
434 | 433 | breq1d 5120 |
. . . . 5
β’ (π§ = π β (((1 + (πΏ Β· πΈ)) Β· π§) < (π Β· π) β ((1 + (πΏ Β· πΈ)) Β· π) < (π Β· π))) |
435 | 432, 434 | anbi12d 632 |
. . . 4
β’ (π§ = π β ((π < π§ β§ ((1 + (πΏ Β· πΈ)) Β· π§) < (π Β· π)) β (π < π β§ ((1 + (πΏ Β· πΈ)) Β· π) < (π Β· π)))) |
436 | | id 22 |
. . . . . 6
β’ (π§ = π β π§ = π) |
437 | 436, 433 | oveq12d 7380 |
. . . . 5
β’ (π§ = π β (π§[,]((1 + (πΏ Β· πΈ)) Β· π§)) = (π[,]((1 + (πΏ Β· πΈ)) Β· π))) |
438 | 437 | raleqdv 3316 |
. . . 4
β’ (π§ = π β (βπ’ β (π§[,]((1 + (πΏ Β· πΈ)) Β· π§))(absβ((π
βπ’) / π’)) β€ πΈ β βπ’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))(absβ((π
βπ’) / π’)) β€ πΈ)) |
439 | 435, 438 | anbi12d 632 |
. . 3
β’ (π§ = π β (((π < π§ β§ ((1 + (πΏ Β· πΈ)) Β· π§) < (π Β· π)) β§ βπ’ β (π§[,]((1 + (πΏ Β· πΈ)) Β· π§))(absβ((π
βπ’) / π’)) β€ πΈ) β ((π < π β§ ((1 + (πΏ Β· πΈ)) Β· π) < (π Β· π)) β§ βπ’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))(absβ((π
βπ’) / π’)) β€ πΈ))) |
440 | 439 | rspcev 3584 |
. 2
β’ ((π β β+
β§ ((π < π β§ ((1 + (πΏ Β· πΈ)) Β· π) < (π Β· π)) β§ βπ’ β (π[,]((1 + (πΏ Β· πΈ)) Β· π))(absβ((π
βπ’) / π’)) β€ πΈ)) β βπ§ β β+ ((π < π§ β§ ((1 + (πΏ Β· πΈ)) Β· π§) < (π Β· π)) β§ βπ’ β (π§[,]((1 + (πΏ Β· πΈ)) Β· π§))(absβ((π
βπ’) / π’)) β€ πΈ)) |
441 | 2, 431, 440 | syl2anc 585 |
1
β’ (π β βπ§ β β+ ((π < π§ β§ ((1 + (πΏ Β· πΈ)) Β· π§) < (π Β· π)) β§ βπ’ β (π§[,]((1 + (πΏ Β· πΈ)) Β· π§))(absβ((π
βπ’) / π’)) β€ πΈ)) |