Step | Hyp | Ref
| Expression |
1 | | breq2 5152 |
. . . . . . 7
โข (๐ง = ๐ฅ โ (๐ฆ < ๐ง โ ๐ฆ < ๐ฅ)) |
2 | | oveq2 7416 |
. . . . . . . 8
โข (๐ง = ๐ฅ โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) = ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ)) |
3 | 2 | breq1d 5158 |
. . . . . . 7
โข (๐ง = ๐ฅ โ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ) โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท ๐ฆ))) |
4 | 1, 3 | anbi12d 631 |
. . . . . 6
โข (๐ง = ๐ฅ โ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โ (๐ฆ < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท ๐ฆ)))) |
5 | | id 22 |
. . . . . . . 8
โข (๐ง = ๐ฅ โ ๐ง = ๐ฅ) |
6 | 5, 2 | oveq12d 7426 |
. . . . . . 7
โข (๐ง = ๐ฅ โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง)) = (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))) |
7 | 6 | raleqdv 3325 |
. . . . . 6
โข (๐ง = ๐ฅ โ (โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ โ โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
8 | 4, 7 | anbi12d 631 |
. . . . 5
โข (๐ง = ๐ฅ โ (((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ ((๐ฆ < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
9 | 8 | cbvrexvw 3235 |
. . . 4
โข
(โ๐ง โ
โ+ ((๐ฆ
< ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ฅ โ โ+ ((๐ฆ < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
10 | | breq1 5151 |
. . . . . . 7
โข (๐ฆ = (๐พโ๐ฝ) โ (๐ฆ < ๐ฅ โ (๐พโ๐ฝ) < ๐ฅ)) |
11 | | oveq2 7416 |
. . . . . . . 8
โข (๐ฆ = (๐พโ๐ฝ) โ (๐พ ยท ๐ฆ) = (๐พ ยท (๐พโ๐ฝ))) |
12 | 11 | breq2d 5160 |
. . . . . . 7
โข (๐ฆ = (๐พโ๐ฝ) โ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท ๐ฆ) โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ)))) |
13 | 10, 12 | anbi12d 631 |
. . . . . 6
โข (๐ฆ = (๐พโ๐ฝ) โ ((๐ฆ < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท ๐ฆ)) โ ((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))))) |
14 | 13 | anbi1d 630 |
. . . . 5
โข (๐ฆ = (๐พโ๐ฝ) โ (((๐ฆ < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
15 | 14 | rexbidv 3178 |
. . . 4
โข (๐ฆ = (๐พโ๐ฝ) โ (โ๐ฅ โ โ+ ((๐ฆ < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ฅ โ โ+ (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
16 | 9, 15 | bitrid 282 |
. . 3
โข (๐ฆ = (๐พโ๐ฝ) โ (โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ฅ โ โ+ (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
17 | | pntlem1.K |
. . . 4
โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
18 | 17 | adantr 481 |
. . 3
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
19 | | pntlem1.r |
. . . . . . . 8
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
20 | | pntlem1.a |
. . . . . . . 8
โข (๐ โ ๐ด โ
โ+) |
21 | | pntlem1.b |
. . . . . . . 8
โข (๐ โ ๐ต โ
โ+) |
22 | | pntlem1.l |
. . . . . . . 8
โข (๐ โ ๐ฟ โ (0(,)1)) |
23 | | pntlem1.d |
. . . . . . . 8
โข ๐ท = (๐ด + 1) |
24 | | pntlem1.f |
. . . . . . . 8
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
25 | | pntlem1.u |
. . . . . . . 8
โข (๐ โ ๐ โ
โ+) |
26 | | pntlem1.u2 |
. . . . . . . 8
โข (๐ โ ๐ โค ๐ด) |
27 | | pntlem1.e |
. . . . . . . 8
โข ๐ธ = (๐ / ๐ท) |
28 | | pntlem1.k |
. . . . . . . 8
โข ๐พ = (expโ(๐ต / ๐ธ)) |
29 | 19, 20, 21, 22, 23, 24, 25, 26, 27, 28 | pntlemc 27095 |
. . . . . . 7
โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+
โง (๐ธ โ (0(,)1)
โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+))) |
30 | 29 | simp2d 1143 |
. . . . . 6
โข (๐ โ ๐พ โ
โ+) |
31 | | elfzoelz 13631 |
. . . . . 6
โข (๐ฝ โ (๐..^๐) โ ๐ฝ โ โค) |
32 | | rpexpcl 14045 |
. . . . . 6
โข ((๐พ โ โ+
โง ๐ฝ โ โค)
โ (๐พโ๐ฝ) โ
โ+) |
33 | 30, 31, 32 | syl2an 596 |
. . . . 5
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ (๐พโ๐ฝ) โ
โ+) |
34 | 33 | rpred 13015 |
. . . 4
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ (๐พโ๐ฝ) โ โ) |
35 | | elfzofz 13647 |
. . . . . 6
โข (๐ฝ โ (๐..^๐) โ ๐ฝ โ (๐...๐)) |
36 | | pntlem1.y |
. . . . . . 7
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
37 | | pntlem1.x |
. . . . . . 7
โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) |
38 | | pntlem1.c |
. . . . . . 7
โข (๐ โ ๐ถ โ
โ+) |
39 | | pntlem1.w |
. . . . . . 7
โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
40 | | pntlem1.z |
. . . . . . 7
โข (๐ โ ๐ โ (๐[,)+โ)) |
41 | | pntlem1.m |
. . . . . . 7
โข ๐ =
((โโ((logโ๐) / (logโ๐พ))) + 1) |
42 | | pntlem1.n |
. . . . . . 7
โข ๐ =
(โโ(((logโ๐) / (logโ๐พ)) / 2)) |
43 | 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 36, 37, 38, 39, 40, 41, 42 | pntlemh 27099 |
. . . . . 6
โข ((๐ โง ๐ฝ โ (๐...๐)) โ (๐ < (๐พโ๐ฝ) โง (๐พโ๐ฝ) โค (โโ๐))) |
44 | 35, 43 | sylan2 593 |
. . . . 5
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ (๐ < (๐พโ๐ฝ) โง (๐พโ๐ฝ) โค (โโ๐))) |
45 | 44 | simpld 495 |
. . . 4
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ ๐ < (๐พโ๐ฝ)) |
46 | 37 | simpld 495 |
. . . . . 6
โข (๐ โ ๐ โ
โ+) |
47 | 46 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ ๐ โ
โ+) |
48 | | rpxr 12982 |
. . . . 5
โข (๐ โ โ+
โ ๐ โ
โ*) |
49 | | elioopnf 13419 |
. . . . 5
โข (๐ โ โ*
โ ((๐พโ๐ฝ) โ (๐(,)+โ) โ ((๐พโ๐ฝ) โ โ โง ๐ < (๐พโ๐ฝ)))) |
50 | 47, 48, 49 | 3syl 18 |
. . . 4
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ ((๐พโ๐ฝ) โ (๐(,)+โ) โ ((๐พโ๐ฝ) โ โ โง ๐ < (๐พโ๐ฝ)))) |
51 | 34, 45, 50 | mpbir2and 711 |
. . 3
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ (๐พโ๐ฝ) โ (๐(,)+โ)) |
52 | 16, 18, 51 | rspcdva 3613 |
. 2
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ โ๐ฅ โ โ+ (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
53 | 20 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ด โ
โ+) |
54 | 21 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ต โ
โ+) |
55 | 22 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ฟ โ (0(,)1)) |
56 | 25 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ โ
โ+) |
57 | 26 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ โค ๐ด) |
58 | 36 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ (๐ โ โ+ โง 1 โค
๐)) |
59 | 37 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ (๐ โ โ+ โง ๐ < ๐)) |
60 | 38 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ถ โ
โ+) |
61 | 40 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ โ (๐[,)+โ)) |
62 | | pntlem1.U |
. . . 4
โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐
โ๐ง) / ๐ง)) โค ๐) |
63 | 62 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ โ๐ง โ (๐[,)+โ)(absโ((๐
โ๐ง) / ๐ง)) โค ๐) |
64 | 17 | ad2antrr 724 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
65 | | pntlem1.o |
. . 3
โข ๐ = (((โโ(๐ / (๐พโ(๐ฝ + 1)))) + 1)...(โโ(๐ / (๐พโ๐ฝ)))) |
66 | | simprl 769 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ฅ โ โ+) |
67 | | simprr 771 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
68 | | simplr 767 |
. . 3
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ๐ฝ โ (๐..^๐)) |
69 | | eqid 2732 |
. . 3
โข
(((โโ(๐
/ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))) + 1)...(โโ(๐ / ๐ฅ))) = (((โโ(๐ / ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))) + 1)...(โโ(๐ / ๐ฅ))) |
70 | 19, 53, 54, 55, 23, 24, 56, 57, 27, 28, 58, 59, 60, 39, 61, 41, 42, 63, 64, 65, 66, 67, 68, 69 | pntlemj 27103 |
. 2
โข (((๐ โง ๐ฝ โ (๐..^๐)) โง (๐ฅ โ โ+ โง (((๐พโ๐ฝ) < ๐ฅ โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ) < (๐พ ยท (๐พโ๐ฝ))) โง โ๐ข โ (๐ฅ[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ฅ))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ฮฃ๐ โ ๐ (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |
71 | 52, 70 | rexlimddv 3161 |
1
โข ((๐ โง ๐ฝ โ (๐..^๐)) โ ((๐ โ ๐ธ) ยท (((๐ฟ ยท ๐ธ) / 8) ยท (logโ๐))) โค ฮฃ๐ โ ๐ (((๐ / ๐) โ (absโ((๐
โ(๐ / ๐)) / ๐))) ยท (logโ๐))) |