Step | Hyp | Ref
| Expression |
1 | | pntlem1.r |
. . 3
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
2 | | pntlem1.a |
. . 3
โข (๐ โ ๐ด โ
โ+) |
3 | | pntlem1.b |
. . 3
โข (๐ โ ๐ต โ
โ+) |
4 | | pntlem1.l |
. . 3
โข (๐ โ ๐ฟ โ (0(,)1)) |
5 | | pntlem1.d |
. . 3
โข ๐ท = (๐ด + 1) |
6 | | pntlem1.f |
. . 3
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
7 | | pntlem1.u |
. . 3
โข (๐ โ ๐ โ
โ+) |
8 | | pntlem1.u2 |
. . 3
โข (๐ โ ๐ โค ๐ด) |
9 | | pntlem1.e |
. . 3
โข ๐ธ = (๐ / ๐ท) |
10 | | pntlem1.k |
. . 3
โข ๐พ = (expโ(๐ต / ๐ธ)) |
11 | | pntlem1.y |
. . 3
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
12 | | pntlem1.x |
. . 3
โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) |
13 | | pntlem1.c |
. . 3
โข (๐ โ ๐ถ โ
โ+) |
14 | | pntlem1.w |
. . 3
โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | pntlema 26982 |
. 2
โข (๐ โ ๐ โ
โ+) |
16 | 2 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ ๐ด โ
โ+) |
17 | 3 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ ๐ต โ
โ+) |
18 | 4 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ ๐ฟ โ (0(,)1)) |
19 | 7 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ ๐ โ
โ+) |
20 | 8 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ ๐ โค ๐ด) |
21 | 11 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ (๐ โ โ+ โง 1 โค
๐)) |
22 | 12 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ (๐ โ โ+ โง ๐ < ๐)) |
23 | 13 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ ๐ถ โ
โ+) |
24 | | simpr 486 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ ๐ฃ โ (๐[,)+โ)) |
25 | | eqid 2732 |
. . . 4
โข
((โโ((logโ๐) / (logโ๐พ))) + 1) = ((โโ((logโ๐) / (logโ๐พ))) + 1) |
26 | | eqid 2732 |
. . . 4
โข
(โโ(((logโ๐ฃ) / (logโ๐พ)) / 2)) = (โโ(((logโ๐ฃ) / (logโ๐พ)) / 2)) |
27 | | pntleme.U |
. . . . 5
โข (๐ โ โ๐ง โ (๐[,)+โ)(absโ((๐
โ๐ง) / ๐ง)) โค ๐) |
28 | 27 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ โ๐ง โ (๐[,)+โ)(absโ((๐
โ๐ง) / ๐ง)) โค ๐) |
29 | | oveq1 7370 |
. . . . . . . . . . 11
โข (๐ = ๐พ โ (๐ ยท ๐ฆ) = (๐พ ยท ๐ฆ)) |
30 | 29 | breq2d 5123 |
. . . . . . . . . 10
โข (๐ = ๐พ โ (((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ) โ ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ))) |
31 | 30 | anbi2d 630 |
. . . . . . . . 9
โข (๐ = ๐พ โ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โ (๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)))) |
32 | 31 | anbi1d 631 |
. . . . . . . 8
โข (๐ = ๐พ โ (((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
33 | 32 | rexbidv 3172 |
. . . . . . 7
โข (๐ = ๐พ โ (โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
34 | 33 | ralbidv 3171 |
. . . . . 6
โข (๐ = ๐พ โ (โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ) โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ))) |
35 | | pntleme.K |
. . . . . 6
โข (๐ โ โ๐ โ (๐พ[,)+โ)โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
36 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 26981 |
. . . . . . . . 9
โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+
โง (๐ธ โ (0(,)1)
โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+))) |
37 | 36 | simp2d 1144 |
. . . . . . . 8
โข (๐ โ ๐พ โ
โ+) |
38 | 37 | rpxrd 12968 |
. . . . . . 7
โข (๐ โ ๐พ โ
โ*) |
39 | | pnfxr 11219 |
. . . . . . . 8
โข +โ
โ โ* |
40 | 39 | a1i 11 |
. . . . . . 7
โข (๐ โ +โ โ
โ*) |
41 | 37 | rpred 12967 |
. . . . . . . 8
โข (๐ โ ๐พ โ โ) |
42 | 41 | ltpnfd 13052 |
. . . . . . 7
โข (๐ โ ๐พ < +โ) |
43 | | lbico1 13329 |
. . . . . . 7
โข ((๐พ โ โ*
โง +โ โ โ* โง ๐พ < +โ) โ ๐พ โ (๐พ[,)+โ)) |
44 | 38, 40, 42, 43 | syl3anc 1372 |
. . . . . 6
โข (๐ โ ๐พ โ (๐พ[,)+โ)) |
45 | 34, 35, 44 | rspcdva 3584 |
. . . . 5
โข (๐ โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
46 | 45 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ โ๐ฆ โ (๐(,)+โ)โ๐ง โ โ+ ((๐ฆ < ๐ง โง ((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง) < (๐พ ยท ๐ฆ)) โง โ๐ข โ (๐ง[,]((1 + (๐ฟ ยท ๐ธ)) ยท ๐ง))(absโ((๐
โ๐ข) / ๐ข)) โค ๐ธ)) |
47 | | pntleme.C |
. . . . 5
โข (๐ โ โ๐ง โ (1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐ถ) |
48 | 47 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ โ๐ง โ
(1(,)+โ)((((absโ(๐
โ๐ง)) ยท (logโ๐ง)) โ ((2 / (logโ๐ง)) ยท ฮฃ๐ โ
(1...(โโ(๐ง /
๐)))((absโ(๐
โ(๐ง / ๐))) ยท (logโ๐)))) / ๐ง) โค ๐ถ) |
49 | 1, 16, 17, 18, 5, 6, 19, 20, 9, 10, 21, 22, 23, 14, 24, 25, 26, 28, 46, 48 | pntlemo 26993 |
. . 3
โข ((๐ โง ๐ฃ โ (๐[,)+โ)) โ (absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) |
50 | 49 | ralrimiva 3140 |
. 2
โข (๐ โ โ๐ฃ โ (๐[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) |
51 | | oveq1 7370 |
. . . 4
โข (๐ค = ๐ โ (๐ค[,)+โ) = (๐[,)+โ)) |
52 | 51 | raleqdv 3312 |
. . 3
โข (๐ค = ๐ โ (โ๐ฃ โ (๐ค[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3))) โ โ๐ฃ โ (๐[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3))))) |
53 | 52 | rspcev 3583 |
. 2
โข ((๐ โ โ+
โง โ๐ฃ โ
(๐[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) |
54 | 15, 50, 53 | syl2anc 585 |
1
โข (๐ โ โ๐ค โ โ+ โ๐ฃ โ (๐ค[,)+โ)(absโ((๐
โ๐ฃ) / ๐ฃ)) โค (๐ โ (๐น ยท (๐โ3)))) |