Step | Hyp | Ref
| Expression |
1 | | binomcxplem.d |
. . . . 5
β’ π· = (β‘abs β (0[,)π
)) |
2 | | nfcv 2904 |
. . . . . 6
β’
β²πβ‘abs |
3 | | nfcv 2904 |
. . . . . . 7
β’
β²π0 |
4 | | nfcv 2904 |
. . . . . . 7
β’
β²π[,) |
5 | | binomcxplem.r |
. . . . . . . 8
β’ π
= sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) |
6 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π
+ |
7 | | binomcxplem.s |
. . . . . . . . . . . . . 14
β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
8 | | nfmpt1 5214 |
. . . . . . . . . . . . . 14
β’
β²π(π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
9 | 7, 8 | nfcxfr 2902 |
. . . . . . . . . . . . 13
β’
β²ππ |
10 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²ππ |
11 | 9, 10 | nffv 6853 |
. . . . . . . . . . . 12
β’
β²π(πβπ) |
12 | 3, 6, 11 | nfseq 13922 |
. . . . . . . . . . 11
β’
β²πseq0(
+ , (πβπ)) |
13 | 12 | nfel1 2920 |
. . . . . . . . . 10
β’
β²πseq0( + ,
(πβπ)) β dom β |
14 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²πβ |
15 | 13, 14 | nfrabw 3439 |
. . . . . . . . 9
β’
β²π{π β β β£ seq0( + , (πβπ)) β dom β } |
16 | | nfcv 2904 |
. . . . . . . . 9
β’
β²πβ* |
17 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π
< |
18 | 15, 16, 17 | nfsup 9392 |
. . . . . . . 8
β’
β²πsup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) |
19 | 5, 18 | nfcxfr 2902 |
. . . . . . 7
β’
β²ππ
|
20 | 3, 4, 19 | nfov 7388 |
. . . . . 6
β’
β²π(0[,)π
) |
21 | 2, 20 | nfima 6022 |
. . . . 5
β’
β²π(β‘abs
β (0[,)π
)) |
22 | 1, 21 | nfcxfr 2902 |
. . . 4
β’
β²ππ· |
23 | | nfcv 2904 |
. . . 4
β’
β²π¦π· |
24 | | nfcv 2904 |
. . . 4
β’
β²π¦((1 +
π)βπ-πΆ) |
25 | | nfcv 2904 |
. . . 4
β’
β²π((1 +
π¦)βπ-πΆ) |
26 | | oveq2 7366 |
. . . . 5
β’ (π = π¦ β (1 + π) = (1 + π¦)) |
27 | 26 | oveq1d 7373 |
. . . 4
β’ (π = π¦ β ((1 + π)βπ-πΆ) = ((1 + π¦)βπ-πΆ)) |
28 | 22, 23, 24, 25, 27 | cbvmptf 5215 |
. . 3
β’ (π β π· β¦ ((1 + π)βπ-πΆ)) = (π¦ β π· β¦ ((1 + π¦)βπ-πΆ)) |
29 | 28 | oveq2i 7369 |
. 2
β’ (β
D (π β π· β¦ ((1 + π)βπ-πΆ))) = (β D (π¦ β π· β¦ ((1 + π¦)βπ-πΆ))) |
30 | | cnelprrecn 11149 |
. . . . 5
β’ β
β {β, β} |
31 | 30 | a1i 11 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β β
β {β, β}) |
32 | | 1cnd 11155 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β 1 β β) |
33 | | cnvimass 6034 |
. . . . . . . . . 10
β’ (β‘abs β (0[,)π
)) β dom abs |
34 | 1, 33 | eqsstri 3979 |
. . . . . . . . 9
β’ π· β dom
abs |
35 | | absf 15228 |
. . . . . . . . . 10
β’
abs:ββΆβ |
36 | 35 | fdmi 6681 |
. . . . . . . . 9
β’ dom abs =
β |
37 | 34, 36 | sseqtri 3981 |
. . . . . . . 8
β’ π· β
β |
38 | 37 | a1i 11 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β π· β
β) |
39 | 38 | sselda 3945 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β π¦ β β) |
40 | 32, 39 | addcld 11179 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β (1 + π¦) β β) |
41 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β (1 + π¦) β
β) |
42 | | 1cnd 11155 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β 1 β
β) |
43 | 39 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β π¦ β β) |
44 | 42, 43 | pncan2d 11519 |
. . . . . . . . 9
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β ((1 + π¦) β 1) = π¦) |
45 | | 1red 11161 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β 1 β
β) |
46 | 41, 45 | resubcld 11588 |
. . . . . . . . 9
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β ((1 + π¦) β 1) β
β) |
47 | 44, 46 | eqeltrrd 2835 |
. . . . . . . 8
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β π¦ β β) |
48 | | 1pneg1e0 12277 |
. . . . . . . . 9
β’ (1 + -1)
= 0 |
49 | | 1red 11161 |
. . . . . . . . . . 11
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β 1 β
β) |
50 | 49 | renegcld 11587 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β -1 β
β) |
51 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β π¦ β β) |
52 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . . 20
β’
(abs:ββΆβ β abs Fn β) |
53 | | elpreima 7009 |
. . . . . . . . . . . . . . . . . . . 20
β’ (abs Fn
β β (π¦ β
(β‘abs β (0[,)π
)) β (π¦ β β β§ (absβπ¦) β (0[,)π
)))) |
54 | 35, 52, 53 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (β‘abs β (0[,)π
)) β (π¦ β β β§ (absβπ¦) β (0[,)π
))) |
55 | 54 | simprbi 498 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β (β‘abs β (0[,)π
)) β (absβπ¦) β (0[,)π
)) |
56 | 55, 1 | eleq2s 2852 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β π· β (absβπ¦) β (0[,)π
)) |
57 | | 0re 11162 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
β |
58 | | ssrab2 4038 |
. . . . . . . . . . . . . . . . . . . . 21
β’ {π β β β£ seq0( +
, (πβπ)) β dom β } β
β |
59 | | ressxr 11204 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
β β* |
60 | 58, 59 | sstri 3954 |
. . . . . . . . . . . . . . . . . . . 20
β’ {π β β β£ seq0( +
, (πβπ)) β dom β } β
β* |
61 | | supxrcl 13240 |
. . . . . . . . . . . . . . . . . . . 20
β’ ({π β β β£ seq0( +
, (πβπ)) β dom β } β
β* β sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) β β*) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’
sup({π β
β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) β β* |
63 | 5, 62 | eqeltri 2830 |
. . . . . . . . . . . . . . . . . 18
β’ π
β
β* |
64 | | elico2 13334 |
. . . . . . . . . . . . . . . . . 18
β’ ((0
β β β§ π
β β*) β ((absβπ¦) β (0[,)π
) β ((absβπ¦) β β β§ 0 β€
(absβπ¦) β§
(absβπ¦) < π
))) |
65 | 57, 63, 64 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
β’
((absβπ¦)
β (0[,)π
) β
((absβπ¦) β
β β§ 0 β€ (absβπ¦) β§ (absβπ¦) < π
)) |
66 | 56, 65 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π· β ((absβπ¦) β β β§ 0 β€
(absβπ¦) β§
(absβπ¦) < π
)) |
67 | 66 | simp3d 1145 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π· β (absβπ¦) < π
) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β (absβπ¦) < π
) |
69 | | binomcxp.a |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β
β+) |
70 | | binomcxp.b |
. . . . . . . . . . . . . . . 16
β’ (π β π΅ β β) |
71 | | binomcxp.lt |
. . . . . . . . . . . . . . . 16
β’ (π β (absβπ΅) < (absβπ΄)) |
72 | | binomcxp.c |
. . . . . . . . . . . . . . . 16
β’ (π β πΆ β β) |
73 | | binomcxplem.f |
. . . . . . . . . . . . . . . 16
β’ πΉ = (π β β0 β¦ (πΆCππ)) |
74 | 69, 70, 71, 72, 73, 7, 5 | binomcxplemradcnv 42720 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β π
= 1) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β π
= 1) |
76 | 68, 75 | breqtrd 5132 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β (absβπ¦) < 1) |
77 | 76 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β (absβπ¦) < 1) |
78 | 51, 49 | absltd 15320 |
. . . . . . . . . . . 12
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β ((absβπ¦) < 1 β (-1 < π¦ β§ π¦ < 1))) |
79 | 77, 78 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β (-1 < π¦ β§ π¦ < 1)) |
80 | 79 | simpld 496 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β -1 < π¦) |
81 | 50, 51, 49, 80 | ltadd2dd 11319 |
. . . . . . . . 9
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β (1 + -1) < (1 +
π¦)) |
82 | 48, 81 | eqbrtrrid 5142 |
. . . . . . . 8
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ π¦ β β) β 0 < (1 + π¦)) |
83 | 47, 82 | syldan 592 |
. . . . . . 7
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β 0 < (1 + π¦)) |
84 | 41, 83 | elrpd 12959 |
. . . . . 6
β’ ((((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β§ (1 + π¦) β β) β (1 + π¦) β
β+) |
85 | 84 | ex 414 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β ((1 + π¦) β β β (1 + π¦) β
β+)) |
86 | | eqid 2733 |
. . . . . 6
β’ (β
β (-β(,]0)) = (β β (-β(,]0)) |
87 | 86 | ellogdm 26010 |
. . . . 5
β’ ((1 +
π¦) β (β β
(-β(,]0)) β ((1 + π¦) β β β§ ((1 + π¦) β β β (1 +
π¦) β
β+))) |
88 | 40, 85, 87 | sylanbrc 584 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β (1 + π¦) β (β β
(-β(,]0))) |
89 | | eldifi 4087 |
. . . . . 6
β’ (π₯ β (β β
(-β(,]0)) β π₯
β β) |
90 | 89 | adantl 483 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β (β β
(-β(,]0))) β π₯
β β) |
91 | 72 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β πΆ β
β) |
92 | 91 | negcld 11504 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β -πΆ β
β) |
93 | 92 | adantr 482 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β (β β
(-β(,]0))) β -πΆ
β β) |
94 | 90, 93 | cxpcld 26079 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β (β β
(-β(,]0))) β (π₯βπ-πΆ) β β) |
95 | | ovexd 7393 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β (β β
(-β(,]0))) β (-πΆ
Β· (π₯βπ(-πΆ β 1))) β V) |
96 | | 1cnd 11155 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β β) β 1 β
β) |
97 | | simpr 486 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β β) β π₯ β
β) |
98 | 96, 97 | addcld 11179 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β β) β (1 +
π₯) β
β) |
99 | | c0ex 11154 |
. . . . . . . . 9
β’ 0 β
V |
100 | 99 | a1i 11 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β β) β 0 β
V) |
101 | | 1cnd 11155 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΆ β β0) β 1 β
β) |
102 | 31, 101 | dvmptc 25338 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π₯ β β β¦
1)) = (π₯ β β
β¦ 0)) |
103 | 31 | dvmptid 25337 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π₯ β β β¦
π₯)) = (π₯ β β β¦ 1)) |
104 | 31, 96, 100, 102, 97, 96, 103 | dvmptadd 25340 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π₯ β β β¦
(1 + π₯))) = (π₯ β β β¦ (0 +
1))) |
105 | | 0p1e1 12280 |
. . . . . . . 8
β’ (0 + 1) =
1 |
106 | 105 | mpteq2i 5211 |
. . . . . . 7
β’ (π₯ β β β¦ (0 + 1))
= (π₯ β β β¦
1) |
107 | 104, 106 | eqtrdi 2789 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π₯ β β β¦
(1 + π₯))) = (π₯ β β β¦
1)) |
108 | | fvex 6856 |
. . . . . . . 8
β’
(TopOpenββfld) β V |
109 | | cnfldtps 24157 |
. . . . . . . . . 10
β’
βfld β TopSp |
110 | | cnfldbas 20816 |
. . . . . . . . . . 11
β’ β =
(Baseββfld) |
111 | | eqid 2733 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
112 | 110, 111 | tpsuni 22301 |
. . . . . . . . . 10
β’
(βfld β TopSp β β = βͺ (TopOpenββfld)) |
113 | 109, 112 | ax-mp 5 |
. . . . . . . . 9
β’ β =
βͺ
(TopOpenββfld) |
114 | 113 | restid 17320 |
. . . . . . . 8
β’
((TopOpenββfld) β V β
((TopOpenββfld) βΎt β) =
(TopOpenββfld)) |
115 | 108, 114 | ax-mp 5 |
. . . . . . 7
β’
((TopOpenββfld) βΎt β) =
(TopOpenββfld) |
116 | 115 | eqcomi 2742 |
. . . . . 6
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
117 | 111 | cnfldtop 24163 |
. . . . . . . 8
β’
(TopOpenββfld) β Top |
118 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (abs
β β ) = (abs β β ) |
119 | 118 | cnbl0 24153 |
. . . . . . . . . . 11
β’ (π
β β*
β (β‘abs β (0[,)π
)) = (0(ballβ(abs β
β ))π
)) |
120 | 63, 119 | ax-mp 5 |
. . . . . . . . . 10
β’ (β‘abs β (0[,)π
)) = (0(ballβ(abs β β
))π
) |
121 | 1, 120 | eqtri 2761 |
. . . . . . . . 9
β’ π· = (0(ballβ(abs β
β ))π
) |
122 | | cnxmet 24152 |
. . . . . . . . . 10
β’ (abs
β β ) β (βMetββ) |
123 | | 0cn 11152 |
. . . . . . . . . 10
β’ 0 β
β |
124 | 111 | cnfldtopn 24161 |
. . . . . . . . . . 11
β’
(TopOpenββfld) = (MetOpenβ(abs β
β )) |
125 | 124 | blopn 23872 |
. . . . . . . . . 10
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ π
β
β*) β (0(ballβ(abs β β ))π
) β
(TopOpenββfld)) |
126 | 122, 123,
63, 125 | mp3an 1462 |
. . . . . . . . 9
β’
(0(ballβ(abs β β ))π
) β
(TopOpenββfld) |
127 | 121, 126 | eqeltri 2830 |
. . . . . . . 8
β’ π· β
(TopOpenββfld) |
128 | | isopn3i 22449 |
. . . . . . . 8
β’
(((TopOpenββfld) β Top β§ π· β
(TopOpenββfld)) β
((intβ(TopOpenββfld))βπ·) = π·) |
129 | 117, 127,
128 | mp2an 691 |
. . . . . . 7
β’
((intβ(TopOpenββfld))βπ·) = π· |
130 | 129 | a1i 11 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β
((intβ(TopOpenββfld))βπ·) = π·) |
131 | 31, 98, 96, 107, 38, 116, 111, 130 | dvmptres2 25342 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π₯ β π· β¦ (1 + π₯))) = (π₯ β π· β¦ 1)) |
132 | | oveq2 7366 |
. . . . . . 7
β’ (π₯ = π¦ β (1 + π₯) = (1 + π¦)) |
133 | 132 | cbvmptv 5219 |
. . . . . 6
β’ (π₯ β π· β¦ (1 + π₯)) = (π¦ β π· β¦ (1 + π¦)) |
134 | 133 | oveq2i 7369 |
. . . . 5
β’ (β
D (π₯ β π· β¦ (1 + π₯))) = (β D (π¦ β π· β¦ (1 + π¦))) |
135 | | eqidd 2734 |
. . . . . 6
β’ (π₯ = π¦ β 1 = 1) |
136 | 135 | cbvmptv 5219 |
. . . . 5
β’ (π₯ β π· β¦ 1) = (π¦ β π· β¦ 1) |
137 | 131, 134,
136 | 3eqtr3g 2796 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π¦ β π· β¦ (1 + π¦))) = (π¦ β π· β¦ 1)) |
138 | 86 | dvcncxp1 26112 |
. . . . 5
β’ (-πΆ β β β (β
D (π₯ β (β
β (-β(,]0)) β¦ (π₯βπ-πΆ))) = (π₯ β (β β (-β(,]0))
β¦ (-πΆ Β· (π₯βπ(-πΆ β 1))))) |
139 | 92, 138 | syl 17 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π₯ β (β
β (-β(,]0)) β¦ (π₯βπ-πΆ))) = (π₯ β (β β (-β(,]0))
β¦ (-πΆ Β· (π₯βπ(-πΆ β 1))))) |
140 | | oveq1 7365 |
. . . 4
β’ (π₯ = (1 + π¦) β (π₯βπ-πΆ) = ((1 + π¦)βπ-πΆ)) |
141 | | oveq1 7365 |
. . . . 5
β’ (π₯ = (1 + π¦) β (π₯βπ(-πΆ β 1)) = ((1 + π¦)βπ(-πΆ β 1))) |
142 | 141 | oveq2d 7374 |
. . . 4
β’ (π₯ = (1 + π¦) β (-πΆ Β· (π₯βπ(-πΆ β 1))) = (-πΆ Β· ((1 + π¦)βπ(-πΆ β 1)))) |
143 | 31, 31, 88, 32, 94, 95, 137, 139, 140, 142 | dvmptco 25352 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π¦ β π· β¦ ((1 + π¦)βπ-πΆ))) = (π¦ β π· β¦ ((-πΆ Β· ((1 + π¦)βπ(-πΆ β 1))) Β·
1))) |
144 | 91 | adantr 482 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β πΆ β β) |
145 | 144 | negcld 11504 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β -πΆ β β) |
146 | 145, 32 | subcld 11517 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β (-πΆ β 1) β β) |
147 | 40, 146 | cxpcld 26079 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β ((1 + π¦)βπ(-πΆ β 1)) β
β) |
148 | 145, 147 | mulcld 11180 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β (-πΆ Β· ((1 + π¦)βπ(-πΆ β 1))) β
β) |
149 | 148 | mulid1d 11177 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π¦ β π·) β ((-πΆ Β· ((1 + π¦)βπ(-πΆ β 1))) Β· 1) =
(-πΆ Β· ((1 + π¦)βπ(-πΆ β 1)))) |
150 | 149 | mpteq2dva 5206 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β (π¦ β π· β¦ ((-πΆ Β· ((1 + π¦)βπ(-πΆ β 1))) Β· 1)) =
(π¦ β π· β¦ (-πΆ Β· ((1 + π¦)βπ(-πΆ β 1))))) |
151 | | nfcv 2904 |
. . . . 5
β’
β²π(-πΆ Β· ((1 + π¦)βπ(-πΆ β 1))) |
152 | | nfcv 2904 |
. . . . 5
β’
β²π¦(-πΆ Β· ((1 + π)βπ(-πΆ β 1))) |
153 | | oveq2 7366 |
. . . . . . 7
β’ (π¦ = π β (1 + π¦) = (1 + π)) |
154 | 153 | oveq1d 7373 |
. . . . . 6
β’ (π¦ = π β ((1 + π¦)βπ(-πΆ β 1)) = ((1 + π)βπ(-πΆ β 1))) |
155 | 154 | oveq2d 7374 |
. . . . 5
β’ (π¦ = π β (-πΆ Β· ((1 + π¦)βπ(-πΆ β 1))) = (-πΆ Β· ((1 + π)βπ(-πΆ β 1)))) |
156 | 23, 22, 151, 152, 155 | cbvmptf 5215 |
. . . 4
β’ (π¦ β π· β¦ (-πΆ Β· ((1 + π¦)βπ(-πΆ β 1)))) = (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1)))) |
157 | 156 | a1i 11 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β (π¦ β π· β¦ (-πΆ Β· ((1 + π¦)βπ(-πΆ β 1)))) = (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))) |
158 | 143, 150,
157 | 3eqtrd 2777 |
. 2
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π¦ β π· β¦ ((1 + π¦)βπ-πΆ))) = (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))) |
159 | 29, 158 | eqtrid 2785 |
1
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π β π· β¦ ((1 + π)βπ-πΆ))) = (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))) |