Step | Hyp | Ref
| Expression |
1 | | ostth.1 |
. . . . . 6
β’ (π β πΉ β π΄) |
2 | | ostth2.2 |
. . . . . . . . 9
β’ (π β π β
(β€β₯β2)) |
3 | | eluz2b2 12854 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
4 | 2, 3 | sylib 217 |
. . . . . . . 8
β’ (π β (π β β β§ 1 < π)) |
5 | 4 | simpld 496 |
. . . . . . 7
β’ (π β π β β) |
6 | | nnq 12895 |
. . . . . . 7
β’ (π β β β π β
β) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (π β π β β) |
8 | | qabsabv.a |
. . . . . . 7
β’ π΄ = (AbsValβπ) |
9 | | qrng.q |
. . . . . . . 8
β’ π = (βfld
βΎs β) |
10 | 9 | qrngbas 26990 |
. . . . . . 7
β’ β =
(Baseβπ) |
11 | 8, 10 | abvcl 20326 |
. . . . . 6
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
12 | 1, 7, 11 | syl2anc 585 |
. . . . 5
β’ (π β (πΉβπ) β β) |
13 | 12 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β (πΉβπ) β β) |
14 | 13 | recnd 11191 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) β β) |
15 | | ostth2.7 |
. . . . . . 7
β’ π = if((πΉβπ) β€ 1, 1, (πΉβπ)) |
16 | | 1re 11163 |
. . . . . . . 8
β’ 1 β
β |
17 | | ostth2.5 |
. . . . . . . . . . . 12
β’ (π β π β
(β€β₯β2)) |
18 | | eluz2b2 12854 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
19 | 17, 18 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π β β β§ 1 < π)) |
20 | 19 | simpld 496 |
. . . . . . . . . 10
β’ (π β π β β) |
21 | | nnq 12895 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
β’ (π β π β β) |
23 | 8, 10 | abvcl 20326 |
. . . . . . . . 9
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
24 | 1, 22, 23 | syl2anc 585 |
. . . . . . . 8
β’ (π β (πΉβπ) β β) |
25 | | ifcl 4535 |
. . . . . . . 8
β’ ((1
β β β§ (πΉβπ) β β) β if((πΉβπ) β€ 1, 1, (πΉβπ)) β β) |
26 | 16, 24, 25 | sylancr 588 |
. . . . . . 7
β’ (π β if((πΉβπ) β€ 1, 1, (πΉβπ)) β β) |
27 | 15, 26 | eqeltrid 2838 |
. . . . . 6
β’ (π β π β β) |
28 | 27 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
29 | | 0red 11166 |
. . . . . . . . 9
β’ (π β 0 β
β) |
30 | | 1red 11164 |
. . . . . . . . 9
β’ (π β 1 β
β) |
31 | | 0lt1 11685 |
. . . . . . . . . 10
β’ 0 <
1 |
32 | 31 | a1i 11 |
. . . . . . . . 9
β’ (π β 0 < 1) |
33 | | max2 13115 |
. . . . . . . . . . 11
β’ (((πΉβπ) β β β§ 1 β β)
β 1 β€ if((πΉβπ) β€ 1, 1, (πΉβπ))) |
34 | 24, 30, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β 1 β€ if((πΉβπ) β€ 1, 1, (πΉβπ))) |
35 | 34, 15 | breqtrrdi 5151 |
. . . . . . . . 9
β’ (π β 1 β€ π) |
36 | 29, 30, 27, 32, 35 | ltletrd 11323 |
. . . . . . . 8
β’ (π β 0 < π) |
37 | 36 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β 0 < π) |
38 | 28, 37 | elrpd 12962 |
. . . . . 6
β’ ((π β§ π β β) β π β
β+) |
39 | 38 | rpge0d 12969 |
. . . . 5
β’ ((π β§ π β β) β 0 β€ π) |
40 | | ostth2.8 |
. . . . . . . 8
β’ π = ((logβπ) / (logβπ)) |
41 | 5 | nnred 12176 |
. . . . . . . . . 10
β’ (π β π β β) |
42 | 4 | simprd 497 |
. . . . . . . . . 10
β’ (π β 1 < π) |
43 | 41, 42 | rplogcld 26007 |
. . . . . . . . 9
β’ (π β (logβπ) β
β+) |
44 | 20 | nnred 12176 |
. . . . . . . . . 10
β’ (π β π β β) |
45 | 19 | simprd 497 |
. . . . . . . . . 10
β’ (π β 1 < π) |
46 | 44, 45 | rplogcld 26007 |
. . . . . . . . 9
β’ (π β (logβπ) β
β+) |
47 | 43, 46 | rpdivcld 12982 |
. . . . . . . 8
β’ (π β ((logβπ) / (logβπ)) β
β+) |
48 | 40, 47 | eqeltrid 2838 |
. . . . . . 7
β’ (π β π β
β+) |
49 | 48 | rpred 12965 |
. . . . . 6
β’ (π β π β β) |
50 | 49 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π β β) |
51 | 28, 39, 50 | recxpcld 26101 |
. . . 4
β’ ((π β§ π β β) β (πβππ) β β) |
52 | 51 | recnd 11191 |
. . 3
β’ ((π β§ π β β) β (πβππ) β β) |
53 | 38, 50 | rpcxpcld 26110 |
. . . 4
β’ ((π β§ π β β) β (πβππ) β
β+) |
54 | 53 | rpne0d 12970 |
. . 3
β’ ((π β§ π β β) β (πβππ) β 0) |
55 | | nnnn0 12428 |
. . . 4
β’ (π β β β π β
β0) |
56 | 55 | adantl 483 |
. . 3
β’ ((π β§ π β β) β π β
β0) |
57 | 14, 52, 54, 56 | expdivd 14074 |
. 2
β’ ((π β§ π β β) β (((πΉβπ) / (πβππ))βπ) = (((πΉβπ)βπ) / ((πβππ)βπ))) |
58 | | reexpcl 13993 |
. . . . . 6
β’ (((πΉβπ) β β β§ π β β0) β ((πΉβπ)βπ) β β) |
59 | 12, 55, 58 | syl2an 597 |
. . . . 5
β’ ((π β§ π β β) β ((πΉβπ)βπ) β β) |
60 | 20 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
61 | 60 | nnred 12176 |
. . . . . . 7
β’ ((π β§ π β β) β π β β) |
62 | | nnre 12168 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
63 | 62 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β) |
64 | 63, 50 | remulcld 11193 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π Β· π) β β) |
65 | 56 | nn0ge0d 12484 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 0 β€ π) |
66 | 48 | rpge0d 12969 |
. . . . . . . . . . . 12
β’ (π β 0 β€ π) |
67 | 66 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 0 β€ π) |
68 | 63, 50, 65, 67 | mulge0d 11740 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 0 β€ (π Β· π)) |
69 | | flge0nn0 13734 |
. . . . . . . . . 10
β’ (((π Β· π) β β β§ 0 β€ (π Β· π)) β (ββ(π Β· π)) β
β0) |
70 | 64, 68, 69 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β β) β
(ββ(π Β·
π)) β
β0) |
71 | | peano2nn0 12461 |
. . . . . . . . 9
β’
((ββ(π
Β· π)) β
β0 β ((ββ(π Β· π)) + 1) β
β0) |
72 | 70, 71 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β
((ββ(π Β·
π)) + 1) β
β0) |
73 | 72 | nn0red 12482 |
. . . . . . 7
β’ ((π β§ π β β) β
((ββ(π Β·
π)) + 1) β
β) |
74 | 61, 73 | remulcld 11193 |
. . . . . 6
β’ ((π β§ π β β) β (π Β· ((ββ(π Β· π)) + 1)) β β) |
75 | 28, 72 | reexpcld 14077 |
. . . . . 6
β’ ((π β§ π β β) β (πβ((ββ(π Β· π)) + 1)) β β) |
76 | 74, 75 | remulcld 11193 |
. . . . 5
β’ ((π β§ π β β) β ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1))) β β) |
77 | | peano2re 11336 |
. . . . . . . . 9
β’ (π β β β (π + 1) β
β) |
78 | 50, 77 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (π + 1) β β) |
79 | 63, 78 | remulcld 11193 |
. . . . . . 7
β’ ((π β§ π β β) β (π Β· (π + 1)) β β) |
80 | 61, 79 | remulcld 11193 |
. . . . . 6
β’ ((π β§ π β β) β (π Β· (π Β· (π + 1))) β β) |
81 | 51, 56 | reexpcld 14077 |
. . . . . . 7
β’ ((π β§ π β β) β ((πβππ)βπ) β β) |
82 | 81, 28 | remulcld 11193 |
. . . . . 6
β’ ((π β§ π β β) β (((πβππ)βπ) Β· π) β β) |
83 | 80, 82 | remulcld 11193 |
. . . . 5
β’ ((π β§ π β β) β ((π Β· (π Β· (π + 1))) Β· (((πβππ)βπ) Β· π)) β β) |
84 | 9, 8 | qabvexp 26997 |
. . . . . . 7
β’ ((πΉ β π΄ β§ π β β β§ π β β0) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |
85 | 1, 7, 55, 84 | syl2an3an 1423 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |
86 | 63 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β β) |
87 | 43 | rpred 12965 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (logβπ) β
β) |
88 | 87 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ (π β (logβπ) β
β) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (logβπ) β
β) |
90 | 46 | rpred 12965 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (logβπ) β
β) |
91 | 90 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ (π β (logβπ) β
β) |
92 | 91 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (logβπ) β
β) |
93 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (logβπ) β
β+) |
94 | 93 | rpne0d 12970 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (logβπ) β 0) |
95 | 86, 89, 92, 94 | divassd 11974 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((π Β· (logβπ)) / (logβπ)) = (π Β· ((logβπ) / (logβπ)))) |
96 | 40 | oveq2i 7372 |
. . . . . . . . . . . . . . 15
β’ (π Β· π) = (π Β· ((logβπ) / (logβπ))) |
97 | 95, 96 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π Β· (logβπ)) / (logβπ)) = (π Β· π)) |
98 | 97 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (((π Β· (logβπ)) / (logβπ)) Β· (logβπ)) = ((π Β· π) Β· (logβπ))) |
99 | 86, 89 | mulcld 11183 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π Β· (logβπ)) β β) |
100 | 99, 92, 94 | divcan1d 11940 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (((π Β· (logβπ)) / (logβπ)) Β· (logβπ)) = (π Β· (logβπ))) |
101 | 98, 100 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π Β· π) Β· (logβπ)) = (π Β· (logβπ))) |
102 | | flltp1 13714 |
. . . . . . . . . . . . . 14
β’ ((π Β· π) β β β (π Β· π) < ((ββ(π Β· π)) + 1)) |
103 | 64, 102 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π Β· π) < ((ββ(π Β· π)) + 1)) |
104 | 64, 73, 93, 103 | ltmul1dd 13020 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π Β· π) Β· (logβπ)) < (((ββ(π Β· π)) + 1) Β· (logβπ))) |
105 | 101, 104 | eqbrtrrd 5133 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π Β· (logβπ)) < (((ββ(π Β· π)) + 1) Β· (logβπ))) |
106 | 87 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (logβπ) β
β) |
107 | 63, 106 | remulcld 11193 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π Β· (logβπ)) β β) |
108 | 90 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (logβπ) β
β) |
109 | 73, 108 | remulcld 11193 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β
(((ββ(π
Β· π)) + 1) Β·
(logβπ)) β
β) |
110 | | eflt 16007 |
. . . . . . . . . . . 12
β’ (((π Β· (logβπ)) β β β§
(((ββ(π
Β· π)) + 1) Β·
(logβπ)) β
β) β ((π
Β· (logβπ))
< (((ββ(π
Β· π)) + 1) Β·
(logβπ)) β
(expβ(π Β·
(logβπ))) <
(expβ(((ββ(π Β· π)) + 1) Β· (logβπ))))) |
111 | 107, 109,
110 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π Β· (logβπ)) < (((ββ(π Β· π)) + 1) Β· (logβπ)) β (expβ(π Β· (logβπ))) <
(expβ(((ββ(π Β· π)) + 1) Β· (logβπ))))) |
112 | 105, 111 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (expβ(π Β· (logβπ))) <
(expβ(((ββ(π Β· π)) + 1) Β· (logβπ)))) |
113 | 5 | nnrpd 12963 |
. . . . . . . . . . 11
β’ (π β π β
β+) |
114 | | nnz 12528 |
. . . . . . . . . . 11
β’ (π β β β π β
β€) |
115 | | reexplog 25973 |
. . . . . . . . . . 11
β’ ((π β β+
β§ π β β€)
β (πβπ) = (expβ(π Β· (logβπ)))) |
116 | 113, 114,
115 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) = (expβ(π Β· (logβπ)))) |
117 | 60 | nnrpd 12963 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β
β+) |
118 | 72 | nn0zd 12533 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β
((ββ(π Β·
π)) + 1) β
β€) |
119 | | reexplog 25973 |
. . . . . . . . . . 11
β’ ((π β β+
β§ ((ββ(π
Β· π)) + 1) β
β€) β (πβ((ββ(π Β· π)) + 1)) =
(expβ(((ββ(π Β· π)) + 1) Β· (logβπ)))) |
120 | 117, 118,
119 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ((ββ(π Β· π)) + 1)) =
(expβ(((ββ(π Β· π)) + 1) Β· (logβπ)))) |
121 | 112, 116,
120 | 3brtr4d 5141 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ) < (πβ((ββ(π Β· π)) + 1))) |
122 | | nnexpcl 13989 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
123 | 5, 55, 122 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) β β) |
124 | 60, 72 | nnexpcld 14157 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ((ββ(π Β· π)) + 1)) β β) |
125 | | nnltlem1 12578 |
. . . . . . . . . 10
β’ (((πβπ) β β β§ (πβ((ββ(π Β· π)) + 1)) β β) β ((πβπ) < (πβ((ββ(π Β· π)) + 1)) β (πβπ) β€ ((πβ((ββ(π Β· π)) + 1)) β 1))) |
126 | 123, 124,
125 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβπ) < (πβ((ββ(π Β· π)) + 1)) β (πβπ) β€ ((πβ((ββ(π Β· π)) + 1)) β 1))) |
127 | 121, 126 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβπ) β€ ((πβ((ββ(π Β· π)) + 1)) β 1)) |
128 | 123 | nnnn0d 12481 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) β
β0) |
129 | | nn0uz 12813 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
130 | 128, 129 | eleqtrdi 2844 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ) β
(β€β₯β0)) |
131 | 124 | nnzd 12534 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ((ββ(π Β· π)) + 1)) β β€) |
132 | | peano2zm 12554 |
. . . . . . . . . 10
β’ ((πβ((ββ(π Β· π)) + 1)) β β€ β ((πβ((ββ(π Β· π)) + 1)) β 1) β
β€) |
133 | 131, 132 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβ((ββ(π Β· π)) + 1)) β 1) β
β€) |
134 | | elfz5 13442 |
. . . . . . . . 9
β’ (((πβπ) β (β€β₯β0)
β§ ((πβ((ββ(π Β· π)) + 1)) β 1) β β€) β
((πβπ) β (0...((πβ((ββ(π Β· π)) + 1)) β 1)) β (πβπ) β€ ((πβ((ββ(π Β· π)) + 1)) β 1))) |
135 | 130, 133,
134 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πβπ) β (0...((πβ((ββ(π Β· π)) + 1)) β 1)) β (πβπ) β€ ((πβ((ββ(π Β· π)) + 1)) β 1))) |
136 | 127, 135 | mpbird 257 |
. . . . . . 7
β’ ((π β§ π β β) β (πβπ) β (0...((πβ((ββ(π Β· π)) + 1)) β 1))) |
137 | | padic.j |
. . . . . . . . . 10
β’ π½ = (π β β β¦ (π₯ β β β¦ if(π₯ = 0, 0, (πβ-(π pCnt π₯))))) |
138 | | ostth.k |
. . . . . . . . . 10
β’ πΎ = (π₯ β β β¦ if(π₯ = 0, 0, 1)) |
139 | | ostth2.3 |
. . . . . . . . . 10
β’ (π β 1 < (πΉβπ)) |
140 | | ostth2.4 |
. . . . . . . . . 10
β’ π
= ((logβ(πΉβπ)) / (logβπ)) |
141 | | ostth2.6 |
. . . . . . . . . 10
β’ π = ((logβ(πΉβπ)) / (logβπ)) |
142 | 9, 8, 137, 138, 1, 2, 139, 140, 17, 141, 15 | ostth2lem2 27005 |
. . . . . . . . 9
β’ ((π β§ ((ββ(π Β· π)) + 1) β β0 β§
(πβπ) β (0...((πβ((ββ(π Β· π)) + 1)) β 1))) β (πΉβ(πβπ)) β€ ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1)))) |
143 | 142 | 3expia 1122 |
. . . . . . . 8
β’ ((π β§ ((ββ(π Β· π)) + 1) β β0) β
((πβπ) β (0...((πβ((ββ(π Β· π)) + 1)) β 1)) β (πΉβ(πβπ)) β€ ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1))))) |
144 | 72, 143 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β β) β ((πβπ) β (0...((πβ((ββ(π Β· π)) + 1)) β 1)) β (πΉβ(πβπ)) β€ ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1))))) |
145 | 136, 144 | mpd 15 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβ(πβπ)) β€ ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1)))) |
146 | 85, 145 | eqbrtrrd 5133 |
. . . . 5
β’ ((π β§ π β β) β ((πΉβπ)βπ) β€ ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1)))) |
147 | 80, 75 | remulcld 11193 |
. . . . . 6
β’ ((π β§ π β β) β ((π Β· (π Β· (π + 1))) Β· (πβ((ββ(π Β· π)) + 1))) β β) |
148 | | peano2re 11336 |
. . . . . . . . . 10
β’ ((π Β· π) β β β ((π Β· π) + 1) β β) |
149 | 64, 148 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π Β· π) + 1) β β) |
150 | 70 | nn0red 12482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
(ββ(π Β·
π)) β
β) |
151 | | 1red 11164 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 1 β
β) |
152 | | flle 13713 |
. . . . . . . . . . 11
β’ ((π Β· π) β β β
(ββ(π Β·
π)) β€ (π Β· π)) |
153 | 64, 152 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
(ββ(π Β·
π)) β€ (π Β· π)) |
154 | 150, 64, 151, 153 | leadd1dd 11777 |
. . . . . . . . 9
β’ ((π β§ π β β) β
((ββ(π Β·
π)) + 1) β€ ((π Β· π) + 1)) |
155 | | nnge1 12189 |
. . . . . . . . . . . 12
β’ (π β β β 1 β€
π) |
156 | 155 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 1 β€ π) |
157 | 151, 63, 64, 156 | leadd2dd 11778 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π Β· π) + 1) β€ ((π Β· π) + π)) |
158 | 50 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
159 | 151 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 1 β
β) |
160 | 86, 158, 159 | adddid 11187 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π Β· (π + 1)) = ((π Β· π) + (π Β· 1))) |
161 | 86 | mulridd 11180 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π Β· 1) = π) |
162 | 161 | oveq2d 7377 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π Β· π) + (π Β· 1)) = ((π Β· π) + π)) |
163 | 160, 162 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π Β· (π + 1)) = ((π Β· π) + π)) |
164 | 157, 163 | breqtrrd 5137 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((π Β· π) + 1) β€ (π Β· (π + 1))) |
165 | 73, 149, 79, 154, 164 | letrd 11320 |
. . . . . . . 8
β’ ((π β§ π β β) β
((ββ(π Β·
π)) + 1) β€ (π Β· (π + 1))) |
166 | 60 | nngt0d 12210 |
. . . . . . . . 9
β’ ((π β§ π β β) β 0 < π) |
167 | | lemul2 12016 |
. . . . . . . . 9
β’
((((ββ(π
Β· π)) + 1) β
β β§ (π Β·
(π + 1)) β β
β§ (π β β
β§ 0 < π)) β
(((ββ(π
Β· π)) + 1) β€
(π Β· (π + 1)) β (π Β· ((ββ(π Β· π)) + 1)) β€ (π Β· (π Β· (π + 1))))) |
168 | 73, 79, 61, 166, 167 | syl112anc 1375 |
. . . . . . . 8
β’ ((π β§ π β β) β
(((ββ(π
Β· π)) + 1) β€
(π Β· (π + 1)) β (π Β· ((ββ(π Β· π)) + 1)) β€ (π Β· (π Β· (π + 1))))) |
169 | 165, 168 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π β β) β (π Β· ((ββ(π Β· π)) + 1)) β€ (π Β· (π Β· (π + 1)))) |
170 | | expgt0 14010 |
. . . . . . . . 9
β’ ((π β β β§
((ββ(π Β·
π)) + 1) β β€
β§ 0 < π) β 0
< (πβ((ββ(π Β· π)) + 1))) |
171 | 28, 118, 37, 170 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β β) β 0 < (πβ((ββ(π Β· π)) + 1))) |
172 | | lemul1 12015 |
. . . . . . . 8
β’ (((π Β· ((ββ(π Β· π)) + 1)) β β β§ (π Β· (π Β· (π + 1))) β β β§ ((πβ((ββ(π Β· π)) + 1)) β β β§ 0 < (πβ((ββ(π Β· π)) + 1)))) β ((π Β· ((ββ(π Β· π)) + 1)) β€ (π Β· (π Β· (π + 1))) β ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1))) β€ ((π Β· (π Β· (π + 1))) Β· (πβ((ββ(π Β· π)) + 1))))) |
173 | 74, 80, 75, 171, 172 | syl112anc 1375 |
. . . . . . 7
β’ ((π β§ π β β) β ((π Β· ((ββ(π Β· π)) + 1)) β€ (π Β· (π Β· (π + 1))) β ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1))) β€ ((π Β· (π Β· (π + 1))) Β· (πβ((ββ(π Β· π)) + 1))))) |
174 | 169, 173 | mpbid 231 |
. . . . . 6
β’ ((π β§ π β β) β ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1))) β€ ((π Β· (π Β· (π + 1))) Β· (πβ((ββ(π Β· π)) + 1)))) |
175 | 28 | recnd 11191 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
176 | 175, 70 | expp1d 14061 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβ((ββ(π Β· π)) + 1)) = ((πβ(ββ(π Β· π))) Β· π)) |
177 | 35 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 1 β€ π) |
178 | | remulcl 11144 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β (π Β· π) β β) |
179 | 49, 62, 178 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π Β· π) β β) |
180 | 86, 158 | mulcomd 11184 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π Β· π) = (π Β· π)) |
181 | 153, 180 | breqtrd 5135 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β
(ββ(π Β·
π)) β€ (π Β· π)) |
182 | 28, 177, 150, 179, 181 | cxplead 26099 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ(ββ(π Β· π))) β€ (πβπ(π Β· π))) |
183 | | cxpexp 26046 |
. . . . . . . . . . 11
β’ ((π β β β§
(ββ(π Β·
π)) β
β0) β (πβπ(ββ(π Β· π))) = (πβ(ββ(π Β· π)))) |
184 | 175, 70, 183 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ(ββ(π Β· π))) = (πβ(ββ(π Β· π)))) |
185 | 38, 50, 86 | cxpmuld 26114 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβπ(π Β· π)) = ((πβππ)βππ)) |
186 | | cxpexp 26046 |
. . . . . . . . . . . 12
β’ (((πβππ) β β β§ π β β0)
β ((πβππ)βππ) = ((πβππ)βπ)) |
187 | 52, 56, 186 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πβππ)βππ) = ((πβππ)βπ)) |
188 | 185, 187 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ(π Β· π)) = ((πβππ)βπ)) |
189 | 182, 184,
188 | 3brtr3d 5140 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβ(ββ(π Β· π))) β€ ((πβππ)βπ)) |
190 | 28, 70 | reexpcld 14077 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ(ββ(π Β· π))) β β) |
191 | 190, 81, 38 | lemul1d 13008 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβ(ββ(π Β· π))) β€ ((πβππ)βπ) β ((πβ(ββ(π Β· π))) Β· π) β€ (((πβππ)βπ) Β· π))) |
192 | 189, 191 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πβ(ββ(π Β· π))) Β· π) β€ (((πβππ)βπ) Β· π)) |
193 | 176, 192 | eqbrtrd 5131 |
. . . . . . 7
β’ ((π β§ π β β) β (πβ((ββ(π Β· π)) + 1)) β€ (((πβππ)βπ) Β· π)) |
194 | | nngt0 12192 |
. . . . . . . . . . 11
β’ (π β β β 0 <
π) |
195 | 194 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 0 < π) |
196 | | 0red 11166 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 0 β
β) |
197 | 48 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β
β+) |
198 | 197 | rpgt0d 12968 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 0 < π) |
199 | 50 | ltp1d 12093 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π < (π + 1)) |
200 | 196, 50, 78, 198, 199 | lttrd 11324 |
. . . . . . . . . 10
β’ ((π β§ π β β) β 0 < (π + 1)) |
201 | 63, 78, 195, 200 | mulgt0d 11318 |
. . . . . . . . 9
β’ ((π β§ π β β) β 0 < (π Β· (π + 1))) |
202 | 61, 79, 166, 201 | mulgt0d 11318 |
. . . . . . . 8
β’ ((π β§ π β β) β 0 < (π Β· (π Β· (π + 1)))) |
203 | | lemul2 12016 |
. . . . . . . 8
β’ (((πβ((ββ(π Β· π)) + 1)) β β β§ (((πβππ)βπ) Β· π) β β β§ ((π Β· (π Β· (π + 1))) β β β§ 0 < (π Β· (π Β· (π + 1))))) β ((πβ((ββ(π Β· π)) + 1)) β€ (((πβππ)βπ) Β· π) β ((π Β· (π Β· (π + 1))) Β· (πβ((ββ(π Β· π)) + 1))) β€ ((π Β· (π Β· (π + 1))) Β· (((πβππ)βπ) Β· π)))) |
204 | 75, 82, 80, 202, 203 | syl112anc 1375 |
. . . . . . 7
β’ ((π β§ π β β) β ((πβ((ββ(π Β· π)) + 1)) β€ (((πβππ)βπ) Β· π) β ((π Β· (π Β· (π + 1))) Β· (πβ((ββ(π Β· π)) + 1))) β€ ((π Β· (π Β· (π + 1))) Β· (((πβππ)βπ) Β· π)))) |
205 | 193, 204 | mpbid 231 |
. . . . . 6
β’ ((π β§ π β β) β ((π Β· (π Β· (π + 1))) Β· (πβ((ββ(π Β· π)) + 1))) β€ ((π Β· (π Β· (π + 1))) Β· (((πβππ)βπ) Β· π))) |
206 | 76, 147, 83, 174, 205 | letrd 11320 |
. . . . 5
β’ ((π β§ π β β) β ((π Β· ((ββ(π Β· π)) + 1)) Β· (πβ((ββ(π Β· π)) + 1))) β€ ((π Β· (π Β· (π + 1))) Β· (((πβππ)βπ) Β· π))) |
207 | 59, 76, 83, 146, 206 | letrd 11320 |
. . . 4
β’ ((π β§ π β β) β ((πΉβπ)βπ) β€ ((π Β· (π Β· (π + 1))) Β· (((πβππ)βπ) Β· π))) |
208 | 80 | recnd 11191 |
. . . . . 6
β’ ((π β§ π β β) β (π Β· (π Β· (π + 1))) β β) |
209 | 81 | recnd 11191 |
. . . . . 6
β’ ((π β§ π β β) β ((πβππ)βπ) β β) |
210 | 208, 209,
175 | mul12d 11372 |
. . . . 5
β’ ((π β§ π β β) β ((π Β· (π Β· (π + 1))) Β· (((πβππ)βπ) Β· π)) = (((πβππ)βπ) Β· ((π Β· (π Β· (π + 1))) Β· π))) |
211 | 61 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
212 | 79 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π β β) β (π Β· (π + 1)) β β) |
213 | 211, 212,
175 | mul32d 11373 |
. . . . . . 7
β’ ((π β§ π β β) β ((π Β· (π Β· (π + 1))) Β· π) = ((π Β· π) Β· (π Β· (π + 1)))) |
214 | 211, 175 | mulcld 11183 |
. . . . . . . 8
β’ ((π β§ π β β) β (π Β· π) β β) |
215 | 78 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π β β) β (π + 1) β β) |
216 | 214, 86, 215 | mul12d 11372 |
. . . . . . 7
β’ ((π β§ π β β) β ((π Β· π) Β· (π Β· (π + 1))) = (π Β· ((π Β· π) Β· (π + 1)))) |
217 | 213, 216 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β β) β ((π Β· (π Β· (π + 1))) Β· π) = (π Β· ((π Β· π) Β· (π + 1)))) |
218 | 217 | oveq2d 7377 |
. . . . 5
β’ ((π β§ π β β) β (((πβππ)βπ) Β· ((π Β· (π Β· (π + 1))) Β· π)) = (((πβππ)βπ) Β· (π Β· ((π Β· π) Β· (π + 1))))) |
219 | 210, 218 | eqtrd 2773 |
. . . 4
β’ ((π β§ π β β) β ((π Β· (π Β· (π + 1))) Β· (((πβππ)βπ) Β· π)) = (((πβππ)βπ) Β· (π Β· ((π Β· π) Β· (π + 1))))) |
220 | 207, 219 | breqtrd 5135 |
. . 3
β’ ((π β§ π β β) β ((πΉβπ)βπ) β€ (((πβππ)βπ) Β· (π Β· ((π Β· π) Β· (π + 1))))) |
221 | 61, 28 | remulcld 11193 |
. . . . . 6
β’ ((π β§ π β β) β (π Β· π) β β) |
222 | 221, 78 | remulcld 11193 |
. . . . 5
β’ ((π β§ π β β) β ((π Β· π) Β· (π + 1)) β β) |
223 | 63, 222 | remulcld 11193 |
. . . 4
β’ ((π β§ π β β) β (π Β· ((π Β· π) Β· (π + 1))) β β) |
224 | 114 | adantl 483 |
. . . . 5
β’ ((π β§ π β β) β π β β€) |
225 | 53, 224 | rpexpcld 14159 |
. . . 4
β’ ((π β§ π β β) β ((πβππ)βπ) β
β+) |
226 | 59, 223, 225 | ledivmuld 13018 |
. . 3
β’ ((π β§ π β β) β ((((πΉβπ)βπ) / ((πβππ)βπ)) β€ (π Β· ((π Β· π) Β· (π + 1))) β ((πΉβπ)βπ) β€ (((πβππ)βπ) Β· (π Β· ((π Β· π) Β· (π + 1)))))) |
227 | 220, 226 | mpbird 257 |
. 2
β’ ((π β§ π β β) β (((πΉβπ)βπ) / ((πβππ)βπ)) β€ (π Β· ((π Β· π) Β· (π + 1)))) |
228 | 57, 227 | eqbrtrd 5131 |
1
β’ ((π β§ π β β) β (((πΉβπ) / (πβππ))βπ) β€ (π Β· ((π Β· π) Β· (π + 1)))) |