Step | Hyp | Ref
| Expression |
1 | | ostth2.3 |
. . . . 5
β’ (π β 1 < (πΉβπ)) |
2 | | 1re 11163 |
. . . . . 6
β’ 1 β
β |
3 | | ostth.1 |
. . . . . . 7
β’ (π β πΉ β π΄) |
4 | | ostth2.2 |
. . . . . . . . . 10
β’ (π β π β
(β€β₯β2)) |
5 | | eluz2b2 12854 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
6 | 4, 5 | sylib 217 |
. . . . . . . . 9
β’ (π β (π β β β§ 1 < π)) |
7 | 6 | simpld 496 |
. . . . . . . 8
β’ (π β π β β) |
8 | | nnq 12895 |
. . . . . . . 8
β’ (π β β β π β
β) |
9 | 7, 8 | syl 17 |
. . . . . . 7
β’ (π β π β β) |
10 | | qabsabv.a |
. . . . . . . 8
β’ π΄ = (AbsValβπ) |
11 | | qrng.q |
. . . . . . . . 9
β’ π = (βfld
βΎs β) |
12 | 11 | qrngbas 26990 |
. . . . . . . 8
β’ β =
(Baseβπ) |
13 | 10, 12 | abvcl 20326 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
14 | 3, 9, 13 | syl2anc 585 |
. . . . . 6
β’ (π β (πΉβπ) β β) |
15 | | ltnle 11242 |
. . . . . 6
β’ ((1
β β β§ (πΉβπ) β β) β (1 < (πΉβπ) β Β¬ (πΉβπ) β€ 1)) |
16 | 2, 14, 15 | sylancr 588 |
. . . . 5
β’ (π β (1 < (πΉβπ) β Β¬ (πΉβπ) β€ 1)) |
17 | 1, 16 | mpbid 231 |
. . . 4
β’ (π β Β¬ (πΉβπ) β€ 1) |
18 | | ostth2.7 |
. . . . . . . . . . . . 13
β’ π = if((πΉβπ) β€ 1, 1, (πΉβπ)) |
19 | | ostth2.5 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β
(β€β₯β2)) |
20 | | eluz2b2 12854 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
21 | 19, 20 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β β β§ 1 < π)) |
22 | 21 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
23 | | nnq 12895 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
25 | 10, 12 | abvcl 20326 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
26 | 3, 24, 25 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (πΉβπ) β β) |
27 | | ifcl 4535 |
. . . . . . . . . . . . . 14
β’ ((1
β β β§ (πΉβπ) β β) β if((πΉβπ) β€ 1, 1, (πΉβπ)) β β) |
28 | 2, 26, 27 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π β if((πΉβπ) β€ 1, 1, (πΉβπ)) β β) |
29 | 18, 28 | eqeltrid 2838 |
. . . . . . . . . . . 12
β’ (π β π β β) |
30 | | 0red 11166 |
. . . . . . . . . . . . 13
β’ (π β 0 β
β) |
31 | 2 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 1 β
β) |
32 | | 0lt1 11685 |
. . . . . . . . . . . . . 14
β’ 0 <
1 |
33 | 32 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 0 < 1) |
34 | | max2 13115 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β β β§ 1 β β)
β 1 β€ if((πΉβπ) β€ 1, 1, (πΉβπ))) |
35 | 26, 2, 34 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (π β 1 β€ if((πΉβπ) β€ 1, 1, (πΉβπ))) |
36 | 35, 18 | breqtrrdi 5151 |
. . . . . . . . . . . . 13
β’ (π β 1 β€ π) |
37 | 30, 31, 29, 33, 36 | ltletrd 11323 |
. . . . . . . . . . . 12
β’ (π β 0 < π) |
38 | 29, 37 | elrpd 12962 |
. . . . . . . . . . 11
β’ (π β π β
β+) |
39 | | ostth2.8 |
. . . . . . . . . . . 12
β’ π = ((logβπ) / (logβπ)) |
40 | 7 | nnrpd 12963 |
. . . . . . . . . . . . . 14
β’ (π β π β
β+) |
41 | 40 | relogcld 26001 |
. . . . . . . . . . . . 13
β’ (π β (logβπ) β
β) |
42 | 22 | nnred 12176 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
43 | 21 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β 1 < π) |
44 | 42, 43 | rplogcld 26007 |
. . . . . . . . . . . . 13
β’ (π β (logβπ) β
β+) |
45 | 41, 44 | rerpdivcld 12996 |
. . . . . . . . . . . 12
β’ (π β ((logβπ) / (logβπ)) β β) |
46 | 39, 45 | eqeltrid 2838 |
. . . . . . . . . . 11
β’ (π β π β β) |
47 | 38, 46 | rpcxpcld 26110 |
. . . . . . . . . 10
β’ (π β (πβππ) β
β+) |
48 | 14, 47 | rerpdivcld 12996 |
. . . . . . . . 9
β’ (π β ((πΉβπ) / (πβππ)) β β) |
49 | 42, 29 | remulcld 11193 |
. . . . . . . . . 10
β’ (π β (π Β· π) β β) |
50 | | peano2re 11336 |
. . . . . . . . . . 11
β’ (π β β β (π + 1) β
β) |
51 | 46, 50 | syl 17 |
. . . . . . . . . 10
β’ (π β (π + 1) β β) |
52 | 49, 51 | remulcld 11193 |
. . . . . . . . 9
β’ (π β ((π Β· π) Β· (π + 1)) β β) |
53 | | padic.j |
. . . . . . . . . 10
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
54 | | ostth.k |
. . . . . . . . . 10
β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) |
55 | | ostth2.4 |
. . . . . . . . . 10
β’ π
= ((logβ(πΉβπ)) / (logβπ)) |
56 | | ostth2.6 |
. . . . . . . . . 10
β’ π = ((logβ(πΉβπ)) / (logβπ)) |
57 | 11, 10, 53, 54, 3, 4, 1, 55, 19, 56, 18, 39 | ostth2lem3 27006 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((πΉβπ) / (πβππ))βπ) β€ (π Β· ((π Β· π) Β· (π + 1)))) |
58 | 48, 52, 57 | ostth2lem1 26989 |
. . . . . . . 8
β’ (π β ((πΉβπ) / (πβππ)) β€ 1) |
59 | 14, 31, 47 | ledivmuld 13018 |
. . . . . . . 8
β’ (π β (((πΉβπ) / (πβππ)) β€ 1 β (πΉβπ) β€ ((πβππ) Β· 1))) |
60 | 58, 59 | mpbid 231 |
. . . . . . 7
β’ (π β (πΉβπ) β€ ((πβππ) Β· 1)) |
61 | 47 | rpcnd 12967 |
. . . . . . . 8
β’ (π β (πβππ) β β) |
62 | 61 | mulridd 11180 |
. . . . . . 7
β’ (π β ((πβππ) Β· 1) = (πβππ)) |
63 | 60, 62 | breqtrd 5135 |
. . . . . 6
β’ (π β (πΉβπ) β€ (πβππ)) |
64 | 63 | adantr 482 |
. . . . 5
β’ ((π β§ (πΉβπ) β€ 1) β (πΉβπ) β€ (πβππ)) |
65 | | iftrue 4496 |
. . . . . . . 8
β’ ((πΉβπ) β€ 1 β if((πΉβπ) β€ 1, 1, (πΉβπ)) = 1) |
66 | 18, 65 | eqtrid 2785 |
. . . . . . 7
β’ ((πΉβπ) β€ 1 β π = 1) |
67 | 66 | oveq1d 7376 |
. . . . . 6
β’ ((πΉβπ) β€ 1 β (πβππ) = (1βππ)) |
68 | 46 | recnd 11191 |
. . . . . . 7
β’ (π β π β β) |
69 | 68 | 1cxpd 26085 |
. . . . . 6
β’ (π β
(1βππ) = 1) |
70 | 67, 69 | sylan9eqr 2795 |
. . . . 5
β’ ((π β§ (πΉβπ) β€ 1) β (πβππ) = 1) |
71 | 64, 70 | breqtrd 5135 |
. . . 4
β’ ((π β§ (πΉβπ) β€ 1) β (πΉβπ) β€ 1) |
72 | 17, 71 | mtand 815 |
. . 3
β’ (π β Β¬ (πΉβπ) β€ 1) |
73 | | ltnle 11242 |
. . . 4
β’ ((1
β β β§ (πΉβπ) β β) β (1 < (πΉβπ) β Β¬ (πΉβπ) β€ 1)) |
74 | 2, 26, 73 | sylancr 588 |
. . 3
β’ (π β (1 < (πΉβπ) β Β¬ (πΉβπ) β€ 1)) |
75 | 72, 74 | mpbird 257 |
. 2
β’ (π β 1 < (πΉβπ)) |
76 | 30, 31, 14, 33, 1 | lttrd 11324 |
. . . . . . . . 9
β’ (π β 0 < (πΉβπ)) |
77 | 14, 76 | elrpd 12962 |
. . . . . . . 8
β’ (π β (πΉβπ) β
β+) |
78 | 77 | reeflogd 26002 |
. . . . . . 7
β’ (π β
(expβ(logβ(πΉβπ))) = (πΉβπ)) |
79 | | iffalse 4499 |
. . . . . . . . . . 11
β’ (Β¬
(πΉβπ) β€ 1 β if((πΉβπ) β€ 1, 1, (πΉβπ)) = (πΉβπ)) |
80 | 18, 79 | eqtrid 2785 |
. . . . . . . . . 10
β’ (Β¬
(πΉβπ) β€ 1 β π = (πΉβπ)) |
81 | 72, 80 | syl 17 |
. . . . . . . . 9
β’ (π β π = (πΉβπ)) |
82 | 81 | oveq1d 7376 |
. . . . . . . 8
β’ (π β (πβππ) = ((πΉβπ)βππ)) |
83 | 26 | recnd 11191 |
. . . . . . . . 9
β’ (π β (πΉβπ) β β) |
84 | 30, 31, 26, 33, 75 | lttrd 11324 |
. . . . . . . . . . 11
β’ (π β 0 < (πΉβπ)) |
85 | 26, 84 | elrpd 12962 |
. . . . . . . . . 10
β’ (π β (πΉβπ) β
β+) |
86 | 85 | rpne0d 12970 |
. . . . . . . . 9
β’ (π β (πΉβπ) β 0) |
87 | 83, 86, 68 | cxpefd 26090 |
. . . . . . . 8
β’ (π β ((πΉβπ)βππ) = (expβ(π Β· (logβ(πΉβπ))))) |
88 | 82, 87 | eqtr2d 2774 |
. . . . . . 7
β’ (π β (expβ(π Β· (logβ(πΉβπ)))) = (πβππ)) |
89 | 63, 78, 88 | 3brtr4d 5141 |
. . . . . 6
β’ (π β
(expβ(logβ(πΉβπ))) β€ (expβ(π Β· (logβ(πΉβπ))))) |
90 | 77 | relogcld 26001 |
. . . . . . 7
β’ (π β (logβ(πΉβπ)) β β) |
91 | 85 | relogcld 26001 |
. . . . . . . 8
β’ (π β (logβ(πΉβπ)) β β) |
92 | 46, 91 | remulcld 11193 |
. . . . . . 7
β’ (π β (π Β· (logβ(πΉβπ))) β β) |
93 | | efle 16008 |
. . . . . . 7
β’
(((logβ(πΉβπ)) β β β§ (π Β· (logβ(πΉβπ))) β β) β
((logβ(πΉβπ)) β€ (π Β· (logβ(πΉβπ))) β (expβ(logβ(πΉβπ))) β€ (expβ(π Β· (logβ(πΉβπ)))))) |
94 | 90, 92, 93 | syl2anc 585 |
. . . . . 6
β’ (π β ((logβ(πΉβπ)) β€ (π Β· (logβ(πΉβπ))) β (expβ(logβ(πΉβπ))) β€ (expβ(π Β· (logβ(πΉβπ)))))) |
95 | 89, 94 | mpbird 257 |
. . . . 5
β’ (π β (logβ(πΉβπ)) β€ (π Β· (logβ(πΉβπ)))) |
96 | 41 | recnd 11191 |
. . . . . . . 8
β’ (π β (logβπ) β
β) |
97 | 91 | recnd 11191 |
. . . . . . . 8
β’ (π β (logβ(πΉβπ)) β β) |
98 | 44 | rpcnd 12967 |
. . . . . . . 8
β’ (π β (logβπ) β
β) |
99 | 44 | rpne0d 12970 |
. . . . . . . 8
β’ (π β (logβπ) β 0) |
100 | 96, 97, 98, 99 | div12d 11975 |
. . . . . . 7
β’ (π β ((logβπ) Β· ((logβ(πΉβπ)) / (logβπ))) = ((logβ(πΉβπ)) Β· ((logβπ) / (logβπ)))) |
101 | 39 | oveq2i 7372 |
. . . . . . 7
β’
((logβ(πΉβπ)) Β· π) = ((logβ(πΉβπ)) Β· ((logβπ) / (logβπ))) |
102 | 100, 101 | eqtr4di 2791 |
. . . . . 6
β’ (π β ((logβπ) Β· ((logβ(πΉβπ)) / (logβπ))) = ((logβ(πΉβπ)) Β· π)) |
103 | 97, 68 | mulcomd 11184 |
. . . . . 6
β’ (π β ((logβ(πΉβπ)) Β· π) = (π Β· (logβ(πΉβπ)))) |
104 | 102, 103 | eqtrd 2773 |
. . . . 5
β’ (π β ((logβπ) Β· ((logβ(πΉβπ)) / (logβπ))) = (π Β· (logβ(πΉβπ)))) |
105 | 95, 104 | breqtrrd 5137 |
. . . 4
β’ (π β (logβ(πΉβπ)) β€ ((logβπ) Β· ((logβ(πΉβπ)) / (logβπ)))) |
106 | 91, 44 | rerpdivcld 12996 |
. . . . 5
β’ (π β ((logβ(πΉβπ)) / (logβπ)) β β) |
107 | 7 | nnred 12176 |
. . . . . 6
β’ (π β π β β) |
108 | 6 | simprd 497 |
. . . . . 6
β’ (π β 1 < π) |
109 | 107, 108 | rplogcld 26007 |
. . . . 5
β’ (π β (logβπ) β
β+) |
110 | 90, 106, 109 | ledivmuld 13018 |
. . . 4
β’ (π β (((logβ(πΉβπ)) / (logβπ)) β€ ((logβ(πΉβπ)) / (logβπ)) β (logβ(πΉβπ)) β€ ((logβπ) Β· ((logβ(πΉβπ)) / (logβπ))))) |
111 | 105, 110 | mpbird 257 |
. . 3
β’ (π β ((logβ(πΉβπ)) / (logβπ)) β€ ((logβ(πΉβπ)) / (logβπ))) |
112 | 111, 55, 56 | 3brtr4g 5143 |
. 2
β’ (π β π
β€ π) |
113 | 75, 112 | jca 513 |
1
β’ (π β (1 < (πΉβπ) β§ π
β€ π)) |