Step | Hyp | Ref
| Expression |
1 | | binomcxplem.p |
. . . . . . 7
β’ π = (π β π· β¦ Ξ£π β β0 ((πβπ)βπ)) |
2 | | binomcxplem.d |
. . . . . . . . 9
β’ π· = (β‘abs β (0[,)π
)) |
3 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²πβ‘abs |
4 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π0 |
5 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π[,) |
6 | | binomcxplem.r |
. . . . . . . . . . . 12
β’ π
= sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) |
7 | | nfcv 2908 |
. . . . . . . . . . . . . . . 16
β’
β²π
+ |
8 | | binomcxplem.s |
. . . . . . . . . . . . . . . . . 18
β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
9 | | nfmpt1 5218 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
10 | 8, 9 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . 17
β’
β²ππ |
11 | | nfcv 2908 |
. . . . . . . . . . . . . . . . 17
β’
β²ππ |
12 | 10, 11 | nffv 6857 |
. . . . . . . . . . . . . . . 16
β’
β²π(πβπ) |
13 | 4, 7, 12 | nfseq 13923 |
. . . . . . . . . . . . . . 15
β’
β²πseq0(
+ , (πβπ)) |
14 | 13 | nfel1 2924 |
. . . . . . . . . . . . . 14
β’
β²πseq0( + ,
(πβπ)) β dom β |
15 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²πβ |
16 | 14, 15 | nfrabw 3443 |
. . . . . . . . . . . . 13
β’
β²π{π β β β£ seq0( + , (πβπ)) β dom β } |
17 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²πβ* |
18 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π
< |
19 | 16, 17, 18 | nfsup 9394 |
. . . . . . . . . . . 12
β’
β²πsup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) |
20 | 6, 19 | nfcxfr 2906 |
. . . . . . . . . . 11
β’
β²ππ
|
21 | 4, 5, 20 | nfov 7392 |
. . . . . . . . . 10
β’
β²π(0[,)π
) |
22 | 3, 21 | nfima 6026 |
. . . . . . . . 9
β’
β²π(β‘abs
β (0[,)π
)) |
23 | 2, 22 | nfcxfr 2906 |
. . . . . . . 8
β’
β²ππ· |
24 | | nfcv 2908 |
. . . . . . . 8
β’
β²π₯π· |
25 | | nfcv 2908 |
. . . . . . . 8
β’
β²π₯Ξ£π β β0 ((πβπ)βπ) |
26 | | nfcv 2908 |
. . . . . . . . 9
β’
β²πβ0 |
27 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²ππ₯ |
28 | 10, 27 | nffv 6857 |
. . . . . . . . . 10
β’
β²π(πβπ₯) |
29 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²ππ |
30 | 28, 29 | nffv 6857 |
. . . . . . . . 9
β’
β²π((πβπ₯)βπ) |
31 | 26, 30 | nfsum 15582 |
. . . . . . . 8
β’
β²πΞ£π β β0 ((πβπ₯)βπ) |
32 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π = π₯ β§ π β β0) β π = π₯) |
33 | 32 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π = π₯ β§ π β β0) β (πβπ) = (πβπ₯)) |
34 | 33 | fveq1d 6849 |
. . . . . . . . 9
β’ ((π = π₯ β§ π β β0) β ((πβπ)βπ) = ((πβπ₯)βπ)) |
35 | 34 | sumeq2dv 15595 |
. . . . . . . 8
β’ (π = π₯ β Ξ£π β β0 ((πβπ)βπ) = Ξ£π β β0 ((πβπ₯)βπ)) |
36 | 23, 24, 25, 31, 35 | cbvmptf 5219 |
. . . . . . 7
β’ (π β π· β¦ Ξ£π β β0 ((πβπ)βπ)) = (π₯ β π· β¦ Ξ£π β β0 ((πβπ₯)βπ)) |
37 | 1, 36 | eqtri 2765 |
. . . . . 6
β’ π = (π₯ β π· β¦ Ξ£π β β0 ((πβπ₯)βπ)) |
38 | 37 | a1i 11 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β π = (π₯ β π· β¦ Ξ£π β β0 ((πβπ₯)βπ))) |
39 | | simplr 768 |
. . . . . . . 8
β’ ((((π β§ Β¬ πΆ β β0) β§ π₯ = (π΅ / π΄)) β§ π β β0) β π₯ = (π΅ / π΄)) |
40 | 39 | fveq2d 6851 |
. . . . . . 7
β’ ((((π β§ Β¬ πΆ β β0) β§ π₯ = (π΅ / π΄)) β§ π β β0) β (πβπ₯) = (πβ(π΅ / π΄))) |
41 | 40 | fveq1d 6849 |
. . . . . 6
β’ ((((π β§ Β¬ πΆ β β0) β§ π₯ = (π΅ / π΄)) β§ π β β0) β ((πβπ₯)βπ) = ((πβ(π΅ / π΄))βπ)) |
42 | 41 | sumeq2dv 15595 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ = (π΅ / π΄)) β Ξ£π β β0 ((πβπ₯)βπ) = Ξ£π β β0 ((πβ(π΅ / π΄))βπ)) |
43 | | binomcxp.b |
. . . . . . . . 9
β’ (π β π΅ β β) |
44 | 43 | recnd 11190 |
. . . . . . . 8
β’ (π β π΅ β β) |
45 | 44 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β π΅ β
β) |
46 | | binomcxp.a |
. . . . . . . . 9
β’ (π β π΄ β
β+) |
47 | 46 | rpcnd 12966 |
. . . . . . . 8
β’ (π β π΄ β β) |
48 | 47 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β π΄ β
β) |
49 | | 0red 11165 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β 0 β
β) |
50 | 45 | abscld 15328 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β
(absβπ΅) β
β) |
51 | 48 | abscld 15328 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β
(absβπ΄) β
β) |
52 | 45 | absge0d 15336 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β 0 β€
(absβπ΅)) |
53 | | binomcxp.lt |
. . . . . . . . . . 11
β’ (π β (absβπ΅) < (absβπ΄)) |
54 | 53 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β
(absβπ΅) <
(absβπ΄)) |
55 | 49, 50, 51, 52, 54 | lelttrd 11320 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΆ β β0) β 0 <
(absβπ΄)) |
56 | 55 | gt0ne0d 11726 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β
(absβπ΄) β
0) |
57 | 48 | abs00ad 15182 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΆ β β0) β
((absβπ΄) = 0 β
π΄ = 0)) |
58 | 57 | necon3bid 2989 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β
((absβπ΄) β 0
β π΄ β
0)) |
59 | 56, 58 | mpbid 231 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β π΄ β 0) |
60 | 45, 48, 59 | divcld 11938 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β (π΅ / π΄) β β) |
61 | 60 | abscld 15328 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β
(absβ(π΅ / π΄)) β
β) |
62 | 60 | absge0d 15336 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β 0 β€
(absβ(π΅ / π΄))) |
63 | 51 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β
(absβπ΄) β
β) |
64 | 63 | mulid1d 11179 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β
((absβπ΄) Β· 1)
= (absβπ΄)) |
65 | 54, 64 | breqtrrd 5138 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΆ β β0) β
(absβπ΅) <
((absβπ΄) Β·
1)) |
66 | | 1red 11163 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β 1 β
β) |
67 | 51, 55 | elrpd 12961 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β
(absβπ΄) β
β+) |
68 | 50, 66, 67 | ltdivmuld 13015 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΆ β β0) β
(((absβπ΅) /
(absβπ΄)) < 1
β (absβπ΅) <
((absβπ΄) Β·
1))) |
69 | 65, 68 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β
((absβπ΅) /
(absβπ΄)) <
1) |
70 | 45, 48, 59 | absdivd 15347 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β
(absβ(π΅ / π΄)) = ((absβπ΅) / (absβπ΄))) |
71 | | binomcxp.c |
. . . . . . . . 9
β’ (π β πΆ β β) |
72 | | binomcxplem.f |
. . . . . . . . 9
β’ πΉ = (π β β0 β¦ (πΆCππ)) |
73 | 46, 43, 53, 71, 72, 8, 6 | binomcxplemradcnv 42706 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β π
= 1) |
74 | 69, 70, 73 | 3brtr4d 5142 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β
(absβ(π΅ / π΄)) < π
) |
75 | | 0re 11164 |
. . . . . . . 8
β’ 0 β
β |
76 | | ssrab2 4042 |
. . . . . . . . . . 11
β’ {π β β β£ seq0( +
, (πβπ)) β dom β } β
β |
77 | | ressxr 11206 |
. . . . . . . . . . 11
β’ β
β β* |
78 | 76, 77 | sstri 3958 |
. . . . . . . . . 10
β’ {π β β β£ seq0( +
, (πβπ)) β dom β } β
β* |
79 | | supxrcl 13241 |
. . . . . . . . . 10
β’ ({π β β β£ seq0( +
, (πβπ)) β dom β } β
β* β sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) β β*) |
80 | 78, 79 | ax-mp 5 |
. . . . . . . . 9
β’
sup({π β
β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) β β* |
81 | 6, 80 | eqeltri 2834 |
. . . . . . . 8
β’ π
β
β* |
82 | | elico2 13335 |
. . . . . . . 8
β’ ((0
β β β§ π
β β*) β ((absβ(π΅ / π΄)) β (0[,)π
) β ((absβ(π΅ / π΄)) β β β§ 0 β€
(absβ(π΅ / π΄)) β§ (absβ(π΅ / π΄)) < π
))) |
83 | 75, 81, 82 | mp2an 691 |
. . . . . . 7
β’
((absβ(π΅ /
π΄)) β (0[,)π
) β ((absβ(π΅ / π΄)) β β β§ 0 β€
(absβ(π΅ / π΄)) β§ (absβ(π΅ / π΄)) < π
)) |
84 | 61, 62, 74, 83 | syl3anbrc 1344 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β
(absβ(π΅ / π΄)) β (0[,)π
)) |
85 | 2 | eleq2i 2830 |
. . . . . . 7
β’ ((π΅ / π΄) β π· β (π΅ / π΄) β (β‘abs β (0[,)π
))) |
86 | | absf 15229 |
. . . . . . . 8
β’
abs:ββΆβ |
87 | | ffn 6673 |
. . . . . . . 8
β’
(abs:ββΆβ β abs Fn β) |
88 | | elpreima 7013 |
. . . . . . . 8
β’ (abs Fn
β β ((π΅ / π΄) β (β‘abs β (0[,)π
)) β ((π΅ / π΄) β β β§ (absβ(π΅ / π΄)) β (0[,)π
)))) |
89 | 86, 87, 88 | mp2b 10 |
. . . . . . 7
β’ ((π΅ / π΄) β (β‘abs β (0[,)π
)) β ((π΅ / π΄) β β β§ (absβ(π΅ / π΄)) β (0[,)π
))) |
90 | 85, 89 | bitri 275 |
. . . . . 6
β’ ((π΅ / π΄) β π· β ((π΅ / π΄) β β β§ (absβ(π΅ / π΄)) β (0[,)π
))) |
91 | 60, 84, 90 | sylanbrc 584 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β (π΅ / π΄) β π·) |
92 | | sumex 15579 |
. . . . . 6
β’
Ξ£π β
β0 ((πβ(π΅ / π΄))βπ) β V |
93 | 92 | a1i 11 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β
Ξ£π β
β0 ((πβ(π΅ / π΄))βπ) β V) |
94 | 38, 42, 91, 93 | fvmptd 6960 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β (πβ(π΅ / π΄)) = Ξ£π β β0 ((πβ(π΅ / π΄))βπ)) |
95 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (abs
β β ) = (abs β β ) |
96 | 95 | cnbl0 24153 |
. . . . . . . . . . . 12
β’ (π
β β*
β (β‘abs β (0[,)π
)) = (0(ballβ(abs β
β ))π
)) |
97 | 81, 96 | ax-mp 5 |
. . . . . . . . . . 11
β’ (β‘abs β (0[,)π
)) = (0(ballβ(abs β β
))π
) |
98 | 2, 97 | eqtri 2765 |
. . . . . . . . . 10
β’ π· = (0(ballβ(abs β
β ))π
) |
99 | | 0cnd 11155 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β 0 β
β) |
100 | 81 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β π
β
β*) |
101 | | mulcl 11142 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
102 | 101 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ πΆ β β0) β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
103 | | nfv 1918 |
. . . . . . . . . . . . . . 15
β’
β²π(π β§ Β¬ πΆ β
β0) |
104 | 23 | nfcri 2895 |
. . . . . . . . . . . . . . 15
β’
β²π π₯ β π· |
105 | 103, 104 | nfan 1903 |
. . . . . . . . . . . . . 14
β’
β²π((π β§ Β¬ πΆ β β0) β§ π₯ β π·) |
106 | 31 | nfel1 2924 |
. . . . . . . . . . . . . 14
β’
β²πΞ£π β β0
((πβπ₯)βπ) β β |
107 | 105, 106 | nfim 1900 |
. . . . . . . . . . . . 13
β’
β²π(((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β Ξ£π β β0 ((πβπ₯)βπ) β β) |
108 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (π β π· β π₯ β π·)) |
109 | 108 | anbi2d 630 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((π β§ Β¬ πΆ β β0) β§ π₯ β π·))) |
110 | 35 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (Ξ£π β β0 ((πβπ)βπ) β β β Ξ£π β β0
((πβπ₯)βπ) β β)) |
111 | 109, 110 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = π₯ β ((((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β0 ((πβπ)βπ) β β) β (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β Ξ£π β β0 ((πβπ₯)βπ) β β))) |
112 | | nn0uz 12812 |
. . . . . . . . . . . . . 14
β’
β0 = (β€β₯β0) |
113 | | 0zd 12518 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β 0 β β€) |
114 | | eqidd 2738 |
. . . . . . . . . . . . . 14
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((πβπ)βπ) = ((πβπ)βπ)) |
115 | | cnvimass 6038 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β‘abs β (0[,)π
)) β dom abs |
116 | 2, 115 | eqsstri 3983 |
. . . . . . . . . . . . . . . . . . 19
β’ π· β dom
abs |
117 | 86 | fdmi 6685 |
. . . . . . . . . . . . . . . . . . 19
β’ dom abs =
β |
118 | 116, 117 | sseqtri 3985 |
. . . . . . . . . . . . . . . . . 18
β’ π· β
β |
119 | 118 | sseli 3945 |
. . . . . . . . . . . . . . . . 17
β’ (π β π· β π β β) |
120 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))) |
121 | | nn0ex 12426 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β0 β V |
122 | 121 | mptex 7178 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β¦ ((πΉβπ) Β· (πβπ))) β V |
123 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (π β β0 β¦ ((πΉβπ) Β· (πβπ))) β V) |
124 | 120, 123 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (πβπ) = (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
125 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β β0) β ((πΉβπ) Β· (πβπ)) β V) |
126 | 124, 125 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β β0) β ((πβπ)βπ) = ((πΉβπ) Β· (πβπ))) |
127 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β0) β πΉ = (π β β0 β¦ (πΆCππ))) |
128 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β0) β§ π = π) β π = π) |
129 | 128 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ π = π) β (πΆCππ) = (πΆCππ)) |
130 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β0) β π β
β0) |
131 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β β0) β (πΆCππ) β V) |
132 | 127, 129,
130, 131 | fvmptd 6960 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β0) β (πΉβπ) = (πΆCππ)) |
133 | 132 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β0) β ((πΉβπ) Β· (πβπ)) = ((πΆCππ) Β· (πβπ))) |
134 | 133 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β β0) β ((πΉβπ) Β· (πβπ)) = ((πΆCππ) Β· (πβπ))) |
135 | 126, 134 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β β0) β ((πβπ)βπ) = ((πΆCππ) Β· (πβπ))) |
136 | 119, 135 | sylanl2 680 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β β0) β ((πβπ)βπ) = ((πΆCππ) Β· (πβπ))) |
137 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β β0) β πΆ β
β) |
138 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β β0) β π β
β0) |
139 | 137, 138 | bcccl 42693 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β β0) β (πΆCππ) β
β) |
140 | 119 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β π·) β§ π β β0) β π β
β) |
141 | 140, 138 | expcld 14058 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π·) β§ π β β0) β (πβπ) β β) |
142 | 139, 141 | mulcld 11182 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π·) β§ π β β0) β ((πΆCππ) Β· (πβπ)) β β) |
143 | 136, 142 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π β β0) β ((πβπ)βπ) β β) |
144 | 143 | adantllr 718 |
. . . . . . . . . . . . . 14
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((πβπ)βπ) β β) |
145 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (π₯ β π· β π β π·)) |
146 | 145 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β ((π β§ π₯ β π·) β (π β§ π β π·))) |
147 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
148 | 147 | seqeq3d 13921 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β seq0( + , (πβπ₯)) = seq0( + , (πβπ))) |
149 | 148 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (seq0( + , (πβπ₯)) β dom β β seq0( + , (πβπ)) β dom β )) |
150 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β (πΈβπ₯) = (πΈβπ)) |
151 | 150 | seqeq3d 13921 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β seq1( + , (πΈβπ₯)) = seq1( + , (πΈβπ))) |
152 | 151 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (seq1( + , (πΈβπ₯)) β dom β β seq1( + , (πΈβπ)) β dom β )) |
153 | 149, 152 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β ((seq0( + , (πβπ₯)) β dom β β§ seq1( + , (πΈβπ₯)) β dom β ) β (seq0( + ,
(πβπ)) β dom β β§ seq1( + , (πΈβπ)) β dom β ))) |
154 | 146, 153 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (((π β§ π₯ β π·) β (seq0( + , (πβπ₯)) β dom β β§ seq1( + , (πΈβπ₯)) β dom β )) β ((π β§ π β π·) β (seq0( + , (πβπ)) β dom β β§ seq1( + , (πΈβπ)) β dom β )))) |
155 | | binomcxplem.e |
. . . . . . . . . . . . . . . . . 18
β’ πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) |
156 | 46, 43, 53, 71, 72, 8, 6, 155, 2 | binomcxplemcvg 42708 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β π·) β (seq0( + , (πβπ₯)) β dom β β§ seq1( + , (πΈβπ₯)) β dom β )) |
157 | 154, 156 | chvarvv 2003 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π·) β (seq0( + , (πβπ)) β dom β β§ seq1( + , (πΈβπ)) β dom β )) |
158 | 157 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π·) β seq0( + , (πβπ)) β dom β ) |
159 | 158 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq0( + , (πβπ)) β dom β ) |
160 | 112, 113,
114, 144, 159 | isumcl 15653 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β0 ((πβπ)βπ) β β) |
161 | 107, 111,
160 | chvarfv 2234 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β Ξ£π β β0 ((πβπ₯)βπ) β β) |
162 | 161, 37 | fmptd 7067 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β π:π·βΆβ) |
163 | | 1cnd 11157 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β 1 β β) |
164 | 118 | sseli 3945 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π· β π₯ β β) |
165 | 164 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β π₯ β β) |
166 | 163, 165 | addcld 11181 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β (1 + π₯) β β) |
167 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β πΆ β β) |
168 | 167 | negcld 11506 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β -πΆ β β) |
169 | 166, 168 | cxpcld 26079 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β ((1 + π₯)βπ-πΆ) β β) |
170 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π₯((1 +
π)βπ-πΆ) |
171 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π((1 +
π₯)βπ-πΆ) |
172 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (1 + π) = (1 + π₯)) |
173 | 172 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π = π₯ β ((1 + π)βπ-πΆ) = ((1 + π₯)βπ-πΆ)) |
174 | 23, 24, 170, 171, 173 | cbvmptf 5219 |
. . . . . . . . . . . 12
β’ (π β π· β¦ ((1 + π)βπ-πΆ)) = (π₯ β π· β¦ ((1 + π₯)βπ-πΆ)) |
175 | 169, 174 | fmptd 7067 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ ((1 + π)βπ-πΆ)):π·βΆβ) |
176 | | cnex 11139 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
177 | | fex 7181 |
. . . . . . . . . . . . . . . 16
β’
((abs:ββΆβ β§ β β V) β abs β
V) |
178 | 86, 176, 177 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ abs
β V |
179 | 178 | cnvex 7867 |
. . . . . . . . . . . . . 14
β’ β‘abs β V |
180 | | imaexg 7857 |
. . . . . . . . . . . . . 14
β’ (β‘abs β V β (β‘abs β (0[,)π
)) β V) |
181 | 179, 180 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (β‘abs β (0[,)π
)) β V |
182 | 2, 181 | eqeltri 2834 |
. . . . . . . . . . . 12
β’ π· β V |
183 | 182 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β π· β V) |
184 | | inidm 4183 |
. . . . . . . . . . 11
β’ (π· β© π·) = π· |
185 | 102, 162,
175, 183, 183, 184 | off 7640 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β (π βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ))):π·βΆβ) |
186 | | 1ex 11158 |
. . . . . . . . . . . . . 14
β’ 1 β
V |
187 | 186 | fconst 6733 |
. . . . . . . . . . . . 13
β’ (π· Γ {1}):π·βΆ{1} |
188 | | fconstmpt 5699 |
. . . . . . . . . . . . . . 15
β’ (π· Γ {1}) = (π₯ β π· β¦ 1) |
189 | | nfcv 2908 |
. . . . . . . . . . . . . . . 16
β’
β²π1 |
190 | | nfcv 2908 |
. . . . . . . . . . . . . . . 16
β’
β²π₯1 |
191 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β 1 = 1) |
192 | 24, 23, 189, 190, 191 | cbvmptf 5219 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π· β¦ 1) = (π β π· β¦ 1) |
193 | 188, 192 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ (π· Γ {1}) = (π β π· β¦ 1) |
194 | 193 | feq1i 6664 |
. . . . . . . . . . . . 13
β’ ((π· Γ {1}):π·βΆ{1} β (π β π· β¦ 1):π·βΆ{1}) |
195 | 187, 194 | mpbi 229 |
. . . . . . . . . . . 12
β’ (π β π· β¦ 1):π·βΆ{1} |
196 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
β’ 1 β
β |
197 | | snssi 4773 |
. . . . . . . . . . . . 13
β’ (1 β
β β {1} β β) |
198 | 196, 197 | ax-mp 5 |
. . . . . . . . . . . 12
β’ {1}
β β |
199 | | fss 6690 |
. . . . . . . . . . . 12
β’ (((π β π· β¦ 1):π·βΆ{1} β§ {1} β β)
β (π β π· β¦ 1):π·βΆβ) |
200 | 195, 198,
199 | mp2an 691 |
. . . . . . . . . . 11
β’ (π β π· β¦ 1):π·βΆβ |
201 | 200 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ 1):π·βΆβ) |
202 | | cnelprrecn 11151 |
. . . . . . . . . . . . . . . . 17
β’ β
β {β, β} |
203 | 202 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β β
β {β, β}) |
204 | 46, 43, 53, 71, 72, 8, 6, 155, 2, 1 | binomcxplemdvsum 42709 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β D π) = (π β π· β¦ Ξ£π β β ((πΈβπ)βπ))) |
205 | 204 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ πΆ β β0) β (β
D π) = (π β π· β¦ Ξ£π β β ((πΈβπ)βπ))) |
206 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯Ξ£π β β ((πΈβπ)βπ) |
207 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²πβ |
208 | | nfmpt1 5218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) |
209 | 155, 208 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²ππΈ |
210 | 209, 27 | nffv 6857 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π(πΈβπ₯) |
211 | 210, 29 | nffv 6857 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π((πΈβπ₯)βπ) |
212 | 207, 211 | nfsum 15582 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²πΞ£π β β ((πΈβπ₯)βπ) |
213 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π = π₯ β§ π β β) β π = π₯) |
214 | 213 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π = π₯ β§ π β β) β (πΈβπ) = (πΈβπ₯)) |
215 | 214 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = π₯ β§ π β β) β ((πΈβπ)βπ) = ((πΈβπ₯)βπ)) |
216 | 215 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β Ξ£π β β ((πΈβπ)βπ) = Ξ£π β β ((πΈβπ₯)βπ)) |
217 | 23, 24, 206, 212, 216 | cbvmptf 5219 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π· β¦ Ξ£π β β ((πΈβπ)βπ)) = (π₯ β π· β¦ Ξ£π β β ((πΈβπ₯)βπ)) |
218 | 205, 217 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ πΆ β β0) β (β
D π) = (π₯ β π· β¦ Ξ£π β β ((πΈβπ₯)βπ))) |
219 | | sumex 15579 |
. . . . . . . . . . . . . . . . . . 19
β’
Ξ£π β
β ((πΈβπ₯)βπ) β V |
220 | 219 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β Ξ£π β β ((πΈβπ₯)βπ) β V) |
221 | 218, 220 | fmpt3d 7069 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β (β
D π):π·βΆV) |
222 | 221 | fdmd 6684 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β dom
(β D π) = π·) |
223 | 46, 43, 53, 71, 72, 8, 6, 155, 2 | binomcxplemdvbinom 42707 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π β π· β¦ ((1 + π)βπ-πΆ))) = (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))) |
224 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯(-πΆ Β· ((1 + π)βπ(-πΆ β 1))) |
225 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(-πΆ Β· ((1 + π₯)βπ(-πΆ β 1))) |
226 | 172 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π₯ β ((1 + π)βπ(-πΆ β 1)) = ((1 + π₯)βπ(-πΆ β 1))) |
227 | 226 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β (-πΆ Β· ((1 + π)βπ(-πΆ β 1))) = (-πΆ Β· ((1 + π₯)βπ(-πΆ β 1)))) |
228 | 23, 24, 224, 225, 227 | cbvmptf 5219 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1)))) = (π₯ β π· β¦ (-πΆ Β· ((1 + π₯)βπ(-πΆ β 1)))) |
229 | 223, 228 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π β π· β¦ ((1 + π)βπ-πΆ))) = (π₯ β π· β¦ (-πΆ Β· ((1 + π₯)βπ(-πΆ β 1))))) |
230 | 168, 163 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β (-πΆ β 1) β β) |
231 | 166, 230 | cxpcld 26079 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β ((1 + π₯)βπ(-πΆ β 1)) β
β) |
232 | 168, 231 | mulcld 11182 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β (-πΆ Β· ((1 + π₯)βπ(-πΆ β 1))) β
β) |
233 | 229, 232 | fmpt3d 7069 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π β π· β¦ ((1 + π)βπ-πΆ))):π·βΆβ) |
234 | 233 | fdmd 6684 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β dom
(β D (π β π· β¦ ((1 + π)βπ-πΆ))) = π·) |
235 | 203, 162,
175, 222, 234 | dvmulf 25323 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π βf
Β· (π β π· β¦ ((1 + π)βπ-πΆ)))) = (((β D π) βf Β· (π β π· β¦ ((1 + π)βπ-πΆ))) βf + ((β D (π β π· β¦ ((1 + π)βπ-πΆ))) βf Β· π))) |
236 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β πΆ β β) |
237 | 236 | mulid1d 11179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ Β· 1) = πΆ) |
238 | 237 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ Β· 1) + (πΆ Β· Ξ£π β β ((πΆCππ) Β· (πβπ)))) = (πΆ + (πΆ Β· Ξ£π β β ((πΆCππ) Β· (πβπ))))) |
239 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β 1 β β) |
240 | | nnuz 12813 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ β =
(β€β₯β1) |
241 | | 1zzd 12541 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β 1 β β€) |
242 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β π β
β0) |
243 | 242, 136 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β π·) β§ π β β) β ((πβπ)βπ) = ((πΆCππ) Β· (πβπ))) |
244 | 243 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πβπ)βπ) = ((πΆCππ) Β· (πβπ))) |
245 | 71 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β πΆ β
β) |
246 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β π β
β0) |
247 | 245, 246 | bcccl 42693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πΆCππ) β
β) |
248 | 242, 247 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (πΆCππ) β β) |
249 | 119 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β π β β) |
250 | 249 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β π β
β) |
251 | 250, 246 | expcld 14058 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πβπ) β β) |
252 | 242, 251 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (πβπ) β β) |
253 | 248, 252 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πΆCππ) Β· (πβπ)) β β) |
254 | | 1nn0 12436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 1 β
β0 |
255 | 254 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β π·) β 1 β
β0) |
256 | 112, 255,
143 | iserex 15548 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β π·) β (seq0( + , (πβπ)) β dom β β seq1( + , (πβπ)) β dom β )) |
257 | 158, 256 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β π·) β seq1( + , (πβπ)) β dom β ) |
258 | 257 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq1( + , (πβπ)) β dom β ) |
259 | 240, 241,
244, 253, 258 | isumcl 15653 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β ((πΆCππ) Β· (πβπ)) β β) |
260 | 236, 239,
259 | adddid 11186 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ Β· (1 + Ξ£π β β ((πΆCππ) Β· (πβπ)))) = ((πΆ Β· 1) + (πΆ Β· Ξ£π β β ((πΆCππ) Β· (πβπ))))) |
261 | 155 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1)))))) |
262 | | nnex 12166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ β
β V |
263 | 262 | mptex 7178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1)))) β V |
264 | 263 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ π β β) β (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1)))) β V) |
265 | 261, 264 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β§ π β β) β (πΈβπ) = (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) |
266 | 119, 265 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β§ π β π·) β (πΈβπ) = (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) |
267 | 266 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΈβπ) = (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) |
268 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((π Β· (πΉβπ)) Β· (πβ(π β 1))) β V) |
269 | 267, 268 | fmpt3d 7069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΈβπ):ββΆV) |
270 | 269 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΈβπ) = (π β β β¦ ((πΈβπ)βπ))) |
271 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((π β§ π β β) β§ π β β) β ((π Β· (πΉβπ)) Β· (πβ(π β 1))) β V) |
272 | 265, 271 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π β§ π β β) β§ π β β) β ((πΈβπ)βπ) = ((π Β· (πΉβπ)) Β· (πβ(π β 1)))) |
273 | 242, 132 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β§ π β β) β (πΉβπ) = (πΆCππ)) |
274 | 273 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β§ π β β) β (π Β· (πΉβπ)) = (π Β· (πΆCππ))) |
275 | 274 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β§ π β β) β ((π Β· (πΉβπ)) Β· (πβ(π β 1))) = ((π Β· (πΆCππ)) Β· (πβ(π β 1)))) |
276 | 275 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π β§ π β β) β§ π β β) β ((π Β· (πΉβπ)) Β· (πβ(π β 1))) = ((π Β· (πΆCππ)) Β· (πβ(π β 1)))) |
277 | 272, 276 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π β§ π β β) β§ π β β) β ((πΈβπ)βπ) = ((π Β· (πΆCππ)) Β· (πβ(π β 1)))) |
278 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β§ π β β) β πΆ β β) |
279 | | nnm1nn0 12461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (π β β β (π β 1) β
β0) |
280 | 279 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β§ π β β) β (π β 1) β
β0) |
281 | 278, 280 | bccp1k 42695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ π β β) β (πΆCπ((π β 1) + 1)) = ((πΆCπ(π β 1)) Β· ((πΆ β (π β 1)) / ((π β 1) + 1)))) |
282 | 242 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π β§ π β β) β π β β0) |
283 | 282 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π β§ π β β) β π β β) |
284 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π β§ π β β) β 1 β
β) |
285 | 283, 284 | npcand 11523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β§ π β β) β ((π β 1) + 1) = π) |
286 | 285 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ π β β) β (πΆCπ((π β 1) + 1)) = (πΆCππ)) |
287 | 285 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β§ π β β) β ((πΆ β (π β 1)) / ((π β 1) + 1)) = ((πΆ β (π β 1)) / π)) |
288 | 287 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ π β β) β ((πΆCπ(π β 1)) Β· ((πΆ β (π β 1)) / ((π β 1) + 1))) = ((πΆCπ(π β 1)) Β· ((πΆ β (π β 1)) / π))) |
289 | 281, 286,
288 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β§ π β β) β (πΆCππ) = ((πΆCπ(π β 1)) Β· ((πΆ β (π β 1)) / π))) |
290 | 289 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β§ π β β) β (π Β· (πΆCππ)) = (π Β· ((πΆCπ(π β 1)) Β· ((πΆ β (π β 1)) / π)))) |
291 | 278, 280 | bcccl 42693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ π β β) β (πΆCπ(π β 1)) β β) |
292 | 283, 284 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β§ π β β) β (π β 1) β β) |
293 | 278, 292 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ π β β) β (πΆ β (π β 1)) β β) |
294 | | nnne0 12194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (π β β β π β 0) |
295 | 294 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ π β β) β π β 0) |
296 | 291, 293,
283, 295 | divassd 11973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β§ π β β) β (((πΆCπ(π β 1)) Β· (πΆ β (π β 1))) / π) = ((πΆCπ(π β 1)) Β· ((πΆ β (π β 1)) / π))) |
297 | 296 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β§ π β β) β (π Β· (((πΆCπ(π β 1)) Β· (πΆ β (π β 1))) / π)) = (π Β· ((πΆCπ(π β 1)) Β· ((πΆ β (π β 1)) / π)))) |
298 | 291, 293 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β§ π β β) β ((πΆCπ(π β 1)) Β· (πΆ β (π β 1))) β
β) |
299 | 298, 283,
295 | divcan2d 11940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β§ π β β) β (π Β· (((πΆCπ(π β 1)) Β· (πΆ β (π β 1))) / π)) = ((πΆCπ(π β 1)) Β· (πΆ β (π β 1)))) |
300 | 290, 297,
299 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β§ π β β) β (π Β· (πΆCππ)) = ((πΆCπ(π β 1)) Β· (πΆ β (π β 1)))) |
301 | 300 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ π β β) β ((π Β· (πΆCππ)) Β· (πβ(π β 1))) = (((πΆCπ(π β 1)) Β· (πΆ β (π β 1))) Β· (πβ(π β 1)))) |
302 | 301 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π β§ π β β) β§ π β β) β ((π Β· (πΆCππ)) Β· (πβ(π β 1))) = (((πΆCπ(π β 1)) Β· (πΆ β (π β 1))) Β· (πβ(π β 1)))) |
303 | 291 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((π β§ π β β) β§ π β β) β (πΆCπ(π β 1)) β β) |
304 | 293 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((π β§ π β β) β§ π β β) β (πΆ β (π β 1)) β β) |
305 | 303, 304 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π β§ π β β) β§ π β β) β ((πΆCπ(π β 1)) Β· (πΆ β (π β 1))) = ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) |
306 | 305 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π β§ π β β) β§ π β β) β (((πΆCπ(π β 1)) Β· (πΆ β (π β 1))) Β· (πβ(π β 1))) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) |
307 | 277, 302,
306 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β§ π β β) β§ π β β) β ((πΈβπ)βπ) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) |
308 | 119, 307 | sylanl2 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ π β π·) β§ π β β) β ((πΈβπ)βπ) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) |
309 | 308 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πΈβπ)βπ) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) |
310 | 309 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (π β β β¦ ((πΈβπ)βπ)) = (π β β β¦ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))))) |
311 | 270, 310 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΈβπ) = (π β β β¦ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))))) |
312 | 311 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΈβπ) shift -1) = ((π β β β¦ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) shift -1)) |
313 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β β β¦ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) = (π β β β¦ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) |
314 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) β V |
315 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = (π β -1) β (π β 1) = ((π β -1) β 1)) |
316 | 315 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = (π β -1) β (πΆ β (π β 1)) = (πΆ β ((π β -1) β 1))) |
317 | 315 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = (π β -1) β (πΆCπ(π β 1)) = (πΆCπ((π β -1) β 1))) |
318 | 316, 317 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = (π β -1) β ((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) = ((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β
1)))) |
319 | 315 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = (π β -1) β (πβ(π β 1)) = (πβ((π β -1) β 1))) |
320 | 318, 319 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = (π β -1) β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) = (((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1)))
Β· (πβ((π β -1) β
1)))) |
321 | | 1pneg1e0 12279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (1 + -1)
= 0 |
322 | 321 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(β€β₯β(1 + -1)) =
(β€β₯β0) |
323 | 112, 322 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
β0 = (β€β₯β(1 +
-1)) |
324 | 241 | znegcld 12616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β -1 β β€) |
325 | 313, 314,
320, 240, 323, 241, 324 | uzmptshftfval 42700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((π β β β¦ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) shift -1) = (π β β0
β¦ (((πΆ β
((π β -1) β 1))
Β· (πΆCπ((π β -1) β 1))) Β· (πβ((π β -1) β 1))))) |
326 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π = π β (π β -1) = (π β -1)) |
327 | 326 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = π β ((π β -1) β 1) = ((π β -1) β
1)) |
328 | 327 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β (πΆ β ((π β -1) β 1)) = (πΆ β ((π β -1) β 1))) |
329 | 327 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β (πΆCπ((π β -1) β 1)) = (πΆCπ((π β -1) β 1))) |
330 | 328, 329 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β ((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1))) =
((πΆ β ((π β -1) β 1))
Β· (πΆCπ((π β -1) β 1)))) |
331 | 327 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β (πβ((π β -1) β 1)) = (πβ((π β -1) β 1))) |
332 | 330, 331 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π β (((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1)))
Β· (πβ((π β -1) β 1))) =
(((πΆ β ((π β -1) β 1))
Β· (πΆCπ((π β -1) β 1))) Β· (πβ((π β -1) β 1)))) |
333 | 332 | cbvmptv 5223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β β0
β¦ (((πΆ β
((π β -1) β 1))
Β· (πΆCπ((π β -1) β 1))) Β· (πβ((π β -1) β 1)))) = (π β β0
β¦ (((πΆ β
((π β -1) β 1))
Β· (πΆCπ((π β -1) β 1))) Β· (πβ((π β -1) β 1)))) |
334 | 333 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (π β β0 β¦ (((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1)))
Β· (πβ((π β -1) β 1)))) =
(π β
β0 β¦ (((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1)))
Β· (πβ((π β -1) β
1))))) |
335 | 312, 325,
334 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΈβπ) shift -1) = (π β β0 β¦ (((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1)))
Β· (πβ((π β -1) β
1))))) |
336 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β β0
β π β
β) |
337 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β β0
β 1 β β) |
338 | 336, 337 | subnegd 11526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β β0
β (π β -1) =
(π + 1)) |
339 | 338 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β0
β ((π β -1)
β 1) = ((π + 1)
β 1)) |
340 | 336, 337 | pncand 11520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β0
β ((π + 1) β 1)
= π) |
341 | 339, 340 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β0
β ((π β -1)
β 1) = π) |
342 | 341 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((π β -1) β 1) = π) |
343 | 342 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πΆ β ((π β -1) β 1)) = (πΆ β π)) |
344 | 342 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πΆCπ((π β -1) β 1)) =
(πΆCππ)) |
345 | 343, 344 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1))) =
((πΆ β π) Β· (πΆCππ))) |
346 | 342 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πβ((π β -1) β 1)) = (πβπ)) |
347 | 345, 346 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1)))
Β· (πβ((π β -1) β 1))) =
(((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) |
348 | 347 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (π β β0 β¦ (((πΆ β ((π β -1) β 1)) Β· (πΆCπ((π β -1) β 1)))
Β· (πβ((π β -1) β 1)))) =
(π β
β0 β¦ (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)))) |
349 | 335, 348 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΈβπ) shift -1) = (π β β0 β¦ (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)))) |
350 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) β V) |
351 | 349, 350 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (((πΈβπ) shift -1)βπ) = (((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) |
352 | 242, 351 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (((πΈβπ) shift -1)βπ) = (((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) |
353 | 336 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β π β
β) |
354 | 245, 353 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πΆ β π) β β) |
355 | 354, 247 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((πΆ β π) Β· (πΆCππ)) β β) |
356 | 355, 251 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) β β) |
357 | 242, 356 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) β β) |
358 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β ((πΈβπ)βπ) = ((πΈβπ)βπ)) |
359 | 358 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (π Β· ((πΈβπ)βπ)) = (π Β· ((πΈβπ)βπ))) |
360 | 359 | cbvmptv 5223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β β¦ (π Β· ((πΈβπ)βπ))) = (π β β β¦ (π Β· ((πΈβπ)βπ))) |
361 | 309 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (π Β· ((πΈβπ)βπ)) = (π Β· (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))))) |
362 | 249 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β π β β) |
363 | 71 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β πΆ β β) |
364 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β β β π β
β) |
365 | 364 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β π β β) |
366 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β 1 β
β) |
367 | 365, 366 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (π β 1) β β) |
368 | 363, 367 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (πΆ β (π β 1)) β β) |
369 | 279 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (π β 1) β
β0) |
370 | 363, 369 | bcccl 42693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (πΆCπ(π β 1)) β β) |
371 | 368, 370 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) β
β) |
372 | 362, 369 | expcld 14058 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (πβ(π β 1)) β β) |
373 | 362, 371,
372 | mul12d 11371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (π Β· (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (π Β· (πβ(π β 1))))) |
374 | 362, 372 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (π Β· (πβ(π β 1))) = ((πβ(π β 1)) Β· π)) |
375 | 362, 369 | expp1d 14059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (πβ((π β 1) + 1)) = ((πβ(π β 1)) Β· π)) |
376 | 285 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β ((π β 1) + 1) = π) |
377 | 376 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((π β 1) + 1) = π) |
378 | 377 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (πβ((π β 1) + 1)) = (πβπ)) |
379 | 374, 375,
378 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (π Β· (πβ(π β 1))) = (πβπ)) |
380 | 379 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (π Β· (πβ(π β 1)))) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) |
381 | 373, 380 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (π Β· (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) |
382 | 361, 381 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (π Β· ((πΈβπ)βπ)) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) |
383 | 382 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (π β β β¦ (π Β· ((πΈβπ)βπ))) = (π β β β¦ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) |
384 | 360, 383 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (π β β β¦ (π Β· ((πΈβπ)βπ))) = (π β β β¦ (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) |
385 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)) β V) |
386 | 384, 385 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((π β β β¦ (π Β· ((πΈβπ)βπ)))βπ) = (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) |
387 | 371, 252 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)) β β) |
388 | | climrel 15381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ Rel
β |
389 | 157 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β π·) β seq1( + , (πΈβπ)) β dom β ) |
390 | 389 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq1( + , (πΈβπ)) β dom β ) |
391 | | climdm 15443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (seq1( +
, (πΈβπ)) β dom β β
seq1( + , (πΈβπ)) β ( β
βseq1( + , (πΈβπ)))) |
392 | 390, 391 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq1( + , (πΈβπ)) β ( β βseq1( + , (πΈβπ)))) |
393 | | 0z 12517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ 0 β
β€ |
394 | | neg1z 12546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ -1 β
β€ |
395 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (πΈβπ) β V |
396 | 395 | seqshft 14977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((0
β β€ β§ -1 β β€) β seq0( + , ((πΈβπ) shift -1)) = (seq(0 β -1)( + , (πΈβπ)) shift -1)) |
397 | 393, 394,
396 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ seq0( + ,
((πΈβπ) shift -1)) = (seq(0 β
-1)( + , (πΈβπ)) shift -1) |
398 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ 0 β
β |
399 | 398, 196 | subnegi 11487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (0
β -1) = (0 + 1) |
400 | | 0p1e1 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (0 + 1) =
1 |
401 | 399, 400 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (0
β -1) = 1 |
402 | | seqeq1 13916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((0
β -1) = 1 β seq(0 β -1)( + , (πΈβπ)) = seq1( + , (πΈβπ))) |
403 | 401, 402 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ seq(0
β -1)( + , (πΈβπ)) = seq1( + , (πΈβπ)) |
404 | 403 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (seq(0
β -1)( + , (πΈβπ)) shift -1) = (seq1( + , (πΈβπ)) shift -1) |
405 | 397, 404 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ seq0( + ,
((πΈβπ) shift -1)) = (seq1( + , (πΈβπ)) shift -1) |
406 | 405 | breq1i 5117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (seq0( +
, ((πΈβπ) shift -1)) β ( β
βseq1( + , (πΈβπ))) β (seq1( + , (πΈβπ)) shift -1) β ( β βseq1( +
, (πΈβπ)))) |
407 | | seqex 13915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ seq1( + ,
(πΈβπ)) β V |
408 | | climshft 15465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((-1
β β€ β§ seq1( + , (πΈβπ)) β V) β ((seq1( + , (πΈβπ)) shift -1) β ( β βseq1( +
, (πΈβπ))) β seq1( + , (πΈβπ)) β ( β βseq1( + , (πΈβπ))))) |
409 | 394, 407,
408 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((seq1( +
, (πΈβπ)) shift -1) β ( β
βseq1( + , (πΈβπ))) β seq1( + , (πΈβπ)) β ( β βseq1( + , (πΈβπ)))) |
410 | 406, 409 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (seq0( +
, ((πΈβπ) shift -1)) β ( β
βseq1( + , (πΈβπ))) β seq1( + , (πΈβπ)) β ( β βseq1( + , (πΈβπ)))) |
411 | 392, 410 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq0( + , ((πΈβπ) shift -1)) β ( β βseq1( +
, (πΈβπ)))) |
412 | | releldm 5904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((Rel
β β§ seq0( + , ((πΈβπ) shift -1)) β ( β βseq1( +
, (πΈβπ)))) β seq0( + , ((πΈβπ) shift -1)) β dom β
) |
413 | 388, 411,
412 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq0( + , ((πΈβπ) shift -1)) β dom β
) |
414 | 254 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β 1 β
β0) |
415 | 351, 356 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (((πΈβπ) shift -1)βπ) β β) |
416 | 112, 414,
415 | iserex 15548 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (seq0( + , ((πΈβπ) shift -1)) β dom β β seq1(
+ , ((πΈβπ) shift -1)) β dom β
)) |
417 | 413, 416 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq1( + , ((πΈβπ) shift -1)) β dom β
) |
418 | 371, 372 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) β
β) |
419 | 309, 418 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πΈβπ)βπ) β β) |
420 | 386, 382 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((π β β β¦ (π Β· ((πΈβπ)βπ)))βπ) = (π Β· ((πΈβπ)βπ))) |
421 | 240, 241,
249, 392, 419, 420 | isermulc2 15549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq1( + , (π β β β¦ (π Β· ((πΈβπ)βπ)))) β (π Β· ( β βseq1( + , (πΈβπ))))) |
422 | | releldm 5904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((Rel
β β§ seq1( + , (π
β β β¦ (π
Β· ((πΈβπ)βπ)))) β (π Β· ( β βseq1( + , (πΈβπ))))) β seq1( + , (π β β β¦ (π Β· ((πΈβπ)βπ)))) β dom β ) |
423 | 388, 421,
422 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β seq1( + , (π β β β¦ (π Β· ((πΈβπ)βπ)))) β dom β ) |
424 | 240, 241,
352, 357, 386, 387, 417, 423 | isumadd 15659 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) = (Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) |
425 | 424 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ + Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) = (πΆ + (Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))))) |
426 | 363, 365 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β (πΆ β π) β β) |
427 | 426, 248 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πΆ β π) Β· (πΆCππ)) β β) |
428 | 427, 371,
252 | adddird 11187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) Β· (πβπ)) = ((((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) |
429 | 428 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) Β· (πβπ)) = Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) |
430 | 429 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ + Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) Β· (πβπ))) = (πΆ + Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))))) |
431 | 307 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β) β Ξ£π β β ((πΈβπ)βπ) = Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) |
432 | 431 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β β) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = ((1 + π) Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))))) |
433 | 119, 432 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β π·) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = ((1 + π) Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))))) |
434 | 433 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = ((1 + π) Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))))) |
435 | 240, 241,
309, 418, 390 | isumcl 15653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) β
β) |
436 | 239, 249,
435 | adddird 11187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π) Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) = ((1 Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) + (π Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))))) |
437 | 435 | mulid2d 11180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) = Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) |
438 | 240, 241,
309, 418, 390, 249 | isummulc2 15654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (π Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) = Ξ£π β β (π Β· (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))))) |
439 | 381 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β (π Β· (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) = Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) |
440 | 438, 439 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (π Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) = Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) |
441 | 437, 440 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) + (π Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))))) = (Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) |
442 | 434, 436,
441 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = (Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) |
443 | 400 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(β€β₯β(0 + 1)) =
(β€β₯β1) |
444 | 240, 443 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ β =
(β€β₯β(0 + 1)) |
445 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = (1 + π) β (π β 1) = ((1 + π) β 1)) |
446 | 445 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = (1 + π) β (πΆ β (π β 1)) = (πΆ β ((1 + π) β 1))) |
447 | 445 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = (1 + π) β (πΆCπ(π β 1)) = (πΆCπ((1 + π) β 1))) |
448 | 446, 447 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = (1 + π) β ((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) = ((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1)))) |
449 | 445 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = (1 + π) β (πβ(π β 1)) = (πβ((1 + π) β 1))) |
450 | 448, 449 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = (1 + π) β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) = (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1)))) |
451 | 112, 444,
450, 241, 113, 418 | isumshft 15731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) = Ξ£π β β0 (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1)))) |
452 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β (1 + π) = (1 + π)) |
453 | 452 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β ((1 + π) β 1) = ((1 + π) β 1)) |
454 | 453 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π β (πΆ β ((1 + π) β 1)) = (πΆ β ((1 + π) β 1))) |
455 | 453 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = π β (πΆCπ((1 + π) β 1)) = (πΆCπ((1 + π) β 1))) |
456 | 454, 455 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = π β ((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) = ((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1)))) |
457 | 453 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = π β (πβ((1 + π) β 1)) = (πβ((1 + π) β 1))) |
458 | 456, 457 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1))) = (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1)))) |
459 | 458 | cbvsumv 15588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
Ξ£π β
β0 (((πΆ
β ((1 + π) β
1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1))) = Ξ£π β β0 (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1))) |
460 | 459 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β0 (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1))) = Ξ£π β β0 (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1)))) |
461 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β 1 β
β) |
462 | 461, 353 | pncan2d 11521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((1 +
π) β 1) = π) |
463 | 462 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πΆ β ((1 + π) β 1)) = (πΆ β π)) |
464 | 462 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πΆCπ((1 + π) β 1)) = (πΆCππ)) |
465 | 463, 464 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) = ((πΆ β π) Β· (πΆCππ))) |
466 | 462 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πβ((1 + π) β 1)) = (πβπ)) |
467 | 465, 466 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1))) = (((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) |
468 | 467 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β0 (((πΆ β ((1 + π) β 1)) Β· (πΆCπ((1 + π) β 1))) Β· (πβ((1 + π) β 1))) = Ξ£π β β0 (((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) |
469 | 451, 460,
468 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) = Ξ£π β β0 (((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) |
470 | 112, 113,
351, 356, 413 | isum1p 15733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β0 (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) = ((((πΈβπ) shift -1)β0) + Ξ£π β
(β€β₯β(0 + 1))(((πΆ β π) Β· (πΆCππ)) Β· (πβπ)))) |
471 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π = 0) β π = 0) |
472 | 471 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π = 0) β (πΆ β π) = (πΆ β 0)) |
473 | 471 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π = 0) β (πΆCππ) = (πΆCπ0)) |
474 | 472, 473 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π = 0) β ((πΆ β π) Β· (πΆCππ)) = ((πΆ β 0) Β· (πΆCπ0))) |
475 | 471 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π = 0) β (πβπ) = (πβ0)) |
476 | 474, 475 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π = 0) β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) = (((πΆ β 0) Β· (πΆCπ0)) Β· (πβ0))) |
477 | | 0nn0 12435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 0 β
β0 |
478 | 477 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β 0 β
β0) |
479 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΆ β 0) Β· (πΆCπ0)) Β· (πβ0)) β
V) |
480 | 349, 476,
478, 479 | fvmptd 6960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΈβπ) shift -1)β0) = (((πΆ β 0) Β· (πΆCπ0)) Β· (πβ0))) |
481 | 236 | subid1d 11508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ β 0) = πΆ) |
482 | 236 | bccn0 42697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆCπ0) =
1) |
483 | 481, 482 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ β 0) Β· (πΆCπ0)) = (πΆ Β· 1)) |
484 | 483, 237 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ β 0) Β· (πΆCπ0)) = πΆ) |
485 | 249 | exp0d 14052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πβ0) = 1) |
486 | 484, 485 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΆ β 0) Β· (πΆCπ0)) Β· (πβ0)) = (πΆ Β· 1)) |
487 | 480, 486,
237 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΈβπ) shift -1)β0) = πΆ) |
488 | 444 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(β€β₯β(0 + 1)) = β |
489 | 488 | sumeq1i 15590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
Ξ£π β
(β€β₯β(0 + 1))(((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) = Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) |
490 | 489 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β (β€β₯β(0 +
1))(((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) = Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) |
491 | 487, 490 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((((πΈβπ) shift -1)β0) + Ξ£π β
(β€β₯β(0 + 1))(((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) = (πΆ + Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)))) |
492 | 469, 470,
491 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) = (πΆ + Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)))) |
493 | 492 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1))) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) = ((πΆ + Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)))) |
494 | 240, 241,
352, 357, 417 | isumcl 15653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) β β) |
495 | 249, 435 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (π Β· Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβ(π β 1)))) β
β) |
496 | 440, 495 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ)) β β) |
497 | 236, 494,
496 | addassd 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ + Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ))) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))) = (πΆ + (Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))))) |
498 | 442, 493,
497 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = (πΆ + (Ξ£π β β (((πΆ β π) Β· (πΆCππ)) Β· (πβπ)) + Ξ£π β β (((πΆ β (π β 1)) Β· (πΆCπ(π β 1))) Β· (πβπ))))) |
499 | 425, 430,
498 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = (πΆ + Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) Β· (πβπ)))) |
500 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β β) β π β β) |
501 | 278, 500 | binomcxplemwb 42702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β β) β (((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) = (πΆ Β· (πΆCππ))) |
502 | 501 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β β) β ((((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) Β· (πβπ)) = ((πΆ Β· (πΆCππ)) Β· (πβπ))) |
503 | 502 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) Β· (πβπ)) = Ξ£π β β ((πΆ Β· (πΆCππ)) Β· (πβπ))) |
504 | 503 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (πΆ + Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) Β· (πβπ))) = (πΆ + Ξ£π β β ((πΆ Β· (πΆCππ)) Β· (πβπ)))) |
505 | 504 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ + Ξ£π β β ((((πΆ β π) Β· (πΆCππ)) + ((πΆ β (π β 1)) Β· (πΆCπ(π β 1)))) Β· (πβπ))) = (πΆ + Ξ£π β β ((πΆ Β· (πΆCππ)) Β· (πβπ)))) |
506 | 363, 248,
252 | mulassd 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πΆ Β· (πΆCππ)) Β· (πβπ)) = (πΆ Β· ((πΆCππ) Β· (πβπ)))) |
507 | 506 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β ((πΆ Β· (πΆCππ)) Β· (πβπ)) = Ξ£π β β (πΆ Β· ((πΆCππ) Β· (πβπ)))) |
508 | 240, 241,
244, 253, 258, 236 | isummulc2 15654 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ Β· Ξ£π β β ((πΆCππ) Β· (πβπ))) = Ξ£π β β (πΆ Β· ((πΆCππ) Β· (πβπ)))) |
509 | 507, 508 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β ((πΆ Β· (πΆCππ)) Β· (πβπ)) = (πΆ Β· Ξ£π β β ((πΆCππ) Β· (πβπ)))) |
510 | 509 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ + Ξ£π β β ((πΆ Β· (πΆCππ)) Β· (πβπ))) = (πΆ + (πΆ Β· Ξ£π β β ((πΆCππ) Β· (πβπ))))) |
511 | 499, 505,
510 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = (πΆ + (πΆ Β· Ξ£π β β ((πΆCππ) Β· (πβπ))))) |
512 | 238, 260,
511 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = (πΆ Β· (1 + Ξ£π β β ((πΆCππ) Β· (πβπ))))) |
513 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ Β¬ πΆ β β0) β π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))) |
514 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β (π β β0
β¦ ((πΉβπ) Β· (πβπ))) β V) |
515 | 513, 514 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β (πβπ) = (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
516 | 119, 515 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πβπ) = (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
517 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((πΉβπ) Β· (πβπ)) β V) |
518 | 516, 517 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((πβπ)βπ) = ((πΉβπ) Β· (πβπ))) |
519 | 518 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β0 ((πβπ)βπ) = Ξ£π β β0 ((πΉβπ) Β· (πβπ))) |
520 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β0) β πΆ β
β) |
521 | 520, 130 | bcccl 42693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π β β0) β (πΆCππ) β
β) |
522 | 132, 521 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π β β0) β (πΉβπ) β β) |
523 | 522 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΉβπ) β
β) |
524 | 523 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β (πΉβπ) β β) |
525 | 524, 251 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β0) β ((πΉβπ) Β· (πβπ)) β β) |
526 | 112, 113,
518, 525, 159 | isum1p 15733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β0 ((πΉβπ) Β· (πβπ)) = (((πβπ)β0) + Ξ£π β (β€β₯β(0 +
1))((πΉβπ) Β· (πβπ)))) |
527 | 471 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π = 0) β (πΉβπ) = (πΉβ0)) |
528 | 527, 475 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π = 0) β ((πΉβπ) Β· (πβπ)) = ((πΉβ0) Β· (πβ0))) |
529 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΉβ0) Β· (πβ0)) β V) |
530 | 516, 528,
478, 529 | fvmptd 6960 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πβπ)β0) = ((πΉβ0) Β· (πβ0))) |
531 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β πΉ = (π β β0 β¦ (πΆCππ))) |
532 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π = 0) β π = 0) |
533 | 532 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π = 0) β (πΆCππ) = (πΆCπ0)) |
534 | 477 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β 0 β
β0) |
535 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (πΆCπ0) β
V) |
536 | 531, 533,
534, 535 | fvmptd 6960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (πΉβ0) = (πΆCπ0)) |
537 | 536 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΉβ0) = (πΆCπ0)) |
538 | 537, 482 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΉβ0) = 1) |
539 | 538, 485 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΉβ0) Β· (πβ0)) = (1 Β· 1)) |
540 | 239 | mulid1d 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 Β· 1) =
1) |
541 | 530, 539,
540 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πβπ)β0) = 1) |
542 | 488 | sumeq1i 15590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
Ξ£π β
(β€β₯β(0 + 1))((πΉβπ) Β· (πβπ)) = Ξ£π β β ((πΉβπ) Β· (πβπ)) |
543 | 133 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β π·) β§ π β β0) β ((πΉβπ) Β· (πβπ)) = ((πΆCππ) Β· (πβπ))) |
544 | 242, 543 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β π·) β§ π β β) β ((πΉβπ) Β· (πβπ)) = ((πΆCππ) Β· (πβπ))) |
545 | 544 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πΉβπ) Β· (πβπ)) = ((πΆCππ) Β· (πβπ))) |
546 | 545 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β ((πΉβπ) Β· (πβπ)) = Ξ£π β β ((πΆCππ) Β· (πβπ))) |
547 | 542, 546 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β (β€β₯β(0 +
1))((πΉβπ) Β· (πβπ)) = Ξ£π β β ((πΆCππ) Β· (πβπ))) |
548 | 541, 547 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πβπ)β0) + Ξ£π β (β€β₯β(0 +
1))((πΉβπ) Β· (πβπ))) = (1 + Ξ£π β β ((πΆCππ) Β· (πβπ)))) |
549 | 519, 526,
548 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 + Ξ£π β β ((πΆCππ) Β· (πβπ))) = Ξ£π β β0 ((πβπ)βπ)) |
550 | 549 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ Β· (1 + Ξ£π β β ((πΆCππ) Β· (πβπ)))) = (πΆ Β· Ξ£π β β0 ((πβπ)βπ))) |
551 | 512, 550 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = (πΆ Β· Ξ£π β β0 ((πβπ)βπ))) |
552 | 236, 160 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ Β· Ξ£π β β0 ((πβπ)βπ)) β β) |
553 | 239, 249 | addcld 11181 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 + π) β β) |
554 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ Β¬ πΆ β β0) β§ π β π·) β§ π β β) β ((πΈβπ)βπ) = ((πΈβπ)βπ)) |
555 | 240, 241,
554, 419, 390 | isumcl 15653 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β ((πΈβπ)βπ) β β) |
556 | 239, 249 | subnegd 11526 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 β -π) = (1 + π)) |
557 | 249 | negcld 11506 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β -π β β) |
558 | | elpreima 7013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (abs Fn
β β (π β
(β‘abs β (0[,)π
)) β (π β β β§ (absβπ) β (0[,)π
)))) |
559 | 86, 87, 558 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (β‘abs β (0[,)π
)) β (π β β β§ (absβπ) β (0[,)π
))) |
560 | 559 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (β‘abs β (0[,)π
)) β (absβπ) β (0[,)π
)) |
561 | 560, 2 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π· β (absβπ) β (0[,)π
)) |
562 | | elico2 13335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((0
β β β§ π
β β*) β ((absβπ) β (0[,)π
) β ((absβπ) β β β§ 0 β€
(absβπ) β§
(absβπ) < π
))) |
563 | 75, 81, 562 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((absβπ)
β (0[,)π
) β
((absβπ) β
β β§ 0 β€ (absβπ) β§ (absβπ) < π
)) |
564 | 563 | simp3bi 1148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((absβπ)
β (0[,)π
) β
(absβπ) < π
) |
565 | 561, 564 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π· β (absβπ) < π
) |
566 | 565 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (absβπ) < π
) |
567 | 249 | absnegd 15341 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (absβ-π) = (absβπ)) |
568 | 567 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (absβπ) = (absβ-π)) |
569 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β π
= 1) |
570 | 566, 568,
569 | 3brtr3d 5141 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (absβ-π) < 1) |
571 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 1 β
β |
572 | | abssubne0 15208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((-π β β β§ 1 β
β β§ (absβ-π) < 1) β (1 β -π) β 0) |
573 | 571, 572 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((-π β β β§
(absβ-π) < 1)
β (1 β -π) β
0) |
574 | 557, 570,
573 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 β -π) β 0) |
575 | 556, 574 | eqnetrrd 3013 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 + π) β 0) |
576 | 552, 553,
555, 575 | divmuld 11960 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΆ Β· Ξ£π β β0 ((πβπ)βπ)) / (1 + π)) = Ξ£π β β ((πΈβπ)βπ) β ((1 + π) Β· Ξ£π β β ((πΈβπ)βπ)) = (πΆ Β· Ξ£π β β0 ((πβπ)βπ)))) |
577 | 551, 576 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ Β· Ξ£π β β0 ((πβπ)βπ)) / (1 + π)) = Ξ£π β β ((πΈβπ)βπ)) |
578 | 236, 160,
553, 575 | div23d 11975 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ Β· Ξ£π β β0 ((πβπ)βπ)) / (1 + π)) = ((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ))) |
579 | 577, 578 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β ((πΈβπ)βπ) = ((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ))) |
580 | 579 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ Ξ£π β β ((πΈβπ)βπ)) = (π β π· β¦ ((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)))) |
581 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ / (1 + π)) β V) |
582 | | sumex 15579 |
. . . . . . . . . . . . . . . . . . . 20
β’
Ξ£π β
β0 ((πβπ)βπ) β V |
583 | 582 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β Ξ£π β β0 ((πβπ)βπ) β V) |
584 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ (πΆ / (1 + π))) = (π β π· β¦ (πΆ / (1 + π)))) |
585 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ πΆ β β0) β π = (π β π· β¦ Ξ£π β β0 ((πβπ)βπ))) |
586 | 103, 23, 183, 581, 583, 584, 585 | offval2f 7637 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ πΆ β β0) β ((π β π· β¦ (πΆ / (1 + π))) βf Β· π) = (π β π· β¦ ((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)))) |
587 | 580, 205,
586 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β (β
D π) = ((π β π· β¦ (πΆ / (1 + π))) βf Β· π)) |
588 | 587 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β
((β D π)
βf Β· (π β π· β¦ ((1 + π)βπ-πΆ))) = (((π β π· β¦ (πΆ / (1 + π))) βf Β· π) βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ)))) |
589 | 223 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β
((β D (π β π· β¦ ((1 + π)βπ-πΆ))) βf Β· π) = ((π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))
βf Β· π)) |
590 | 588, 589 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β
(((β D π)
βf Β· (π β π· β¦ ((1 + π)βπ-πΆ))) βf + ((β D (π β π· β¦ ((1 + π)βπ-πΆ))) βf Β· π)) = ((((π β π· β¦ (πΆ / (1 + π))) βf Β· π) βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ))) βf + ((π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))
βf Β· π))) |
591 | | ovexd 7397 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)) β V) |
592 | | ovexd 7397 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)) β V) |
593 | | ovexd 7397 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) β V) |
594 | | ovexd 7397 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π)βπ-πΆ) β V) |
595 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ ((1 + π)βπ-πΆ)) = (π β π· β¦ ((1 + π)βπ-πΆ))) |
596 | 103, 23, 183, 593, 594, 586, 595 | offval2f 7637 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β (((π β π· β¦ (πΆ / (1 + π))) βf Β· π) βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ))) = (π β π· β¦ (((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)))) |
597 | | ovexd 7397 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (-πΆ Β· ((1 + π)βπ(-πΆ β 1))) β
V) |
598 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1)))) = (π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))) |
599 | 103, 23, 183, 597, 583, 598, 585 | offval2f 7637 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β ((π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))
βf Β· π) = (π β π· β¦ ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)))) |
600 | 103, 23, 183, 591, 592, 596, 599 | offval2f 7637 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β
((((π β π· β¦ (πΆ / (1 + π))) βf Β· π) βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ))) βf + ((π β π· β¦ (-πΆ Β· ((1 + π)βπ(-πΆ β 1))))
βf Β· π)) = (π β π· β¦ ((((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)) + ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))))) |
601 | 235, 590,
600 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π βf
Β· (π β π· β¦ ((1 + π)βπ-πΆ)))) = (π β π· β¦ ((((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)) + ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))))) |
602 | 236, 553,
575 | divcld 11938 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ / (1 + π)) β β) |
603 | 236 | negcld 11506 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β -πΆ β β) |
604 | 553, 603 | cxpcld 26079 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π)βπ-πΆ) β β) |
605 | 602, 160,
604 | mul32d 11372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)) = (((πΆ / (1 + π)) Β· ((1 + π)βπ-πΆ)) Β· Ξ£π β β0 ((πβπ)βπ))) |
606 | 236, 553,
604, 575 | div32d 11961 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ / (1 + π)) Β· ((1 + π)βπ-πΆ)) = (πΆ Β· (((1 + π)βπ-πΆ) / (1 + π)))) |
607 | 553, 575,
603, 239 | cxpsubd 26089 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π)βπ(-πΆ β 1)) = (((1 + π)βπ-πΆ) / ((1 + π)βπ1))) |
608 | 553 | cxp1d 26077 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π)βπ1) = (1 + π)) |
609 | 608 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((1 + π)βπ-πΆ) / ((1 + π)βπ1)) = (((1 + π)βπ-πΆ) / (1 + π))) |
610 | 607, 609 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((1 + π)βπ-πΆ) / (1 + π)) = ((1 + π)βπ(-πΆ β 1))) |
611 | 610 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ Β· (((1 + π)βπ-πΆ) / (1 + π))) = (πΆ Β· ((1 + π)βπ(-πΆ β 1)))) |
612 | 606, 611 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ / (1 + π)) Β· ((1 + π)βπ-πΆ)) = (πΆ Β· ((1 + π)βπ(-πΆ β 1)))) |
613 | 612 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΆ / (1 + π)) Β· ((1 + π)βπ-πΆ)) Β· Ξ£π β β0 ((πβπ)βπ)) = ((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))) |
614 | 605, 613 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)) = ((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))) |
615 | 603, 239 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (-πΆ β 1) β β) |
616 | 553, 615 | cxpcld 26079 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π)βπ(-πΆ β 1)) β
β) |
617 | 236, 616 | mulneg1d 11615 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (-πΆ Β· ((1 + π)βπ(-πΆ β 1))) = -(πΆ Β· ((1 + π)βπ(-πΆ β 1)))) |
618 | 617 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)) = (-(πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))) |
619 | 236, 616 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (πΆ Β· ((1 + π)βπ(-πΆ β 1))) β
β) |
620 | 619, 160 | mulneg1d 11615 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (-(πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)) = -((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))) |
621 | 618, 620 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)) = -((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))) |
622 | 614, 621 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)) + ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))) = (((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)) + -((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)))) |
623 | 619, 160 | mulcld 11182 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)) β β) |
624 | 623 | negidd 11509 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)) + -((πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))) = 0) |
625 | 622, 624 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)) + ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ))) = 0) |
626 | 625 | mpteq2dva 5210 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ ((((πΆ / (1 + π)) Β· Ξ£π β β0 ((πβπ)βπ)) Β· ((1 + π)βπ-πΆ)) + ((-πΆ Β· ((1 + π)βπ(-πΆ β 1))) Β·
Ξ£π β
β0 ((πβπ)βπ)))) = (π β π· β¦ 0)) |
627 | 601, 626 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π βf
Β· (π β π· β¦ ((1 + π)βπ-πΆ)))) = (π β π· β¦ 0)) |
628 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π₯0 |
629 | | eqidd 2738 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β 0 = 0) |
630 | 24, 23, 4, 628, 629 | cbvmptf 5219 |
. . . . . . . . . . . . 13
β’ (π₯ β π· β¦ 0) = (π β π· β¦ 0) |
631 | 627, 630 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π βf
Β· (π β π· β¦ ((1 + π)βπ-πΆ)))) = (π₯ β π· β¦ 0)) |
632 | | c0ex 11156 |
. . . . . . . . . . . . . 14
β’ 0 β
V |
633 | 632 | snid 4627 |
. . . . . . . . . . . . 13
β’ 0 β
{0} |
634 | 633 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β 0 β {0}) |
635 | 631, 634 | fmpt3d 7069 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π βf
Β· (π β π· β¦ ((1 + π)βπ-πΆ)))):π·βΆ{0}) |
636 | 635 | fdmd 6684 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β dom
(β D (π
βf Β· (π β π· β¦ ((1 + π)βπ-πΆ)))) = π·) |
637 | | 1cnd 11157 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β β) β 1 β
β) |
638 | | 0cnd 11155 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β β) β 0 β
β) |
639 | | dvconst 25297 |
. . . . . . . . . . . . . . . 16
β’ (1 β
β β (β D (β Γ {1})) = (β Γ
{0})) |
640 | 196, 639 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (β
D (β Γ {1})) = (β Γ {0}) |
641 | | fconstmpt 5699 |
. . . . . . . . . . . . . . . 16
β’ (β
Γ {1}) = (π₯ β
β β¦ 1) |
642 | 641 | oveq2i 7373 |
. . . . . . . . . . . . . . 15
β’ (β
D (β Γ {1})) = (β D (π₯ β β β¦ 1)) |
643 | | fconstmpt 5699 |
. . . . . . . . . . . . . . 15
β’ (β
Γ {0}) = (π₯ β
β β¦ 0) |
644 | 640, 642,
643 | 3eqtr3i 2773 |
. . . . . . . . . . . . . 14
β’ (β
D (π₯ β β β¦
1)) = (π₯ β β
β¦ 0) |
645 | 644 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π₯ β β β¦
1)) = (π₯ β β
β¦ 0)) |
646 | 118 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΆ β β0) β π· β
β) |
647 | | fvex 6860 |
. . . . . . . . . . . . . . 15
β’
(TopOpenββfld) β V |
648 | | cnfldtps 24157 |
. . . . . . . . . . . . . . . . 17
β’
βfld β TopSp |
649 | | cnfldbas 20816 |
. . . . . . . . . . . . . . . . . 18
β’ β =
(Baseββfld) |
650 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(TopOpenββfld) =
(TopOpenββfld) |
651 | 649, 650 | tpsuni 22301 |
. . . . . . . . . . . . . . . . 17
β’
(βfld β TopSp β β = βͺ (TopOpenββfld)) |
652 | 648, 651 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ β =
βͺ
(TopOpenββfld) |
653 | 652 | restid 17322 |
. . . . . . . . . . . . . . 15
β’
((TopOpenββfld) β V β
((TopOpenββfld) βΎt β) =
(TopOpenββfld)) |
654 | 647, 653 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
((TopOpenββfld) βΎt β) =
(TopOpenββfld) |
655 | 654 | eqcomi 2746 |
. . . . . . . . . . . . 13
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
656 | 650 | cnfldtop 24163 |
. . . . . . . . . . . . . . 15
β’
(TopOpenββfld) β Top |
657 | | cnxmet 24152 |
. . . . . . . . . . . . . . . . 17
β’ (abs
β β ) β (βMetββ) |
658 | 650 | cnfldtopn 24161 |
. . . . . . . . . . . . . . . . . 18
β’
(TopOpenββfld) = (MetOpenβ(abs β
β )) |
659 | 658 | blopn 23872 |
. . . . . . . . . . . . . . . . 17
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ π
β
β*) β (0(ballβ(abs β β ))π
) β
(TopOpenββfld)) |
660 | 657, 398,
81, 659 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
β’
(0(ballβ(abs β β ))π
) β
(TopOpenββfld) |
661 | 98, 660 | eqeltri 2834 |
. . . . . . . . . . . . . . 15
β’ π· β
(TopOpenββfld) |
662 | | isopn3i 22449 |
. . . . . . . . . . . . . . 15
β’
(((TopOpenββfld) β Top β§ π· β
(TopOpenββfld)) β
((intβ(TopOpenββfld))βπ·) = π·) |
663 | 656, 661,
662 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
((intβ(TopOpenββfld))βπ·) = π· |
664 | 663 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΆ β β0) β
((intβ(TopOpenββfld))βπ·) = π·) |
665 | 203, 637,
638, 645, 646, 655, 650, 664 | dvmptres2 25342 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π₯ β π· β¦ 1)) = (π₯ β π· β¦ 0)) |
666 | 192 | oveq2i 7373 |
. . . . . . . . . . . 12
β’ (β
D (π₯ β π· β¦ 1)) = (β D (π β π· β¦ 1)) |
667 | 665, 666,
630 | 3eqtr3g 2800 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π β π· β¦ 1)) = (π β π· β¦ 0)) |
668 | 626, 601,
667 | 3eqtr4d 2787 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β (β
D (π βf
Β· (π β π· β¦ ((1 + π)βπ-πΆ)))) = (β D (π β π· β¦ 1))) |
669 | | 1rp 12926 |
. . . . . . . . . . . . 13
β’ 1 β
β+ |
670 | 73, 669 | eqeltrdi 2846 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ πΆ β β0) β π
β
β+) |
671 | | blcntr 23782 |
. . . . . . . . . . . . 13
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ π
β
β+) β 0 β (0(ballβ(abs β β ))π
)) |
672 | 657, 398,
671 | mp3an12 1452 |
. . . . . . . . . . . 12
β’ (π
β β+
β 0 β (0(ballβ(abs β β ))π
)) |
673 | 670, 672 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β 0 β
(0(ballβ(abs β β ))π
)) |
674 | 673, 98 | eleqtrrdi 2849 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β 0 β
π·) |
675 | | 0zd 12518 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β 0 β
β€) |
676 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πβ0)βπ) = ((πβ0)βπ)) |
677 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²ππ |
678 | 23 | nfel2 2926 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π0 β
π· |
679 | 677, 678 | nfan 1903 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(π β§ 0 β π·) |
680 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π π β
β0 |
681 | 679, 680 | nfan 1903 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π β§ 0 β π·) β§ π β β0) |
682 | 10, 4 | nffv 6857 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(πβ0) |
683 | 682, 29 | nffv 6857 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π((πβ0)βπ) |
684 | 683 | nfel1 2924 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((πβ0)βπ) β
β |
685 | 681, 684 | nfim 1900 |
. . . . . . . . . . . . . . . . 17
β’
β²π(((π β§ 0 β π·) β§ π β β0) β ((πβ0)βπ) β
β) |
686 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β (π β π· β 0 β π·)) |
687 | 686 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β ((π β§ π β π·) β (π β§ 0 β π·))) |
688 | 687 | anbi1d 631 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (((π β§ π β π·) β§ π β β0) β ((π β§ 0 β π·) β§ π β
β0))) |
689 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β (πβπ) = (πβ0)) |
690 | 689 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β ((πβπ)βπ) = ((πβ0)βπ)) |
691 | 690 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (((πβπ)βπ) β β β ((πβ0)βπ) β β)) |
692 | 688, 691 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β ((((π β§ π β π·) β§ π β β0) β ((πβπ)βπ) β β) β (((π β§ 0 β π·) β§ π β β0) β ((πβ0)βπ) β
β))) |
693 | 685, 632,
692, 143 | vtoclf 3519 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ 0 β π·) β§ π β β0) β ((πβ0)βπ) β
β) |
694 | 674, 693 | syldanl 603 |
. . . . . . . . . . . . . . 15
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πβ0)βπ) β β) |
695 | 4, 7, 682 | nfseq 13923 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πseq0(
+ , (πβ0)) |
696 | 695 | nfel1 2924 |
. . . . . . . . . . . . . . . . . 18
β’
β²πseq0( + ,
(πβ0)) β dom
β |
697 | 679, 696 | nfim 1900 |
. . . . . . . . . . . . . . . . 17
β’
β²π((π β§ 0 β π·) β seq0( + , (πβ0)) β dom β
) |
698 | 689 | seqeq3d 13921 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β seq0( + , (πβπ)) = seq0( + , (πβ0))) |
699 | 698 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (seq0( + , (πβπ)) β dom β β seq0( + , (πβ0)) β dom β
)) |
700 | 687, 699 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (((π β§ π β π·) β seq0( + , (πβπ)) β dom β ) β ((π β§ 0 β π·) β seq0( + , (πβ0)) β dom β
))) |
701 | 697, 632,
700, 158 | vtoclf 3519 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ 0 β π·) β seq0( + , (πβ0)) β dom β
) |
702 | 674, 701 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β seq0( +
, (πβ0)) β dom
β ) |
703 | 112, 675,
676, 694, 702 | isum1p 15733 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΆ β β0) β
Ξ£π β
β0 ((πβ0)βπ) = (((πβ0)β0) + Ξ£π β
(β€β₯β(0 + 1))((πβ0)βπ))) |
704 | 132 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΉβπ) = (πΆCππ)) |
705 | 704 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ πΆ β β0) β§ π = 0) β§ π β β0) β (πΉβπ) = (πΆCππ)) |
706 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ Β¬ πΆ β β0) β§ π = 0) β§ π β β0) β π = 0) |
707 | 706 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ Β¬ πΆ β β0) β§ π = 0) β§ π β β0) β (πβπ) = (0βπ)) |
708 | 705, 707 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ Β¬ πΆ β β0) β§ π = 0) β§ π β β0) β ((πΉβπ) Β· (πβπ)) = ((πΆCππ) Β· (0βπ))) |
709 | 708 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π = 0) β (π β β0 β¦ ((πΉβπ) Β· (πβπ))) = (π β β0 β¦ ((πΆCππ) Β· (0βπ)))) |
710 | 121 | mptex 7178 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β¦ ((πΆCππ) Β· (0βπ))) β V |
711 | 710 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ πΆ β β0) β (π β β0
β¦ ((πΆCππ) Β· (0βπ))) β V) |
712 | 513, 709,
99, 711 | fvmptd 6960 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β (πβ0) = (π β β0 β¦ ((πΆCππ) Β· (0βπ)))) |
713 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π = 0) β π = 0) |
714 | 713 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π = 0) β (πΆCππ) = (πΆCπ0)) |
715 | 713 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π = 0) β (0βπ) = (0β0)) |
716 | 714, 715 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ Β¬ πΆ β β0) β§ π = 0) β ((πΆCππ) Β· (0βπ)) = ((πΆCπ0) Β·
(0β0))) |
717 | 477 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β 0 β
β0) |
718 | | ovexd 7397 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β ((πΆCπ0) Β·
(0β0)) β V) |
719 | 712, 716,
717, 718 | fvmptd 6960 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β ((πβ0)β0) = ((πΆCπ0) Β·
(0β0))) |
720 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ πΆ β β0) β πΆ β
β) |
721 | 720 | bccn0 42697 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β (πΆCπ0) =
1) |
722 | 99 | exp0d 14052 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΆ β β0) β
(0β0) = 1) |
723 | 721, 722 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β ((πΆCπ0) Β·
(0β0)) = (1 Β· 1)) |
724 | | 1t1e1 12322 |
. . . . . . . . . . . . . . . . 17
β’ (1
Β· 1) = 1 |
725 | 724 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β (1
Β· 1) = 1) |
726 | 719, 723,
725 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β ((πβ0)β0) =
1) |
727 | | ovexd 7397 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πΆCππ) Β· (0βπ)) β V) |
728 | 712, 727 | fvmpt2d 6966 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πβ0)βπ) = ((πΆCππ) Β· (0βπ))) |
729 | 242, 728 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β ((πβ0)βπ) = ((πΆCππ) Β· (0βπ))) |
730 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β π β
β) |
731 | 730 | 0expd 14051 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β
(0βπ) =
0) |
732 | 731 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β ((πΆCππ) Β· (0βπ)) = ((πΆCππ) Β· 0)) |
733 | 521 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΆCππ) β β) |
734 | 242, 733 | sylan2 594 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β (πΆCππ) β
β) |
735 | 734 | mul01d 11361 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β ((πΆCππ) Β· 0) =
0) |
736 | 729, 732,
735 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ Β¬ πΆ β β0) β§ π β β) β ((πβ0)βπ) = 0) |
737 | 736 | sumeq2dv 15595 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΆ β β0) β
Ξ£π β β
((πβ0)βπ) = Ξ£π β β 0) |
738 | 444 | sumeq1i 15590 |
. . . . . . . . . . . . . . . 16
β’
Ξ£π β
β ((πβ0)βπ) = Ξ£π β (β€β₯β(0 +
1))((πβ0)βπ) |
739 | 240 | eqimssi 4007 |
. . . . . . . . . . . . . . . . . 18
β’ β
β (β€β₯β1) |
740 | 739 | orci 864 |
. . . . . . . . . . . . . . . . 17
β’ (β
β (β€β₯β1) β¨ β β
Fin) |
741 | | sumz 15614 |
. . . . . . . . . . . . . . . . 17
β’ ((β
β (β€β₯β1) β¨ β β Fin) β
Ξ£π β β 0 =
0) |
742 | 740, 741 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
Ξ£π β
β 0 = 0 |
743 | 737, 738,
742 | 3eqtr3g 2800 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β
Ξ£π β
(β€β₯β(0 + 1))((πβ0)βπ) = 0) |
744 | 726, 743 | oveq12d 7380 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΆ β β0) β (((πβ0)β0) +
Ξ£π β
(β€β₯β(0 + 1))((πβ0)βπ)) = (1 + 0)) |
745 | 703, 744 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΆ β β0) β
Ξ£π β
β0 ((πβ0)βπ) = (1 + 0)) |
746 | | 1p0e1 12284 |
. . . . . . . . . . . . . . 15
β’ (1 + 0) =
1 |
747 | 746 | oveq1i 7372 |
. . . . . . . . . . . . . 14
β’ ((1 +
0)βπ-πΆ) = (1βπ-πΆ) |
748 | 720 | negcld 11506 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΆ β β0) β -πΆ β
β) |
749 | 748 | 1cxpd 26078 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΆ β β0) β
(1βπ-πΆ) = 1) |
750 | 747, 749 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΆ β β0) β ((1 +
0)βπ-πΆ) = 1) |
751 | 745, 750 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ πΆ β β0) β
(Ξ£π β
β0 ((πβ0)βπ) Β· ((1 +
0)βπ-πΆ)) = ((1 + 0) Β· 1)) |
752 | 746 | oveq1i 7372 |
. . . . . . . . . . . . 13
β’ ((1 + 0)
Β· 1) = (1 Β· 1) |
753 | 752, 724 | eqtri 2765 |
. . . . . . . . . . . 12
β’ ((1 + 0)
Β· 1) = 1 |
754 | 751, 753 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β
(Ξ£π β
β0 ((πβ0)βπ) Β· ((1 +
0)βπ-πΆ)) = 1) |
755 | 162 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΆ β β0) β π Fn π·) |
756 | 175 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ ((1 + π)βπ-πΆ)) Fn π·) |
757 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β π = (π₯ β π· β¦ Ξ£π β β0 ((πβπ₯)βπ))) |
758 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ Β¬
πΆ β
β0) β§ 0 β π·) β§ π₯ = 0) β§ π β β0) β π₯ = 0) |
759 | 758 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ Β¬
πΆ β
β0) β§ 0 β π·) β§ π₯ = 0) β§ π β β0) β (πβπ₯) = (πβ0)) |
760 | 759 | fveq1d 6849 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ Β¬
πΆ β
β0) β§ 0 β π·) β§ π₯ = 0) β§ π β β0) β ((πβπ₯)βπ) = ((πβ0)βπ)) |
761 | 760 | sumeq2dv 15595 |
. . . . . . . . . . . . . 14
β’ ((((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β§ π₯ = 0) β Ξ£π β β0 ((πβπ₯)βπ) = Ξ£π β β0 ((πβ0)βπ)) |
762 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β 0 β π·) |
763 | | sumex 15579 |
. . . . . . . . . . . . . . 15
β’
Ξ£π β
β0 ((πβ0)βπ) β V |
764 | 763 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β Ξ£π β β0
((πβ0)βπ) β V) |
765 | 757, 761,
762, 764 | fvmptd 6960 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β (πβ0) = Ξ£π β β0
((πβ0)βπ)) |
766 | 174 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β (π β π· β¦ ((1 + π)βπ-πΆ)) = (π₯ β π· β¦ ((1 + π₯)βπ-πΆ))) |
767 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β§ π₯ = 0) β π₯ = 0) |
768 | 767 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β§ π₯ = 0) β (1 + π₯) = (1 + 0)) |
769 | 768 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ ((((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β§ π₯ = 0) β ((1 + π₯)βπ-πΆ) = ((1 + 0)βπ-πΆ)) |
770 | | ovexd 7397 |
. . . . . . . . . . . . . 14
β’ (((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β ((1 +
0)βπ-πΆ) β V) |
771 | 766, 769,
762, 770 | fvmptd 6960 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β ((π β π· β¦ ((1 + π)βπ-πΆ))β0) = ((1 +
0)βπ-πΆ)) |
772 | 755, 756,
183, 183, 184, 765, 771 | ofval 7633 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ πΆ β β0) β§ 0 β
π·) β ((π βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ)))β0) = (Ξ£π β β0 ((πβ0)βπ) Β· ((1 +
0)βπ-πΆ))) |
773 | 674, 772 | mpdan 686 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β ((π βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ)))β0) = (Ξ£π β β0 ((πβ0)βπ) Β· ((1 +
0)βπ-πΆ))) |
774 | 193 | fveq1i 6848 |
. . . . . . . . . . . 12
β’ ((π· Γ {1})β0) = ((π β π· β¦ 1)β0) |
775 | 186 | fvconst2 7158 |
. . . . . . . . . . . . 13
β’ (0 β
π· β ((π· Γ {1})β0) =
1) |
776 | 674, 775 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ πΆ β β0) β ((π· Γ {1})β0) =
1) |
777 | 774, 776 | eqtr3id 2791 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΆ β β0) β ((π β π· β¦ 1)β0) = 1) |
778 | 754, 773,
777 | 3eqtr4d 2787 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΆ β β0) β ((π βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ)))β0) = ((π β π· β¦ 1)β0)) |
779 | 98, 99, 100, 185, 201, 636, 668, 674, 778 | dv11cn 25381 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΆ β β0) β (π βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ))) = (π β π· β¦ 1)) |
780 | 779 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β ((π βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ))) βf / (π β π· β¦ ((1 + π)βπ-πΆ))) = ((π β π· β¦ 1) βf / (π β π· β¦ ((1 + π)βπ-πΆ)))) |
781 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π(1 + π₯) β 0 |
782 | 105, 781 | nfim 1900 |
. . . . . . . . . . . . 13
β’
β²π(((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β (1 + π₯) β 0) |
783 | 172 | neeq1d 3004 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β ((1 + π) β 0 β (1 + π₯) β 0)) |
784 | 109, 783 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = π₯ β ((((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 + π) β 0) β (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β (1 + π₯) β 0))) |
785 | 782, 784,
575 | chvarfv 2234 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β (1 + π₯) β 0) |
786 | 166, 785,
168 | cxpne0d 26084 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β ((1 + π₯)βπ-πΆ) β 0) |
787 | | eldifsn 4752 |
. . . . . . . . . . 11
β’ (((1 +
π₯)βπ-πΆ) β (β β {0}) β (((1 +
π₯)βπ-πΆ) β β β§ ((1 + π₯)βπ-πΆ) β 0)) |
788 | 169, 786,
787 | sylanbrc 584 |
. . . . . . . . . 10
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ β π·) β ((1 + π₯)βπ-πΆ) β (β β
{0})) |
789 | 788, 174 | fmptd 7067 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ ((1 + π)βπ-πΆ)):π·βΆ(β β
{0})) |
790 | | ofdivcan4 42681 |
. . . . . . . . 9
β’ ((π· β V β§ π:π·βΆβ β§ (π β π· β¦ ((1 + π)βπ-πΆ)):π·βΆ(β β {0})) β
((π βf
Β· (π β π· β¦ ((1 + π)βπ-πΆ))) βf / (π β π· β¦ ((1 + π)βπ-πΆ))) = π) |
791 | 183, 162,
789, 790 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β ((π βf Β·
(π β π· β¦ ((1 + π)βπ-πΆ))) βf / (π β π· β¦ ((1 + π)βπ-πΆ))) = π) |
792 | | eqidd 2738 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ 1) = (π β π· β¦ 1)) |
793 | 103, 23, 183, 239, 604, 792, 595 | offval2f 7637 |
. . . . . . . 8
β’ ((π β§ Β¬ πΆ β β0) β ((π β π· β¦ 1) βf / (π β π· β¦ ((1 + π)βπ-πΆ))) = (π β π· β¦ (1 / ((1 + π)βπ-πΆ)))) |
794 | 780, 791,
793 | 3eqtr3d 2785 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β π = (π β π· β¦ (1 / ((1 + π)βπ-πΆ)))) |
795 | 553, 575,
603 | cxpnegd 26086 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π)βπ--πΆ) = (1 / ((1 + π)βπ-πΆ))) |
796 | 236 | negnegd 11510 |
. . . . . . . . . 10
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β --πΆ = πΆ) |
797 | 796 | oveq2d 7378 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β ((1 + π)βπ--πΆ) = ((1 + π)βππΆ)) |
798 | 795, 797 | eqtr3d 2779 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π β π·) β (1 / ((1 + π)βπ-πΆ)) = ((1 + π)βππΆ)) |
799 | 798 | mpteq2dva 5210 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β (π β π· β¦ (1 / ((1 + π)βπ-πΆ))) = (π β π· β¦ ((1 + π)βππΆ))) |
800 | 794, 799 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β π = (π β π· β¦ ((1 + π)βππΆ))) |
801 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯((1 +
π)βππΆ) |
802 | | nfcv 2908 |
. . . . . . 7
β’
β²π((1 +
π₯)βππΆ) |
803 | 172 | oveq1d 7377 |
. . . . . . 7
β’ (π = π₯ β ((1 + π)βππΆ) = ((1 + π₯)βππΆ)) |
804 | 23, 24, 801, 802, 803 | cbvmptf 5219 |
. . . . . 6
β’ (π β π· β¦ ((1 + π)βππΆ)) = (π₯ β π· β¦ ((1 + π₯)βππΆ)) |
805 | 800, 804 | eqtrdi 2793 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β π = (π₯ β π· β¦ ((1 + π₯)βππΆ))) |
806 | | simpr 486 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ = (π΅ / π΄)) β π₯ = (π΅ / π΄)) |
807 | 806 | oveq2d 7378 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ = (π΅ / π΄)) β (1 + π₯) = (1 + (π΅ / π΄))) |
808 | 807 | oveq1d 7377 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π₯ = (π΅ / π΄)) β ((1 + π₯)βππΆ) = ((1 + (π΅ / π΄))βππΆ)) |
809 | | 1cnd 11157 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β 1 β
β) |
810 | 809, 60 | addcld 11181 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β (1 +
(π΅ / π΄)) β β) |
811 | 810, 720 | cxpcld 26079 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β ((1 +
(π΅ / π΄))βππΆ) β
β) |
812 | 805, 808,
91, 811 | fvmptd 6960 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β (πβ(π΅ / π΄)) = ((1 + (π΅ / π΄))βππΆ)) |
813 | 704 | adantlr 714 |
. . . . . . . . 9
β’ ((((π β§ Β¬ πΆ β β0) β§ π = (π΅ / π΄)) β§ π β β0) β (πΉβπ) = (πΆCππ)) |
814 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ Β¬ πΆ β β0) β§ π = (π΅ / π΄)) β§ π β β0) β π = (π΅ / π΄)) |
815 | 814 | oveq1d 7377 |
. . . . . . . . 9
β’ ((((π β§ Β¬ πΆ β β0) β§ π = (π΅ / π΄)) β§ π β β0) β (πβπ) = ((π΅ / π΄)βπ)) |
816 | 813, 815 | oveq12d 7380 |
. . . . . . . 8
β’ ((((π β§ Β¬ πΆ β β0) β§ π = (π΅ / π΄)) β§ π β β0) β ((πΉβπ) Β· (πβπ)) = ((πΆCππ) Β· ((π΅ / π΄)βπ))) |
817 | 816 | mpteq2dva 5210 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π = (π΅ / π΄)) β (π β β0 β¦ ((πΉβπ) Β· (πβπ))) = (π β β0 β¦ ((πΆCππ) Β· ((π΅ / π΄)βπ)))) |
818 | 121 | mptex 7178 |
. . . . . . . 8
β’ (π β β0
β¦ ((πΆCππ) Β· ((π΅ / π΄)βπ))) β V |
819 | 818 | a1i 11 |
. . . . . . 7
β’ ((π β§ Β¬ πΆ β β0) β (π β β0
β¦ ((πΆCππ) Β· ((π΅ / π΄)βπ))) β V) |
820 | 513, 817,
60, 819 | fvmptd 6960 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β (πβ(π΅ / π΄)) = (π β β0 β¦ ((πΆCππ) Β· ((π΅ / π΄)βπ)))) |
821 | | ovexd 7397 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πΆCππ) Β· ((π΅ / π΄)βπ)) β V) |
822 | 820, 821 | fvmpt2d 6966 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πβ(π΅ / π΄))βπ) = ((πΆCππ) Β· ((π΅ / π΄)βπ))) |
823 | 822 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β
Ξ£π β
β0 ((πβ(π΅ / π΄))βπ) = Ξ£π β β0 ((πΆCππ) Β· ((π΅ / π΄)βπ))) |
824 | 94, 812, 823 | 3eqtr3d 2785 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β ((1 +
(π΅ / π΄))βππΆ) = Ξ£π β β0 ((πΆCππ) Β· ((π΅ / π΄)βπ))) |
825 | 824 | oveq1d 7377 |
. 2
β’ ((π β§ Β¬ πΆ β β0) β (((1 +
(π΅ / π΄))βππΆ) Β· (π΄βππΆ)) = (Ξ£π β β0 ((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ))) |
826 | 43, 46 | rerpdivcld 12995 |
. . . . . 6
β’ (π β (π΅ / π΄) β β) |
827 | 826 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β (π΅ / π΄) β β) |
828 | 66, 827 | readdcld 11191 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β (1 +
(π΅ / π΄)) β β) |
829 | | df-neg 11395 |
. . . . . . 7
β’ -(π΅ / π΄) = (0 β (π΅ / π΄)) |
830 | 826 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π β (π΅ / π΄) β β) |
831 | 830 | negcld 11506 |
. . . . . . . . . . 11
β’ (π β -(π΅ / π΄) β β) |
832 | 831 | abscld 15328 |
. . . . . . . . . 10
β’ (π β (absβ-(π΅ / π΄)) β β) |
833 | | 1red 11163 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
834 | 830 | absnegd 15341 |
. . . . . . . . . . . 12
β’ (π β (absβ-(π΅ / π΄)) = (absβ(π΅ / π΄))) |
835 | 46 | rpne0d 12969 |
. . . . . . . . . . . . 13
β’ (π β π΄ β 0) |
836 | 44, 47, 835 | absdivd 15347 |
. . . . . . . . . . . 12
β’ (π β (absβ(π΅ / π΄)) = ((absβπ΅) / (absβπ΄))) |
837 | 834, 836 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β (absβ-(π΅ / π΄)) = ((absβπ΅) / (absβπ΄))) |
838 | 44 | abscld 15328 |
. . . . . . . . . . . 12
β’ (π β (absβπ΅) β
β) |
839 | 669 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 1 β
β+) |
840 | 47, 835 | absrpcld 15340 |
. . . . . . . . . . . 12
β’ (π β (absβπ΄) β
β+) |
841 | 838 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (π β (absβπ΅) β
β) |
842 | 841 | div1d 11930 |
. . . . . . . . . . . . 13
β’ (π β ((absβπ΅) / 1) = (absβπ΅)) |
843 | 842, 53 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (π β ((absβπ΅) / 1) < (absβπ΄)) |
844 | 838, 839,
840, 843 | ltdiv23d 13031 |
. . . . . . . . . . 11
β’ (π β ((absβπ΅) / (absβπ΄)) < 1) |
845 | 837, 844 | eqbrtrd 5132 |
. . . . . . . . . 10
β’ (π β (absβ-(π΅ / π΄)) < 1) |
846 | 832, 833,
845 | ltled 11310 |
. . . . . . . . 9
β’ (π β (absβ-(π΅ / π΄)) β€ 1) |
847 | 826 | renegcld 11589 |
. . . . . . . . . 10
β’ (π β -(π΅ / π΄) β β) |
848 | 847, 833 | absled 15322 |
. . . . . . . . 9
β’ (π β ((absβ-(π΅ / π΄)) β€ 1 β (-1 β€ -(π΅ / π΄) β§ -(π΅ / π΄) β€ 1))) |
849 | 846, 848 | mpbid 231 |
. . . . . . . 8
β’ (π β (-1 β€ -(π΅ / π΄) β§ -(π΅ / π΄) β€ 1)) |
850 | 849 | simprd 497 |
. . . . . . 7
β’ (π β -(π΅ / π΄) β€ 1) |
851 | 829, 850 | eqbrtrrid 5146 |
. . . . . 6
β’ (π β (0 β (π΅ / π΄)) β€ 1) |
852 | | 0red 11165 |
. . . . . . 7
β’ (π β 0 β
β) |
853 | 852, 826,
833 | lesubaddd 11759 |
. . . . . 6
β’ (π β ((0 β (π΅ / π΄)) β€ 1 β 0 β€ (1 + (π΅ / π΄)))) |
854 | 851, 853 | mpbid 231 |
. . . . 5
β’ (π β 0 β€ (1 + (π΅ / π΄))) |
855 | 854 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β 0 β€
(1 + (π΅ / π΄))) |
856 | 46 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β π΄ β
β+) |
857 | 856 | rpred 12964 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β π΄ β
β) |
858 | 856 | rpge0d 12968 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β 0 β€
π΄) |
859 | 828, 855,
857, 858, 720 | mulcxpd 26099 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β (((1 +
(π΅ / π΄)) Β· π΄)βππΆ) = (((1 + (π΅ / π΄))βππΆ) Β· (π΄βππΆ))) |
860 | 809, 60, 48 | adddird 11187 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β ((1 +
(π΅ / π΄)) Β· π΄) = ((1 Β· π΄) + ((π΅ / π΄) Β· π΄))) |
861 | 48 | mulid2d 11180 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β (1
Β· π΄) = π΄) |
862 | 45, 48, 59 | divcan1d 11939 |
. . . . . 6
β’ ((π β§ Β¬ πΆ β β0) β ((π΅ / π΄) Β· π΄) = π΅) |
863 | 861, 862 | oveq12d 7380 |
. . . . 5
β’ ((π β§ Β¬ πΆ β β0) β ((1
Β· π΄) + ((π΅ / π΄) Β· π΄)) = (π΄ + π΅)) |
864 | 860, 863 | eqtrd 2777 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β ((1 +
(π΅ / π΄)) Β· π΄) = (π΄ + π΅)) |
865 | 864 | oveq1d 7377 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β (((1 +
(π΅ / π΄)) Β· π΄)βππΆ) = ((π΄ + π΅)βππΆ)) |
866 | 859, 865 | eqtr3d 2779 |
. 2
β’ ((π β§ Β¬ πΆ β β0) β (((1 +
(π΅ / π΄))βππΆ) Β· (π΄βππΆ)) = ((π΄ + π΅)βππΆ)) |
867 | 60 | adantr 482 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΅ / π΄) β
β) |
868 | | simpr 486 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β π β
β0) |
869 | 867, 868 | expcld 14058 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((π΅ / π΄)βπ) β β) |
870 | 733, 869 | mulcld 11182 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πΆCππ) Β· ((π΅ / π΄)βπ)) β β) |
871 | 46, 43, 53, 71, 72, 8, 6, 155, 2 | binomcxplemcvg 42708 |
. . . . . 6
β’ ((π β§ (π΅ / π΄) β π·) β (seq0( + , (πβ(π΅ / π΄))) β dom β β§ seq1( + ,
(πΈβ(π΅ / π΄))) β dom β )) |
872 | 871 | simpld 496 |
. . . . 5
β’ ((π β§ (π΅ / π΄) β π·) β seq0( + , (πβ(π΅ / π΄))) β dom β ) |
873 | 91, 872 | syldan 592 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β seq0( +
, (πβ(π΅ / π΄))) β dom β ) |
874 | 48, 720 | cxpcld 26079 |
. . . 4
β’ ((π β§ Β¬ πΆ β β0) β (π΄βππΆ) β
β) |
875 | 112, 675,
822, 870, 873, 874 | isummulc1 15655 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β
(Ξ£π β
β0 ((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ)) = Ξ£π β β0 (((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ))) |
876 | 44 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β π΅ β
β) |
877 | 47 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β π΄ β
β) |
878 | 835 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β π΄ β
0) |
879 | 876, 877,
878 | divrecd 11941 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΅ / π΄) = (π΅ Β· (1 / π΄))) |
880 | 879 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((π΅ / π΄)βπ) = ((π΅ Β· (1 / π΄))βπ)) |
881 | 877, 878 | reccld 11931 |
. . . . . . . . . . . 12
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (1 / π΄) β
β) |
882 | 876, 881,
868 | mulexpd 14073 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((π΅ Β· (1 /
π΄))βπ) = ((π΅βπ) Β· ((1 / π΄)βπ))) |
883 | 880, 882 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((π΅ / π΄)βπ) = ((π΅βπ) Β· ((1 / π΄)βπ))) |
884 | 883 | oveq2d 7378 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πΆCππ) Β· ((π΅ / π΄)βπ)) = ((πΆCππ) Β· ((π΅βπ) Β· ((1 / π΄)βπ)))) |
885 | 876, 868 | expcld 14058 |
. . . . . . . . . 10
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΅βπ) β
β) |
886 | 881, 868 | expcld 14058 |
. . . . . . . . . 10
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((1 / π΄)βπ) β
β) |
887 | 733, 885,
886 | mulassd 11185 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (((πΆCππ) Β· (π΅βπ)) Β· ((1 / π΄)βπ)) = ((πΆCππ) Β· ((π΅βπ) Β· ((1 / π΄)βπ)))) |
888 | 884, 887 | eqtr4d 2780 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πΆCππ) Β· ((π΅ / π΄)βπ)) = (((πΆCππ) Β· (π΅βπ)) Β· ((1 / π΄)βπ))) |
889 | 888 | oveq1d 7377 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ)) = ((((πΆCππ) Β· (π΅βπ)) Β· ((1 / π΄)βπ)) Β· (π΄βππΆ))) |
890 | 733, 885 | mulcld 11182 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((πΆCππ) Β· (π΅βπ)) β β) |
891 | 874 | adantr 482 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΄βππΆ) β β) |
892 | 890, 886,
891 | mul32d 11372 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((((πΆCππ) Β· (π΅βπ)) Β· ((1 / π΄)βπ)) Β· (π΄βππΆ)) = ((((πΆCππ) Β· (π΅βπ)) Β· (π΄βππΆ)) Β· ((1 / π΄)βπ))) |
893 | 890, 891,
886 | mulassd 11185 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((((πΆCππ) Β· (π΅βπ)) Β· (π΄βππΆ)) Β· ((1 / π΄)βπ)) = (((πΆCππ) Β· (π΅βπ)) Β· ((π΄βππΆ) Β· ((1 / π΄)βπ)))) |
894 | 889, 892,
893 | 3eqtrd 2781 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ)) = (((πΆCππ) Β· (π΅βπ)) Β· ((π΄βππΆ) Β· ((1 / π΄)βπ)))) |
895 | 868 | nn0cnd 12482 |
. . . . . . . . . 10
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β π β
β) |
896 | 877, 895 | cxpcld 26079 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΄βππ) β β) |
897 | 877, 878,
895 | cxpne0d 26084 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΄βππ) β 0) |
898 | 891, 896,
897 | divrecd 11941 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((π΄βππΆ) / (π΄βππ)) = ((π΄βππΆ) Β· (1 / (π΄βππ)))) |
899 | 71 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β πΆ β
β) |
900 | 877, 878,
899, 895 | cxpsubd 26089 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΄βπ(πΆ β π)) = ((π΄βππΆ) / (π΄βππ))) |
901 | 868 | nn0zd 12532 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β π β
β€) |
902 | 877, 878,
901 | exprecd 14066 |
. . . . . . . . . 10
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((1 / π΄)βπ) = (1 / (π΄βπ))) |
903 | | cxpexp 26039 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π β β0)
β (π΄βππ) = (π΄βπ)) |
904 | 877, 868,
903 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΄βππ) = (π΄βπ)) |
905 | 904 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (1 / (π΄βππ)) = (1 / (π΄βπ))) |
906 | 902, 905 | eqtr4d 2780 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((1 / π΄)βπ) = (1 / (π΄βππ))) |
907 | 906 | oveq2d 7378 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((π΄βππΆ) Β· ((1 / π΄)βπ)) = ((π΄βππΆ) Β· (1 / (π΄βππ)))) |
908 | 898, 900,
907 | 3eqtr4rd 2788 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β ((π΄βππΆ) Β· ((1 / π΄)βπ)) = (π΄βπ(πΆ β π))) |
909 | 908 | oveq2d 7378 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (((πΆCππ) Β· (π΅βπ)) Β· ((π΄βππΆ) Β· ((1 / π΄)βπ))) = (((πΆCππ) Β· (π΅βπ)) Β· (π΄βπ(πΆ β π)))) |
910 | 899, 895 | subcld 11519 |
. . . . . . . 8
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (πΆ β π) β
β) |
911 | 877, 910 | cxpcld 26079 |
. . . . . . 7
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (π΄βπ(πΆ β π)) β β) |
912 | 733, 885,
911 | mul32d 11372 |
. . . . . 6
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (((πΆCππ) Β· (π΅βπ)) Β· (π΄βπ(πΆ β π))) = (((πΆCππ) Β· (π΄βπ(πΆ β π))) Β· (π΅βπ))) |
913 | 894, 909,
912 | 3eqtrd 2781 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ)) = (((πΆCππ) Β· (π΄βπ(πΆ β π))) Β· (π΅βπ))) |
914 | 733, 911,
885 | mulassd 11185 |
. . . . 5
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (((πΆCππ) Β· (π΄βπ(πΆ β π))) Β· (π΅βπ)) = ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
915 | 913, 914 | eqtrd 2777 |
. . . 4
β’ (((π β§ Β¬ πΆ β β0) β§ π β β0)
β (((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ)) = ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
916 | 915 | sumeq2dv 15595 |
. . 3
β’ ((π β§ Β¬ πΆ β β0) β
Ξ£π β
β0 (((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ)) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
917 | 875, 916 | eqtrd 2777 |
. 2
β’ ((π β§ Β¬ πΆ β β0) β
(Ξ£π β
β0 ((πΆCππ) Β· ((π΅ / π΄)βπ)) Β· (π΄βππΆ)) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
918 | 825, 866,
917 | 3eqtr3d 2785 |
1
β’ ((π β§ Β¬ πΆ β β0) β ((π΄ + π΅)βππΆ) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |