Step | Hyp | Ref
| Expression |
1 | | logcn.d |
. . 3
β’ π· = (β β
(-β(,]0)) |
2 | | difss 4126 |
. . 3
β’ (β
β (-β(,]0)) β β |
3 | 1, 2 | eqsstri 4011 |
. 2
β’ π· β
β |
4 | | ax-resscn 11169 |
. 2
β’ β
β β |
5 | | eqid 2726 |
. . . 4
β’ (π₯ β π· β¦ (ββ(logβπ₯))) = (π₯ β π· β¦ (ββ(logβπ₯))) |
6 | 1 | ellogdm 26528 |
. . . . . . 7
β’ (π₯ β π· β (π₯ β β β§ (π₯ β β β π₯ β
β+))) |
7 | 6 | simplbi 497 |
. . . . . 6
β’ (π₯ β π· β π₯ β β) |
8 | 1 | logdmn0 26529 |
. . . . . 6
β’ (π₯ β π· β π₯ β 0) |
9 | 7, 8 | logcld 26459 |
. . . . 5
β’ (π₯ β π· β (logβπ₯) β β) |
10 | 9 | imcld 15148 |
. . . 4
β’ (π₯ β π· β (ββ(logβπ₯)) β
β) |
11 | 5, 10 | fmpti 7107 |
. . 3
β’ (π₯ β π· β¦ (ββ(logβπ₯))):π·βΆβ |
12 | | eqid 2726 |
. . . 4
β’ if(π¦ β β+,
π¦,
(absβ(ββπ¦))) = if(π¦ β β+, π¦,
(absβ(ββπ¦))) |
13 | | eqid 2726 |
. . . 4
β’
((absβπ¦)
Β· (π§ / (1 + π§))) = ((absβπ¦) Β· (π§ / (1 + π§))) |
14 | | simpl 482 |
. . . 4
β’ ((π¦ β π· β§ π§ β β+) β π¦ β π·) |
15 | | simpr 484 |
. . . 4
β’ ((π¦ β π· β§ π§ β β+) β π§ β
β+) |
16 | 1, 12, 13, 14, 15 | logcnlem2 26532 |
. . 3
β’ ((π¦ β π· β§ π§ β β+) β
if(if(π¦ β
β+, π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§)))) β
β+) |
17 | | simpll 764 |
. . . . . 6
β’ (((π¦ β π· β§ π€ β π·) β§ (π§ β β+ β§
(absβ(π¦ β π€)) < if(if(π¦ β β+, π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§)))))) β π¦ β π·) |
18 | | simprl 768 |
. . . . . 6
β’ (((π¦ β π· β§ π€ β π·) β§ (π§ β β+ β§
(absβ(π¦ β π€)) < if(if(π¦ β β+, π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§)))))) β π§ β β+) |
19 | | simplr 766 |
. . . . . 6
β’ (((π¦ β π· β§ π€ β π·) β§ (π§ β β+ β§
(absβ(π¦ β π€)) < if(if(π¦ β β+, π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§)))))) β π€ β π·) |
20 | | simprr 770 |
. . . . . 6
β’ (((π¦ β π· β§ π€ β π·) β§ (π§ β β+ β§
(absβ(π¦ β π€)) < if(if(π¦ β β+, π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§)))))) β (absβ(π¦ β π€)) < if(if(π¦ β β+, π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§))))) |
21 | 1, 12, 13, 17, 18, 19, 20 | logcnlem4 26534 |
. . . . 5
β’ (((π¦ β π· β§ π€ β π·) β§ (π§ β β+ β§
(absβ(π¦ β π€)) < if(if(π¦ β β+, π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§)))))) β
(absβ((ββ(logβπ¦)) β (ββ(logβπ€)))) < π§) |
22 | 21 | expr 456 |
. . . 4
β’ (((π¦ β π· β§ π€ β π·) β§ π§ β β+) β
((absβ(π¦ β
π€)) < if(if(π¦ β β+,
π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§)))) β
(absβ((ββ(logβπ¦)) β (ββ(logβπ€)))) < π§)) |
23 | | 2fveq3 6890 |
. . . . . . . . 9
β’ (π₯ = π¦ β (ββ(logβπ₯)) =
(ββ(logβπ¦))) |
24 | | fvex 6898 |
. . . . . . . . 9
β’
(ββ(logβπ¦)) β V |
25 | 23, 5, 24 | fvmpt 6992 |
. . . . . . . 8
β’ (π¦ β π· β ((π₯ β π· β¦ (ββ(logβπ₯)))βπ¦) = (ββ(logβπ¦))) |
26 | 25 | ad2antrr 723 |
. . . . . . 7
β’ (((π¦ β π· β§ π€ β π·) β§ π§ β β+) β ((π₯ β π· β¦ (ββ(logβπ₯)))βπ¦) = (ββ(logβπ¦))) |
27 | | 2fveq3 6890 |
. . . . . . . . 9
β’ (π₯ = π€ β (ββ(logβπ₯)) =
(ββ(logβπ€))) |
28 | | fvex 6898 |
. . . . . . . . 9
β’
(ββ(logβπ€)) β V |
29 | 27, 5, 28 | fvmpt 6992 |
. . . . . . . 8
β’ (π€ β π· β ((π₯ β π· β¦ (ββ(logβπ₯)))βπ€) = (ββ(logβπ€))) |
30 | 29 | ad2antlr 724 |
. . . . . . 7
β’ (((π¦ β π· β§ π€ β π·) β§ π§ β β+) β ((π₯ β π· β¦ (ββ(logβπ₯)))βπ€) = (ββ(logβπ€))) |
31 | 26, 30 | oveq12d 7423 |
. . . . . 6
β’ (((π¦ β π· β§ π€ β π·) β§ π§ β β+) β (((π₯ β π· β¦ (ββ(logβπ₯)))βπ¦) β ((π₯ β π· β¦ (ββ(logβπ₯)))βπ€)) = ((ββ(logβπ¦)) β
(ββ(logβπ€)))) |
32 | 31 | fveq2d 6889 |
. . . . 5
β’ (((π¦ β π· β§ π€ β π·) β§ π§ β β+) β
(absβ(((π₯ β
π· β¦
(ββ(logβπ₯)))βπ¦) β ((π₯ β π· β¦ (ββ(logβπ₯)))βπ€))) =
(absβ((ββ(logβπ¦)) β (ββ(logβπ€))))) |
33 | 32 | breq1d 5151 |
. . . 4
β’ (((π¦ β π· β§ π€ β π·) β§ π§ β β+) β
((absβ(((π₯ β
π· β¦
(ββ(logβπ₯)))βπ¦) β ((π₯ β π· β¦ (ββ(logβπ₯)))βπ€))) < π§ β
(absβ((ββ(logβπ¦)) β (ββ(logβπ€)))) < π§)) |
34 | 22, 33 | sylibrd 259 |
. . 3
β’ (((π¦ β π· β§ π€ β π·) β§ π§ β β+) β
((absβ(π¦ β
π€)) < if(if(π¦ β β+,
π¦,
(absβ(ββπ¦))) β€ ((absβπ¦) Β· (π§ / (1 + π§))), if(π¦ β β+, π¦,
(absβ(ββπ¦))), ((absβπ¦) Β· (π§ / (1 + π§)))) β (absβ(((π₯ β π· β¦ (ββ(logβπ₯)))βπ¦) β ((π₯ β π· β¦ (ββ(logβπ₯)))βπ€))) < π§)) |
35 | 11, 16, 34 | elcncf1ii 24771 |
. 2
β’ ((π· β β β§ β
β β) β (π₯
β π· β¦
(ββ(logβπ₯))) β (π·βcnββ)) |
36 | 3, 4, 35 | mp2an 689 |
1
β’ (π₯ β π· β¦ (ββ(logβπ₯))) β (π·βcnββ) |