Step | Hyp | Ref
| Expression |
1 | | pntlem1.u |
. . . . . 6
β’ (π β π β
β+) |
2 | 1 | adantr 481 |
. . . . 5
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π β
β+) |
3 | 2 | rpred 13012 |
. . . 4
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π β β) |
4 | | simprl 769 |
. . . 4
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π½ β β) |
5 | 3, 4 | nndivred 12262 |
. . 3
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π / π½) β β) |
6 | | pntlem1.r |
. . . . . . . . . . 11
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
7 | | pntlem1.a |
. . . . . . . . . . 11
β’ (π β π΄ β
β+) |
8 | | pntlem1.b |
. . . . . . . . . . 11
β’ (π β π΅ β
β+) |
9 | | pntlem1.l |
. . . . . . . . . . 11
β’ (π β πΏ β (0(,)1)) |
10 | | pntlem1.d |
. . . . . . . . . . 11
β’ π· = (π΄ + 1) |
11 | | pntlem1.f |
. . . . . . . . . . 11
β’ πΉ = ((1 β (1 / π·)) Β· ((πΏ / (;32 Β· π΅)) / (π·β2))) |
12 | | pntlem1.u2 |
. . . . . . . . . . 11
β’ (π β π β€ π΄) |
13 | | pntlem1.e |
. . . . . . . . . . 11
β’ πΈ = (π / π·) |
14 | | pntlem1.k |
. . . . . . . . . . 11
β’ πΎ = (expβ(π΅ / πΈ)) |
15 | | pntlem1.y |
. . . . . . . . . . 11
β’ (π β (π β β+ β§ 1 β€
π)) |
16 | | pntlem1.x |
. . . . . . . . . . 11
β’ (π β (π β β+ β§ π < π)) |
17 | | pntlem1.c |
. . . . . . . . . . 11
β’ (π β πΆ β
β+) |
18 | | pntlem1.w |
. . . . . . . . . . 11
β’ π = (((π + (4 / (πΏ Β· πΈ)))β2) + (((π Β· (πΎβ2))β4) + (expβ(((;32 Β· π΅) / ((π β πΈ) Β· (πΏ Β· (πΈβ2)))) Β· ((π Β· 3) + πΆ))))) |
19 | | pntlem1.z |
. . . . . . . . . . 11
β’ (π β π β (π[,)+β)) |
20 | 6, 7, 8, 9, 10, 11, 1, 12, 13, 14, 15, 16, 17, 18, 19 | pntlemb 27089 |
. . . . . . . . . 10
β’ (π β (π β β+ β§ (1 <
π β§ e β€
(ββπ) β§
(ββπ) β€
(π / π)) β§ ((4 / (πΏ Β· πΈ)) β€ (ββπ) β§ (((logβπ) / (logβπΎ)) + 2) β€ (((logβπ) / (logβπΎ)) / 4) β§ ((π Β· 3) + πΆ) β€ (((π β πΈ) Β· ((πΏ Β· (πΈβ2)) / (;32 Β· π΅))) Β· (logβπ))))) |
21 | 20 | simp1d 1142 |
. . . . . . . . 9
β’ (π β π β
β+) |
22 | 21 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π β
β+) |
23 | 4 | nnrpd 13010 |
. . . . . . . 8
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π½ β
β+) |
24 | 22, 23 | rpdivcld 13029 |
. . . . . . 7
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π / π½) β
β+) |
25 | 6 | pntrf 27055 |
. . . . . . . 8
β’ π
:β+βΆβ |
26 | 25 | ffvelcdmi 7082 |
. . . . . . 7
β’ ((π / π½) β β+ β (π
β(π / π½)) β β) |
27 | 24, 26 | syl 17 |
. . . . . 6
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π
β(π / π½)) β β) |
28 | 27, 22 | rerpdivcld 13043 |
. . . . 5
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((π
β(π / π½)) / π) β β) |
29 | 28 | recnd 11238 |
. . . 4
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((π
β(π / π½)) / π) β β) |
30 | 29 | abscld 15379 |
. . 3
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (absβ((π
β(π / π½)) / π)) β β) |
31 | 5, 30 | resubcld 11638 |
. 2
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((π / π½) β (absβ((π
β(π / π½)) / π))) β β) |
32 | 23 | relogcld 26122 |
. 2
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (logβπ½) β β) |
33 | 27 | recnd 11238 |
. . . . . . . . 9
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π
β(π / π½)) β β) |
34 | 22 | rpcnne0d 13021 |
. . . . . . . . 9
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π β β β§ π β 0)) |
35 | 23 | rpcnne0d 13021 |
. . . . . . . . 9
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π½ β β β§ π½ β 0)) |
36 | | divdiv2 11922 |
. . . . . . . . 9
β’ (((π
β(π / π½)) β β β§ (π β β β§ π β 0) β§ (π½ β β β§ π½ β 0)) β ((π
β(π / π½)) / (π / π½)) = (((π
β(π / π½)) Β· π½) / π)) |
37 | 33, 34, 35, 36 | syl3anc 1371 |
. . . . . . . 8
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((π
β(π / π½)) / (π / π½)) = (((π
β(π / π½)) Β· π½) / π)) |
38 | 4 | nncnd 12224 |
. . . . . . . . 9
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π½ β β) |
39 | | div23 11887 |
. . . . . . . . 9
β’ (((π
β(π / π½)) β β β§ π½ β β β§ (π β β β§ π β 0)) β (((π
β(π / π½)) Β· π½) / π) = (((π
β(π / π½)) / π) Β· π½)) |
40 | 33, 38, 34, 39 | syl3anc 1371 |
. . . . . . . 8
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (((π
β(π / π½)) Β· π½) / π) = (((π
β(π / π½)) / π) Β· π½)) |
41 | 37, 40 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((π
β(π / π½)) / (π / π½)) = (((π
β(π / π½)) / π) Β· π½)) |
42 | 41 | fveq2d 6892 |
. . . . . 6
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (absβ((π
β(π / π½)) / (π / π½))) = (absβ(((π
β(π / π½)) / π) Β· π½))) |
43 | 29, 38 | absmuld 15397 |
. . . . . 6
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (absβ(((π
β(π / π½)) / π) Β· π½)) = ((absβ((π
β(π / π½)) / π)) Β· (absβπ½))) |
44 | 23 | rprege0d 13019 |
. . . . . . . 8
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π½ β β β§ 0 β€ π½)) |
45 | | absid 15239 |
. . . . . . . 8
β’ ((π½ β β β§ 0 β€
π½) β (absβπ½) = π½) |
46 | 44, 45 | syl 17 |
. . . . . . 7
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (absβπ½) = π½) |
47 | 46 | oveq2d 7421 |
. . . . . 6
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((absβ((π
β(π / π½)) / π)) Β· (absβπ½)) = ((absβ((π
β(π / π½)) / π)) Β· π½)) |
48 | 42, 43, 47 | 3eqtrd 2776 |
. . . . 5
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (absβ((π
β(π / π½)) / (π / π½))) = ((absβ((π
β(π / π½)) / π)) Β· π½)) |
49 | | fveq2 6888 |
. . . . . . . . 9
β’ (π§ = (π / π½) β (π
βπ§) = (π
β(π / π½))) |
50 | | id 22 |
. . . . . . . . 9
β’ (π§ = (π / π½) β π§ = (π / π½)) |
51 | 49, 50 | oveq12d 7423 |
. . . . . . . 8
β’ (π§ = (π / π½) β ((π
βπ§) / π§) = ((π
β(π / π½)) / (π / π½))) |
52 | 51 | fveq2d 6892 |
. . . . . . 7
β’ (π§ = (π / π½) β (absβ((π
βπ§) / π§)) = (absβ((π
β(π / π½)) / (π / π½)))) |
53 | 52 | breq1d 5157 |
. . . . . 6
β’ (π§ = (π / π½) β ((absβ((π
βπ§) / π§)) β€ π β (absβ((π
β(π / π½)) / (π / π½))) β€ π)) |
54 | | pntlem1.U |
. . . . . . 7
β’ (π β βπ§ β (π[,)+β)(absβ((π
βπ§) / π§)) β€ π) |
55 | 54 | adantr 481 |
. . . . . 6
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β βπ§ β (π[,)+β)(absβ((π
βπ§) / π§)) β€ π) |
56 | 24 | rpred 13012 |
. . . . . . 7
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π / π½) β β) |
57 | | simprr 771 |
. . . . . . . . 9
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π½ β€ (π / π)) |
58 | 23 | rpred 13012 |
. . . . . . . . . 10
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π½ β β) |
59 | 22 | rpred 13012 |
. . . . . . . . . 10
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π β β) |
60 | 15 | simpld 495 |
. . . . . . . . . . 11
β’ (π β π β
β+) |
61 | 60 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π β
β+) |
62 | 58, 59, 61 | lemuldiv2d 13062 |
. . . . . . . . 9
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((π Β· π½) β€ π β π½ β€ (π / π))) |
63 | 57, 62 | mpbird 256 |
. . . . . . . 8
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π Β· π½) β€ π) |
64 | 61 | rpred 13012 |
. . . . . . . . 9
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π β β) |
65 | 64, 59, 23 | lemuldivd 13061 |
. . . . . . . 8
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((π Β· π½) β€ π β π β€ (π / π½))) |
66 | 63, 65 | mpbid 231 |
. . . . . . 7
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β π β€ (π / π½)) |
67 | | elicopnf 13418 |
. . . . . . . 8
β’ (π β β β ((π / π½) β (π[,)+β) β ((π / π½) β β β§ π β€ (π / π½)))) |
68 | 64, 67 | syl 17 |
. . . . . . 7
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((π / π½) β (π[,)+β) β ((π / π½) β β β§ π β€ (π / π½)))) |
69 | 56, 66, 68 | mpbir2and 711 |
. . . . . 6
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (π / π½) β (π[,)+β)) |
70 | 53, 55, 69 | rspcdva 3613 |
. . . . 5
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (absβ((π
β(π / π½)) / (π / π½))) β€ π) |
71 | 48, 70 | eqbrtrrd 5171 |
. . . 4
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β ((absβ((π
β(π / π½)) / π)) Β· π½) β€ π) |
72 | 30, 3, 23 | lemuldivd 13061 |
. . . 4
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (((absβ((π
β(π / π½)) / π)) Β· π½) β€ π β (absβ((π
β(π / π½)) / π)) β€ (π / π½))) |
73 | 71, 72 | mpbid 231 |
. . 3
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (absβ((π
β(π / π½)) / π)) β€ (π / π½)) |
74 | 5, 30 | subge0d 11800 |
. . 3
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (0 β€ ((π / π½) β (absβ((π
β(π / π½)) / π))) β (absβ((π
β(π / π½)) / π)) β€ (π / π½))) |
75 | 73, 74 | mpbird 256 |
. 2
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β 0 β€ ((π / π½) β (absβ((π
β(π / π½)) / π)))) |
76 | | log1 26085 |
. . 3
β’
(logβ1) = 0 |
77 | | nnge1 12236 |
. . . . 5
β’ (π½ β β β 1 β€
π½) |
78 | 77 | ad2antrl 726 |
. . . 4
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β 1 β€ π½) |
79 | | 1rp 12974 |
. . . . 5
β’ 1 β
β+ |
80 | | logleb 26102 |
. . . . 5
β’ ((1
β β+ β§ π½ β β+) β (1 β€
π½ β (logβ1) β€
(logβπ½))) |
81 | 79, 23, 80 | sylancr 587 |
. . . 4
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (1 β€ π½ β (logβ1) β€ (logβπ½))) |
82 | 78, 81 | mpbid 231 |
. . 3
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β (logβ1) β€
(logβπ½)) |
83 | 76, 82 | eqbrtrrid 5183 |
. 2
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β 0 β€ (logβπ½)) |
84 | 31, 32, 75, 83 | mulge0d 11787 |
1
β’ ((π β§ (π½ β β β§ π½ β€ (π / π))) β 0 β€ (((π / π½) β (absβ((π
β(π / π½)) / π))) Β· (logβπ½))) |