Step | Hyp | Ref
| Expression |
1 | | expgrowthi.yt |
. . . . 5
β’ π = (π‘ β π β¦ (πΆ Β· (expβ(πΎ Β· π‘)))) |
2 | | oveq2 7369 |
. . . . . . . 8
β’ (π‘ = π¦ β (πΎ Β· π‘) = (πΎ Β· π¦)) |
3 | 2 | fveq2d 6850 |
. . . . . . 7
β’ (π‘ = π¦ β (expβ(πΎ Β· π‘)) = (expβ(πΎ Β· π¦))) |
4 | 3 | oveq2d 7377 |
. . . . . 6
β’ (π‘ = π¦ β (πΆ Β· (expβ(πΎ Β· π‘))) = (πΆ Β· (expβ(πΎ Β· π¦)))) |
5 | 4 | cbvmptv 5222 |
. . . . 5
β’ (π‘ β π β¦ (πΆ Β· (expβ(πΎ Β· π‘)))) = (π¦ β π β¦ (πΆ Β· (expβ(πΎ Β· π¦)))) |
6 | 1, 5 | eqtri 2761 |
. . . 4
β’ π = (π¦ β π β¦ (πΆ Β· (expβ(πΎ Β· π¦)))) |
7 | 6 | oveq2i 7372 |
. . 3
β’ (π D π) = (π D (π¦ β π β¦ (πΆ Β· (expβ(πΎ Β· π¦))))) |
8 | | expgrowthi.s |
. . . . 5
β’ (π β π β {β, β}) |
9 | | elpri 4612 |
. . . . . . . 8
β’ (π β {β, β}
β (π = β β¨
π =
β)) |
10 | | eleq2 2823 |
. . . . . . . . . 10
β’ (π = β β (π¦ β π β π¦ β β)) |
11 | | recn 11149 |
. . . . . . . . . 10
β’ (π¦ β β β π¦ β
β) |
12 | 10, 11 | syl6bi 253 |
. . . . . . . . 9
β’ (π = β β (π¦ β π β π¦ β β)) |
13 | | eleq2 2823 |
. . . . . . . . . 10
β’ (π = β β (π¦ β π β π¦ β β)) |
14 | 13 | biimpd 228 |
. . . . . . . . 9
β’ (π = β β (π¦ β π β π¦ β β)) |
15 | 12, 14 | jaoi 856 |
. . . . . . . 8
β’ ((π = β β¨ π = β) β (π¦ β π β π¦ β β)) |
16 | 8, 9, 15 | 3syl 18 |
. . . . . . 7
β’ (π β (π¦ β π β π¦ β β)) |
17 | 16 | imp 408 |
. . . . . 6
β’ ((π β§ π¦ β π) β π¦ β β) |
18 | | expgrowthi.k |
. . . . . . . 8
β’ (π β πΎ β β) |
19 | | mulcl 11143 |
. . . . . . . 8
β’ ((πΎ β β β§ π¦ β β) β (πΎ Β· π¦) β β) |
20 | 18, 19 | sylan 581 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (πΎ Β· π¦) β β) |
21 | | efcl 15973 |
. . . . . . 7
β’ ((πΎ Β· π¦) β β β (expβ(πΎ Β· π¦)) β β) |
22 | 20, 21 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β β) β (expβ(πΎ Β· π¦)) β β) |
23 | 17, 22 | syldan 592 |
. . . . 5
β’ ((π β§ π¦ β π) β (expβ(πΎ Β· π¦)) β β) |
24 | | ovexd 7396 |
. . . . 5
β’ ((π β§ π¦ β π) β (πΎ Β· (expβ(πΎ Β· π¦))) β V) |
25 | | cnelprrecn 11152 |
. . . . . . . 8
β’ β
β {β, β} |
26 | 25 | a1i 11 |
. . . . . . 7
β’ (π β β β {β,
β}) |
27 | 17, 20 | syldan 592 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (πΎ Β· π¦) β β) |
28 | 18 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β π) β πΎ β β) |
29 | | efcl 15973 |
. . . . . . . 8
β’ (π₯ β β β
(expβπ₯) β
β) |
30 | 29 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (expβπ₯) β
β) |
31 | | 1cnd 11158 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β 1 β β) |
32 | 8 | dvmptid 25344 |
. . . . . . . . 9
β’ (π β (π D (π¦ β π β¦ π¦)) = (π¦ β π β¦ 1)) |
33 | 8, 17, 31, 32, 18 | dvmptcmul 25351 |
. . . . . . . 8
β’ (π β (π D (π¦ β π β¦ (πΎ Β· π¦))) = (π¦ β π β¦ (πΎ Β· 1))) |
34 | 18 | mulridd 11180 |
. . . . . . . . 9
β’ (π β (πΎ Β· 1) = πΎ) |
35 | 34 | mpteq2dv 5211 |
. . . . . . . 8
β’ (π β (π¦ β π β¦ (πΎ Β· 1)) = (π¦ β π β¦ πΎ)) |
36 | 33, 35 | eqtrd 2773 |
. . . . . . 7
β’ (π β (π D (π¦ β π β¦ (πΎ Β· π¦))) = (π¦ β π β¦ πΎ)) |
37 | | dvef 25367 |
. . . . . . . . 9
β’ (β
D exp) = exp |
38 | | eff 15972 |
. . . . . . . . . . . 12
β’
exp:ββΆβ |
39 | | ffn 6672 |
. . . . . . . . . . . 12
β’
(exp:ββΆβ β exp Fn β) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . 11
β’ exp Fn
β |
41 | | dffn5 6905 |
. . . . . . . . . . 11
β’ (exp Fn
β β exp = (π₯
β β β¦ (expβπ₯))) |
42 | 40, 41 | mpbi 229 |
. . . . . . . . . 10
β’ exp =
(π₯ β β β¦
(expβπ₯)) |
43 | 42 | oveq2i 7372 |
. . . . . . . . 9
β’ (β
D exp) = (β D (π₯
β β β¦ (expβπ₯))) |
44 | 37, 43, 42 | 3eqtr3i 2769 |
. . . . . . . 8
β’ (β
D (π₯ β β β¦
(expβπ₯))) = (π₯ β β β¦
(expβπ₯)) |
45 | 44 | a1i 11 |
. . . . . . 7
β’ (π β (β D (π₯ β β β¦
(expβπ₯))) = (π₯ β β β¦
(expβπ₯))) |
46 | | fveq2 6846 |
. . . . . . 7
β’ (π₯ = (πΎ Β· π¦) β (expβπ₯) = (expβ(πΎ Β· π¦))) |
47 | 8, 26, 27, 28, 30, 30, 36, 45, 46, 46 | dvmptco 25359 |
. . . . . 6
β’ (π β (π D (π¦ β π β¦ (expβ(πΎ Β· π¦)))) = (π¦ β π β¦ ((expβ(πΎ Β· π¦)) Β· πΎ))) |
48 | | mulcom 11145 |
. . . . . . . . 9
β’
(((expβ(πΎ
Β· π¦)) β β
β§ πΎ β β)
β ((expβ(πΎ
Β· π¦)) Β· πΎ) = (πΎ Β· (expβ(πΎ Β· π¦)))) |
49 | 23, 18, 48 | syl2anr 598 |
. . . . . . . 8
β’ ((π β§ (π β§ π¦ β π)) β ((expβ(πΎ Β· π¦)) Β· πΎ) = (πΎ Β· (expβ(πΎ Β· π¦)))) |
50 | 49 | anabss5 667 |
. . . . . . 7
β’ ((π β§ π¦ β π) β ((expβ(πΎ Β· π¦)) Β· πΎ) = (πΎ Β· (expβ(πΎ Β· π¦)))) |
51 | 50 | mpteq2dva 5209 |
. . . . . 6
β’ (π β (π¦ β π β¦ ((expβ(πΎ Β· π¦)) Β· πΎ)) = (π¦ β π β¦ (πΎ Β· (expβ(πΎ Β· π¦))))) |
52 | 47, 51 | eqtrd 2773 |
. . . . 5
β’ (π β (π D (π¦ β π β¦ (expβ(πΎ Β· π¦)))) = (π¦ β π β¦ (πΎ Β· (expβ(πΎ Β· π¦))))) |
53 | | expgrowthi.y0 |
. . . . 5
β’ (π β πΆ β β) |
54 | 8, 23, 24, 52, 53 | dvmptcmul 25351 |
. . . 4
β’ (π β (π D (π¦ β π β¦ (πΆ Β· (expβ(πΎ Β· π¦))))) = (π¦ β π β¦ (πΆ Β· (πΎ Β· (expβ(πΎ Β· π¦)))))) |
55 | 53, 18, 23 | 3anim123i 1152 |
. . . . . . . 8
β’ ((π β§ π β§ (π β§ π¦ β π)) β (πΆ β β β§ πΎ β β β§ (expβ(πΎ Β· π¦)) β β)) |
56 | 55 | 3anidm12 1420 |
. . . . . . 7
β’ ((π β§ (π β§ π¦ β π)) β (πΆ β β β§ πΎ β β β§ (expβ(πΎ Β· π¦)) β β)) |
57 | 56 | anabss5 667 |
. . . . . 6
β’ ((π β§ π¦ β π) β (πΆ β β β§ πΎ β β β§ (expβ(πΎ Β· π¦)) β β)) |
58 | | mul12 11328 |
. . . . . 6
β’ ((πΆ β β β§ πΎ β β β§
(expβ(πΎ Β·
π¦)) β β) β
(πΆ Β· (πΎ Β· (expβ(πΎ Β· π¦)))) = (πΎ Β· (πΆ Β· (expβ(πΎ Β· π¦))))) |
59 | 57, 58 | syl 17 |
. . . . 5
β’ ((π β§ π¦ β π) β (πΆ Β· (πΎ Β· (expβ(πΎ Β· π¦)))) = (πΎ Β· (πΆ Β· (expβ(πΎ Β· π¦))))) |
60 | 59 | mpteq2dva 5209 |
. . . 4
β’ (π β (π¦ β π β¦ (πΆ Β· (πΎ Β· (expβ(πΎ Β· π¦))))) = (π¦ β π β¦ (πΎ Β· (πΆ Β· (expβ(πΎ Β· π¦)))))) |
61 | 54, 60 | eqtrd 2773 |
. . 3
β’ (π β (π D (π¦ β π β¦ (πΆ Β· (expβ(πΎ Β· π¦))))) = (π¦ β π β¦ (πΎ Β· (πΆ Β· (expβ(πΎ Β· π¦)))))) |
62 | 7, 61 | eqtrid 2785 |
. 2
β’ (π β (π D π) = (π¦ β π β¦ (πΎ Β· (πΆ Β· (expβ(πΎ Β· π¦)))))) |
63 | | ovexd 7396 |
. . 3
β’ ((π β§ π¦ β π) β (πΆ Β· (expβ(πΎ Β· π¦))) β V) |
64 | | fconstmpt 5698 |
. . . 4
β’ (π Γ {πΎ}) = (π¦ β π β¦ πΎ) |
65 | 64 | a1i 11 |
. . 3
β’ (π β (π Γ {πΎ}) = (π¦ β π β¦ πΎ)) |
66 | 6 | a1i 11 |
. . 3
β’ (π β π = (π¦ β π β¦ (πΆ Β· (expβ(πΎ Β· π¦))))) |
67 | 8, 28, 63, 65, 66 | offval2 7641 |
. 2
β’ (π β ((π Γ {πΎ}) βf Β· π) = (π¦ β π β¦ (πΎ Β· (πΆ Β· (expβ(πΎ Β· π¦)))))) |
68 | 62, 67 | eqtr4d 2776 |
1
β’ (π β (π D π) = ((π Γ {πΎ}) βf Β· π)) |