Step | Hyp | Ref
| Expression |
1 | | ostth2.4 |
. . . . 5
β’ π
= ((logβ(πΉβπ)) / (logβπ)) |
2 | | ostth.1 |
. . . . . . . 8
β’ (π β πΉ β π΄) |
3 | | ostth2.2 |
. . . . . . . . . . 11
β’ (π β π β
(β€β₯β2)) |
4 | | eluz2b2 12854 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
5 | 3, 4 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π β β β§ 1 < π)) |
6 | 5 | simpld 496 |
. . . . . . . . 9
β’ (π β π β β) |
7 | | nnq 12895 |
. . . . . . . . 9
β’ (π β β β π β
β) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
β’ (π β π β β) |
9 | | qabsabv.a |
. . . . . . . . 9
β’ π΄ = (AbsValβπ) |
10 | | qrng.q |
. . . . . . . . . 10
β’ π = (βfld
βΎs β) |
11 | 10 | qrngbas 26990 |
. . . . . . . . 9
β’ β =
(Baseβπ) |
12 | 9, 11 | abvcl 20326 |
. . . . . . . 8
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
13 | 2, 8, 12 | syl2anc 585 |
. . . . . . 7
β’ (π β (πΉβπ) β β) |
14 | | ostth2.3 |
. . . . . . 7
β’ (π β 1 < (πΉβπ)) |
15 | 13, 14 | rplogcld 26007 |
. . . . . 6
β’ (π β (logβ(πΉβπ)) β
β+) |
16 | 6 | nnred 12176 |
. . . . . . 7
β’ (π β π β β) |
17 | 5 | simprd 497 |
. . . . . . 7
β’ (π β 1 < π) |
18 | 16, 17 | rplogcld 26007 |
. . . . . 6
β’ (π β (logβπ) β
β+) |
19 | 15, 18 | rpdivcld 12982 |
. . . . 5
β’ (π β ((logβ(πΉβπ)) / (logβπ)) β
β+) |
20 | 1, 19 | eqeltrid 2838 |
. . . 4
β’ (π β π
β
β+) |
21 | 20 | rpred 12965 |
. . 3
β’ (π β π
β β) |
22 | 20 | rpgt0d 12968 |
. . 3
β’ (π β 0 < π
) |
23 | 6 | nnnn0d 12481 |
. . . . . . . . 9
β’ (π β π β
β0) |
24 | 10, 9 | qabvle 26996 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ π β β0) β (πΉβπ) β€ π) |
25 | 2, 23, 24 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΉβπ) β€ π) |
26 | 6 | nnne0d 12211 |
. . . . . . . . . . 11
β’ (π β π β 0) |
27 | 10 | qrng0 26992 |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ) |
28 | 9, 11, 27 | abvgt0 20330 |
. . . . . . . . . . 11
β’ ((πΉ β π΄ β§ π β β β§ π β 0) β 0 < (πΉβπ)) |
29 | 2, 8, 26, 28 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β 0 < (πΉβπ)) |
30 | 13, 29 | elrpd 12962 |
. . . . . . . . 9
β’ (π β (πΉβπ) β
β+) |
31 | 30 | reeflogd 26002 |
. . . . . . . 8
β’ (π β
(expβ(logβ(πΉβπ))) = (πΉβπ)) |
32 | 6 | nnrpd 12963 |
. . . . . . . . 9
β’ (π β π β
β+) |
33 | 32 | reeflogd 26002 |
. . . . . . . 8
β’ (π β
(expβ(logβπ)) =
π) |
34 | 25, 31, 33 | 3brtr4d 5141 |
. . . . . . 7
β’ (π β
(expβ(logβ(πΉβπ))) β€ (expβ(logβπ))) |
35 | 15 | rpred 12965 |
. . . . . . . 8
β’ (π β (logβ(πΉβπ)) β β) |
36 | 32 | relogcld 26001 |
. . . . . . . 8
β’ (π β (logβπ) β
β) |
37 | | efle 16008 |
. . . . . . . 8
β’
(((logβ(πΉβπ)) β β β§ (logβπ) β β) β
((logβ(πΉβπ)) β€ (logβπ) β
(expβ(logβ(πΉβπ))) β€ (expβ(logβπ)))) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . . 7
β’ (π β ((logβ(πΉβπ)) β€ (logβπ) β (expβ(logβ(πΉβπ))) β€ (expβ(logβπ)))) |
39 | 34, 38 | mpbird 257 |
. . . . . 6
β’ (π β (logβ(πΉβπ)) β€ (logβπ)) |
40 | 18 | rpcnd 12967 |
. . . . . . 7
β’ (π β (logβπ) β
β) |
41 | 40 | mulridd 11180 |
. . . . . 6
β’ (π β ((logβπ) Β· 1) = (logβπ)) |
42 | 39, 41 | breqtrrd 5137 |
. . . . 5
β’ (π β (logβ(πΉβπ)) β€ ((logβπ) Β· 1)) |
43 | | 1red 11164 |
. . . . . 6
β’ (π β 1 β
β) |
44 | 35, 43, 18 | ledivmuld 13018 |
. . . . 5
β’ (π β (((logβ(πΉβπ)) / (logβπ)) β€ 1 β (logβ(πΉβπ)) β€ ((logβπ) Β· 1))) |
45 | 42, 44 | mpbird 257 |
. . . 4
β’ (π β ((logβ(πΉβπ)) / (logβπ)) β€ 1) |
46 | 1, 45 | eqbrtrid 5144 |
. . 3
β’ (π β π
β€ 1) |
47 | | 0xr 11210 |
. . . 4
β’ 0 β
β* |
48 | | 1re 11163 |
. . . 4
β’ 1 β
β |
49 | | elioc2 13336 |
. . . 4
β’ ((0
β β* β§ 1 β β) β (π
β (0(,]1) β (π
β β β§ 0 < π
β§ π
β€ 1))) |
50 | 47, 48, 49 | mp2an 691 |
. . 3
β’ (π
β (0(,]1) β (π
β β β§ 0 <
π
β§ π
β€ 1)) |
51 | 21, 22, 46, 50 | syl3anbrc 1344 |
. 2
β’ (π β π
β (0(,]1)) |
52 | 10, 9 | qabsabv 27000 |
. . . 4
β’ (abs
βΎ β) β π΄ |
53 | | fvres 6865 |
. . . . . . . 8
β’ (π¦ β β β ((abs
βΎ β)βπ¦) =
(absβπ¦)) |
54 | 53 | oveq1d 7376 |
. . . . . . 7
β’ (π¦ β β β (((abs
βΎ β)βπ¦)βππ
) = ((absβπ¦)βππ
)) |
55 | 54 | mpteq2ia 5212 |
. . . . . 6
β’ (π¦ β β β¦ (((abs
βΎ β)βπ¦)βππ
)) = (π¦ β β β¦ ((absβπ¦)βππ
)) |
56 | 55 | eqcomi 2742 |
. . . . 5
β’ (π¦ β β β¦
((absβπ¦)βππ
)) = (π¦ β β β¦ (((abs βΎ
β)βπ¦)βππ
)) |
57 | 9, 11, 56 | abvcxp 26986 |
. . . 4
β’ (((abs
βΎ β) β π΄
β§ π
β (0(,]1))
β (π¦ β β
β¦ ((absβπ¦)βππ
)) β π΄) |
58 | 52, 51, 57 | sylancr 588 |
. . 3
β’ (π β (π¦ β β β¦ ((absβπ¦)βππ
)) β π΄) |
59 | | eluzelz 12781 |
. . . . . 6
β’ (π§ β
(β€β₯β2) β π§ β β€) |
60 | | zq 12887 |
. . . . . 6
β’ (π§ β β€ β π§ β
β) |
61 | | fveq2 6846 |
. . . . . . . 8
β’ (π¦ = π§ β (absβπ¦) = (absβπ§)) |
62 | 61 | oveq1d 7376 |
. . . . . . 7
β’ (π¦ = π§ β ((absβπ¦)βππ
) = ((absβπ§)βππ
)) |
63 | | eqid 2733 |
. . . . . . 7
β’ (π¦ β β β¦
((absβπ¦)βππ
)) = (π¦ β β β¦ ((absβπ¦)βππ
)) |
64 | | ovex 7394 |
. . . . . . 7
β’
((absβπ§)βππ
) β V |
65 | 62, 63, 64 | fvmpt 6952 |
. . . . . 6
β’ (π§ β β β ((π¦ β β β¦
((absβπ¦)βππ
))βπ§) = ((absβπ§)βππ
)) |
66 | 59, 60, 65 | 3syl 18 |
. . . . 5
β’ (π§ β
(β€β₯β2) β ((π¦ β β β¦ ((absβπ¦)βππ
))βπ§) = ((absβπ§)βππ
)) |
67 | 66 | adantl 483 |
. . . 4
β’ ((π β§ π§ β (β€β₯β2))
β ((π¦ β β
β¦ ((absβπ¦)βππ
))βπ§) = ((absβπ§)βππ
)) |
68 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
(β€β₯β2)) |
69 | | eluz2b2 12854 |
. . . . . . . . 9
β’ (π§ β
(β€β₯β2) β (π§ β β β§ 1 < π§)) |
70 | 68, 69 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π§ β (β€β₯β2))
β (π§ β β
β§ 1 < π§)) |
71 | 70 | simpld 496 |
. . . . . . 7
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
β) |
72 | 71 | nnred 12176 |
. . . . . 6
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
β) |
73 | 71 | nnnn0d 12481 |
. . . . . . 7
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
β0) |
74 | 73 | nn0ge0d 12484 |
. . . . . 6
β’ ((π β§ π§ β (β€β₯β2))
β 0 β€ π§) |
75 | 72, 74 | absidd 15316 |
. . . . 5
β’ ((π β§ π§ β (β€β₯β2))
β (absβπ§) =
π§) |
76 | 75 | oveq1d 7376 |
. . . 4
β’ ((π β§ π§ β (β€β₯β2))
β ((absβπ§)βππ
) = (π§βππ
)) |
77 | 72 | recnd 11191 |
. . . . . 6
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
β) |
78 | 71 | nnne0d 12211 |
. . . . . 6
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
0) |
79 | 20 | rpcnd 12967 |
. . . . . . 7
β’ (π β π
β β) |
80 | 79 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β (β€β₯β2))
β π
β
β) |
81 | 77, 78, 80 | cxpefd 26090 |
. . . . 5
β’ ((π β§ π§ β (β€β₯β2))
β (π§βππ
) = (expβ(π
Β· (logβπ§)))) |
82 | | padic.j |
. . . . . . . . . . 11
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
83 | | ostth.k |
. . . . . . . . . . 11
β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) |
84 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (β€β₯β2))
β πΉ β π΄) |
85 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (β€β₯β2))
β π β
(β€β₯β2)) |
86 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (β€β₯β2))
β 1 < (πΉβπ)) |
87 | | eqid 2733 |
. . . . . . . . . . 11
β’
((logβ(πΉβπ§)) / (logβπ§)) = ((logβ(πΉβπ§)) / (logβπ§)) |
88 | | eqid 2733 |
. . . . . . . . . . 11
β’ if((πΉβπ§) β€ 1, 1, (πΉβπ§)) = if((πΉβπ§) β€ 1, 1, (πΉβπ§)) |
89 | | eqid 2733 |
. . . . . . . . . . 11
β’
((logβπ) /
(logβπ§)) =
((logβπ) /
(logβπ§)) |
90 | 10, 9, 82, 83, 84, 85, 86, 1, 68, 87, 88, 89 | ostth2lem4 27007 |
. . . . . . . . . 10
β’ ((π β§ π§ β (β€β₯β2))
β (1 < (πΉβπ§) β§ π
β€ ((logβ(πΉβπ§)) / (logβπ§)))) |
91 | 90 | simprd 497 |
. . . . . . . . 9
β’ ((π β§ π§ β (β€β₯β2))
β π
β€
((logβ(πΉβπ§)) / (logβπ§))) |
92 | 90 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (β€β₯β2))
β 1 < (πΉβπ§)) |
93 | | eqid 2733 |
. . . . . . . . . . 11
β’ if((πΉβπ) β€ 1, 1, (πΉβπ)) = if((πΉβπ) β€ 1, 1, (πΉβπ)) |
94 | | eqid 2733 |
. . . . . . . . . . 11
β’
((logβπ§) /
(logβπ)) =
((logβπ§) /
(logβπ)) |
95 | 10, 9, 82, 83, 84, 68, 92, 87, 85, 1, 93, 94 | ostth2lem4 27007 |
. . . . . . . . . 10
β’ ((π β§ π§ β (β€β₯β2))
β (1 < (πΉβπ) β§ ((logβ(πΉβπ§)) / (logβπ§)) β€ π
)) |
96 | 95 | simprd 497 |
. . . . . . . . 9
β’ ((π β§ π§ β (β€β₯β2))
β ((logβ(πΉβπ§)) / (logβπ§)) β€ π
) |
97 | 21 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π§ β (β€β₯β2))
β π
β
β) |
98 | 59 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
β€) |
99 | 98, 60 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
β) |
100 | 9, 11 | abvcl 20326 |
. . . . . . . . . . . . . 14
β’ ((πΉ β π΄ β§ π§ β β) β (πΉβπ§) β β) |
101 | 84, 99, 100 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (β€β₯β2))
β (πΉβπ§) β
β) |
102 | 9, 11, 27 | abvgt0 20330 |
. . . . . . . . . . . . . 14
β’ ((πΉ β π΄ β§ π§ β β β§ π§ β 0) β 0 < (πΉβπ§)) |
103 | 84, 99, 78, 102 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (β€β₯β2))
β 0 < (πΉβπ§)) |
104 | 101, 103 | elrpd 12962 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (β€β₯β2))
β (πΉβπ§) β
β+) |
105 | 104 | relogcld 26001 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (β€β₯β2))
β (logβ(πΉβπ§)) β β) |
106 | 71 | nnrpd 12963 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (β€β₯β2))
β π§ β
β+) |
107 | 106 | relogcld 26001 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (β€β₯β2))
β (logβπ§) β
β) |
108 | | ef0 15981 |
. . . . . . . . . . . . . 14
β’
(expβ0) = 1 |
109 | 70 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β (β€β₯β2))
β 1 < π§) |
110 | 106 | reeflogd 26002 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β (β€β₯β2))
β (expβ(logβπ§)) = π§) |
111 | 109, 110 | breqtrrd 5137 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β (β€β₯β2))
β 1 < (expβ(logβπ§))) |
112 | 108, 111 | eqbrtrid 5144 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (β€β₯β2))
β (expβ0) < (expβ(logβπ§))) |
113 | | 0re 11165 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
114 | | eflt 16007 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ (logβπ§) β β) β (0 <
(logβπ§) β
(expβ0) < (expβ(logβπ§)))) |
115 | 113, 107,
114 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (β€β₯β2))
β (0 < (logβπ§) β (expβ0) <
(expβ(logβπ§)))) |
116 | 112, 115 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (β€β₯β2))
β 0 < (logβπ§)) |
117 | 116 | gt0ne0d 11727 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (β€β₯β2))
β (logβπ§) β
0) |
118 | 105, 107,
117 | redivcld 11991 |
. . . . . . . . . 10
β’ ((π β§ π§ β (β€β₯β2))
β ((logβ(πΉβπ§)) / (logβπ§)) β β) |
119 | 97, 118 | letri3d 11305 |
. . . . . . . . 9
β’ ((π β§ π§ β (β€β₯β2))
β (π
=
((logβ(πΉβπ§)) / (logβπ§)) β (π
β€ ((logβ(πΉβπ§)) / (logβπ§)) β§ ((logβ(πΉβπ§)) / (logβπ§)) β€ π
))) |
120 | 91, 96, 119 | mpbir2and 712 |
. . . . . . . 8
β’ ((π β§ π§ β (β€β₯β2))
β π
=
((logβ(πΉβπ§)) / (logβπ§))) |
121 | 120 | oveq1d 7376 |
. . . . . . 7
β’ ((π β§ π§ β (β€β₯β2))
β (π
Β·
(logβπ§)) =
(((logβ(πΉβπ§)) / (logβπ§)) Β· (logβπ§))) |
122 | 105 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π§ β (β€β₯β2))
β (logβ(πΉβπ§)) β β) |
123 | 107 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π§ β (β€β₯β2))
β (logβπ§) β
β) |
124 | 122, 123,
117 | divcan1d 11940 |
. . . . . . 7
β’ ((π β§ π§ β (β€β₯β2))
β (((logβ(πΉβπ§)) / (logβπ§)) Β· (logβπ§)) = (logβ(πΉβπ§))) |
125 | 121, 124 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π§ β (β€β₯β2))
β (π
Β·
(logβπ§)) =
(logβ(πΉβπ§))) |
126 | 125 | fveq2d 6850 |
. . . . 5
β’ ((π β§ π§ β (β€β₯β2))
β (expβ(π
Β· (logβπ§))) =
(expβ(logβ(πΉβπ§)))) |
127 | 104 | reeflogd 26002 |
. . . . 5
β’ ((π β§ π§ β (β€β₯β2))
β (expβ(logβ(πΉβπ§))) = (πΉβπ§)) |
128 | 81, 126, 127 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ π§ β (β€β₯β2))
β (π§βππ
) = (πΉβπ§)) |
129 | 67, 76, 128 | 3eqtrrd 2778 |
. . 3
β’ ((π β§ π§ β (β€β₯β2))
β (πΉβπ§) = ((π¦ β β β¦ ((absβπ¦)βππ
))βπ§)) |
130 | 10, 9, 2, 58, 129 | ostthlem1 26998 |
. 2
β’ (π β πΉ = (π¦ β β β¦ ((absβπ¦)βππ
))) |
131 | | oveq2 7369 |
. . . 4
β’ (π = π
β ((absβπ¦)βππ) = ((absβπ¦)βππ
)) |
132 | 131 | mpteq2dv 5211 |
. . 3
β’ (π = π
β (π¦ β β β¦ ((absβπ¦)βππ)) = (π¦ β β β¦ ((absβπ¦)βππ
))) |
133 | 132 | rspceeqv 3599 |
. 2
β’ ((π
β (0(,]1) β§ πΉ = (π¦ β β β¦ ((absβπ¦)βππ
))) β βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ))) |
134 | 51, 130, 133 | syl2anc 585 |
1
β’ (π β βπ β (0(,]1)πΉ = (π¦ β β β¦ ((absβπ¦)βππ))) |