| Step | Hyp | Ref
| Expression |
|---|
| 1 | | rpcndif0 13000 |
. . . . . 6
β’ (π₯ β β+
β π₯ β (β
β {0})) |
| 2 | 1 | adantl 481 |
. . . . 5
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β π₯ β (β
β {0})) |
| 3 | | rpcn 12991 |
. . . . . . . . . . 11
β’ (π΅ β β+
β π΅ β
β) |
| 4 | 3 | adantr 480 |
. . . . . . . . . 10
β’ ((π΅ β β+
β§ 1 < π΅) β
π΅ β
β) |
| 5 | | rpne0 12997 |
. . . . . . . . . . 11
β’ (π΅ β β+
β π΅ β
0) |
| 6 | 5 | adantr 480 |
. . . . . . . . . 10
β’ ((π΅ β β+
β§ 1 < π΅) β
π΅ β 0) |
| 7 | | animorr 976 |
. . . . . . . . . . 11
β’ ((π΅ β β+
β§ 1 < π΅) β
(π΅ < 1 β¨ 1 < π΅)) |
| 8 | | rpre 12989 |
. . . . . . . . . . . 12
β’ (π΅ β β+
β π΅ β
β) |
| 9 | | 1red 11222 |
. . . . . . . . . . . 12
β’ (1 <
π΅ β 1 β
β) |
| 10 | | lttri2 11303 |
. . . . . . . . . . . 12
β’ ((π΅ β β β§ 1 β
β) β (π΅ β 1
β (π΅ < 1 β¨ 1
< π΅))) |
| 11 | 8, 9, 10 | syl2an 595 |
. . . . . . . . . . 11
β’ ((π΅ β β+
β§ 1 < π΅) β
(π΅ β 1 β (π΅ < 1 β¨ 1 < π΅))) |
| 12 | 7, 11 | mpbird 257 |
. . . . . . . . . 10
β’ ((π΅ β β+
β§ 1 < π΅) β
π΅ β 1) |
| 13 | 4, 6, 12 | 3jca 1127 |
. . . . . . . . 9
β’ ((π΅ β β+
β§ 1 < π΅) β
(π΅ β β β§
π΅ β 0 β§ π΅ β 1)) |
| 14 | | logbmpt 26635 |
. . . . . . . . 9
β’ ((π΅ β β β§ π΅ β 0 β§ π΅ β 1) β (curry logb
βπ΅) = (π₯ β (β β {0})
β¦ ((logβπ₯) /
(logβπ΅)))) |
| 15 | 13, 14 | syl 17 |
. . . . . . . 8
β’ ((π΅ β β+
β§ 1 < π΅) β
(curry logb βπ΅) = (π₯ β (β β {0}) β¦
((logβπ₯) /
(logβπ΅)))) |
| 16 | 15 | dmeqd 5905 |
. . . . . . 7
β’ ((π΅ β β+
β§ 1 < π΅) β dom
(curry logb βπ΅) = dom (π₯ β (β β {0}) β¦
((logβπ₯) /
(logβπ΅)))) |
| 17 | | ovexd 7447 |
. . . . . . . . 9
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β (β β {0}))
β ((logβπ₯) /
(logβπ΅)) β
V) |
| 18 | 17 | ralrimiva 3145 |
. . . . . . . 8
β’ ((π΅ β β+
β§ 1 < π΅) β
βπ₯ β (β
β {0})((logβπ₯)
/ (logβπ΅)) β
V) |
| 19 | | dmmptg 6241 |
. . . . . . . 8
β’
(βπ₯ β
(β β {0})((logβπ₯) / (logβπ΅)) β V β dom (π₯ β (β β {0}) β¦
((logβπ₯) /
(logβπ΅))) = (β
β {0})) |
| 20 | 18, 19 | syl 17 |
. . . . . . 7
β’ ((π΅ β β+
β§ 1 < π΅) β dom
(π₯ β (β β
{0}) β¦ ((logβπ₯)
/ (logβπ΅))) =
(β β {0})) |
| 21 | 16, 20 | eqtrd 2771 |
. . . . . 6
β’ ((π΅ β β+
β§ 1 < π΅) β dom
(curry logb βπ΅) = (β β {0})) |
| 22 | 21 | adantr 480 |
. . . . 5
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β dom (curry logb βπ΅) = (β β {0})) |
| 23 | 2, 22 | eleqtrrd 2835 |
. . . 4
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β π₯ β dom (curry
logb βπ΅)) |
| 24 | | logbfval 26637 |
. . . . . 6
β’ (((π΅ β β β§ π΅ β 0 β§ π΅ β 1) β§ π₯ β (β β {0})) β ((curry
logb βπ΅)βπ₯) = (π΅ logb π₯)) |
| 25 | 13, 1, 24 | syl2an 595 |
. . . . 5
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β ((curry logb βπ΅)βπ₯) = (π΅ logb π₯)) |
| 26 | | simpll 764 |
. . . . . . 7
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β π΅ β
β+) |
| 27 | | simpr 484 |
. . . . . . 7
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β π₯ β
β+) |
| 28 | 12 | adantr 480 |
. . . . . . 7
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β π΅ β
1) |
| 29 | 26, 27, 28 | 3jca 1127 |
. . . . . 6
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β (π΅ β
β+ β§ π₯
β β+ β§ π΅ β 1)) |
| 30 | | relogbcl 26620 |
. . . . . 6
β’ ((π΅ β β+
β§ π₯ β
β+ β§ π΅
β 1) β (π΅
logb π₯) β
β) |
| 31 | 29, 30 | syl 17 |
. . . . 5
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β (π΅ logb
π₯) β
β) |
| 32 | 25, 31 | eqeltrd 2832 |
. . . 4
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β ((curry logb βπ΅)βπ₯) β β) |
| 33 | 23, 32 | jca 511 |
. . 3
β’ (((π΅ β β+
β§ 1 < π΅) β§ π₯ β β+)
β (π₯ β dom (curry
logb βπ΅)
β§ ((curry logb βπ΅)βπ₯) β β)) |
| 34 | 33 | ralrimiva 3145 |
. 2
β’ ((π΅ β β+
β§ 1 < π΅) β
βπ₯ β
β+ (π₯
β dom (curry logb βπ΅) β§ ((curry logb βπ΅)βπ₯) β β)) |
| 35 | | logbf 26636 |
. . . 4
β’ ((π΅ β β β§ π΅ β 0 β§ π΅ β 1) β (curry logb
βπ΅):(β β
{0})βΆβ) |
| 36 | 13, 35 | syl 17 |
. . 3
β’ ((π΅ β β+
β§ 1 < π΅) β
(curry logb βπ΅):(β β
{0})βΆβ) |
| 37 | | ffun 6720 |
. . 3
β’ ((curry
logb βπ΅):(β β {0})βΆβ
β Fun (curry logb βπ΅)) |
| 38 | | ffvresb 7126 |
. . 3
β’ (Fun
(curry logb βπ΅) β (((curry logb
βπ΅) βΎ
β+):β+βΆβ β βπ₯ β β+
(π₯ β dom (curry
logb βπ΅)
β§ ((curry logb βπ΅)βπ₯) β β))) |
| 39 | 36, 37, 38 | 3syl 18 |
. 2
β’ ((π΅ β β+
β§ 1 < π΅) β
(((curry logb βπ΅) βΎ
β+):β+βΆβ β βπ₯ β β+
(π₯ β dom (curry
logb βπ΅)
β§ ((curry logb βπ΅)βπ₯) β β))) |
| 40 | 34, 39 | mpbird 257 |
1
β’ ((π΅ β β+
β§ 1 < π΅) β
((curry logb βπ΅) βΎ
β+):β+βΆβ) |
