Step | Hyp | Ref
| Expression |
1 | | binomcxplem.s |
. . . 4
β’ π = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
2 | | binomcxplem.p |
. . . . 5
β’ π = (π β π· β¦ Ξ£π β β0 ((πβπ)βπ)) |
3 | | binomcxplem.d |
. . . . . . 7
β’ π· = (β‘abs β (0[,)π
)) |
4 | | nfcv 2908 |
. . . . . . . 8
β’
β²πβ‘abs |
5 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π0 |
6 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π[,) |
7 | | binomcxplem.r |
. . . . . . . . . 10
β’ π
= sup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) |
8 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π
+ |
9 | | nfmpt1 5218 |
. . . . . . . . . . . . . . . 16
β’
β²π(π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
10 | 1, 9 | nfcxfr 2906 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
11 | | nfcv 2908 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
12 | 10, 11 | nffv 6857 |
. . . . . . . . . . . . . 14
β’
β²π(πβπ) |
13 | 5, 8, 12 | nfseq 13923 |
. . . . . . . . . . . . 13
β’
β²πseq0(
+ , (πβπ)) |
14 | 13 | nfel1 2924 |
. . . . . . . . . . . 12
β’
β²πseq0( + ,
(πβπ)) β dom β |
15 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²πβ |
16 | 14, 15 | nfrabw 3443 |
. . . . . . . . . . 11
β’
β²π{π β β β£ seq0( + , (πβπ)) β dom β } |
17 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²πβ* |
18 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π
< |
19 | 16, 17, 18 | nfsup 9394 |
. . . . . . . . . 10
β’
β²πsup({π β β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) |
20 | 7, 19 | nfcxfr 2906 |
. . . . . . . . 9
β’
β²ππ
|
21 | 5, 6, 20 | nfov 7392 |
. . . . . . . 8
β’
β²π(0[,)π
) |
22 | 4, 21 | nfima 6026 |
. . . . . . 7
β’
β²π(β‘abs
β (0[,)π
)) |
23 | 3, 22 | nfcxfr 2906 |
. . . . . 6
β’
β²ππ· |
24 | | nfcv 2908 |
. . . . . 6
β’
β²π¦π· |
25 | | nfcv 2908 |
. . . . . 6
β’
β²π¦Ξ£π β β0 ((πβπ)βπ) |
26 | | nfcv 2908 |
. . . . . . 7
β’
β²πβ0 |
27 | | nfcv 2908 |
. . . . . . . . 9
β’
β²ππ¦ |
28 | 10, 27 | nffv 6857 |
. . . . . . . 8
β’
β²π(πβπ¦) |
29 | | nfcv 2908 |
. . . . . . . 8
β’
β²ππ |
30 | 28, 29 | nffv 6857 |
. . . . . . 7
β’
β²π((πβπ¦)βπ) |
31 | 26, 30 | nfsum 15582 |
. . . . . 6
β’
β²πΞ£π β β0 ((πβπ¦)βπ) |
32 | | simpl 484 |
. . . . . . . . . 10
β’ ((π = π¦ β§ π β β0) β π = π¦) |
33 | 32 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π = π¦ β§ π β β0) β (πβπ) = (πβπ¦)) |
34 | 33 | fveq1d 6849 |
. . . . . . . 8
β’ ((π = π¦ β§ π β β0) β ((πβπ)βπ) = ((πβπ¦)βπ)) |
35 | 34 | sumeq2dv 15595 |
. . . . . . 7
β’ (π = π¦ β Ξ£π β β0 ((πβπ)βπ) = Ξ£π β β0 ((πβπ¦)βπ)) |
36 | | nfcv 2908 |
. . . . . . . 8
β’
β²π((πβπ¦)βπ) |
37 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²πβ |
38 | | nfmpt1 5218 |
. . . . . . . . . . . 12
β’
β²π(π β β0 β¦ ((πΉβπ) Β· (πβπ))) |
39 | 37, 38 | nfmpt 5217 |
. . . . . . . . . . 11
β’
β²π(π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
40 | 1, 39 | nfcxfr 2906 |
. . . . . . . . . 10
β’
β²ππ |
41 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²ππ¦ |
42 | 40, 41 | nffv 6857 |
. . . . . . . . 9
β’
β²π(πβπ¦) |
43 | | nfcv 2908 |
. . . . . . . . 9
β’
β²ππ |
44 | 42, 43 | nffv 6857 |
. . . . . . . 8
β’
β²π((πβπ¦)βπ) |
45 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β ((πβπ¦)βπ) = ((πβπ¦)βπ)) |
46 | 36, 44, 45 | cbvsumi 15589 |
. . . . . . 7
β’
Ξ£π β
β0 ((πβπ¦)βπ) = Ξ£π β β0 ((πβπ¦)βπ) |
47 | 35, 46 | eqtrdi 2793 |
. . . . . 6
β’ (π = π¦ β Ξ£π β β0 ((πβπ)βπ) = Ξ£π β β0 ((πβπ¦)βπ)) |
48 | 23, 24, 25, 31, 47 | cbvmptf 5219 |
. . . . 5
β’ (π β π· β¦ Ξ£π β β0 ((πβπ)βπ)) = (π¦ β π· β¦ Ξ£π β β0 ((πβπ¦)βπ)) |
49 | 2, 48 | eqtri 2765 |
. . . 4
β’ π = (π¦ β π· β¦ Ξ£π β β0 ((πβπ¦)βπ)) |
50 | | ovexd 7397 |
. . . . 5
β’ ((π β§ π β β0) β (πΆCππ) β V) |
51 | | binomcxplem.f |
. . . . . 6
β’ πΉ = (π β β0 β¦ (πΆCππ)) |
52 | 51 | a1i 11 |
. . . . 5
β’ (π β πΉ = (π β β0 β¦ (πΆCππ))) |
53 | 51 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β0) β πΉ = (π β β0 β¦ (πΆCππ))) |
54 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β β0) β§ π = π) β π = π) |
55 | 54 | oveq2d 7378 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π = π) β (πΆCππ) = (πΆCππ)) |
56 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β β0) β π β
β0) |
57 | | binomcxp.c |
. . . . . . . . 9
β’ (π β πΆ β β) |
58 | 57 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β0) β πΆ β
β) |
59 | 58, 56 | bcccl 42693 |
. . . . . . 7
β’ ((π β§ π β β0) β (πΆCππ) β
β) |
60 | 53, 55, 56, 59 | fvmptd 6960 |
. . . . . 6
β’ ((π β§ π β β0) β (πΉβπ) = (πΆCππ)) |
61 | 60, 59 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ π β β0) β (πΉβπ) β β) |
62 | 50, 52, 61 | fmpt2d 7076 |
. . . 4
β’ (π β πΉ:β0βΆβ) |
63 | | nfcv 2908 |
. . . . . . 7
β’
β²πβ |
64 | | nfcv 2908 |
. . . . . . 7
β’
β²π§β |
65 | | nfv 1918 |
. . . . . . 7
β’
β²π§seq0( + ,
(πβπ)) β dom β |
66 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π0 |
67 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π
+ |
68 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π(π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
69 | 1, 68 | nfcxfr 2906 |
. . . . . . . . . 10
β’
β²ππ |
70 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²ππ§ |
71 | 69, 70 | nffv 6857 |
. . . . . . . . 9
β’
β²π(πβπ§) |
72 | 66, 67, 71 | nfseq 13923 |
. . . . . . . 8
β’
β²πseq0(
+ , (πβπ§)) |
73 | 72 | nfel1 2924 |
. . . . . . 7
β’
β²πseq0( + ,
(πβπ§)) β dom β |
74 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π§ β (πβπ) = (πβπ§)) |
75 | 74 | seqeq3d 13921 |
. . . . . . . 8
β’ (π = π§ β seq0( + , (πβπ)) = seq0( + , (πβπ§))) |
76 | 75 | eleq1d 2823 |
. . . . . . 7
β’ (π = π§ β (seq0( + , (πβπ)) β dom β β seq0( + , (πβπ§)) β dom β )) |
77 | 63, 64, 65, 73, 76 | cbvrabw 3442 |
. . . . . 6
β’ {π β β β£ seq0( +
, (πβπ)) β dom β } = {π§ β β β£ seq0( +
, (πβπ§)) β dom β
} |
78 | 77 | supeq1i 9390 |
. . . . 5
β’
sup({π β
β β£ seq0( + , (πβπ)) β dom β }, β*,
< ) = sup({π§ β
β β£ seq0( + , (πβπ§)) β dom β }, β*,
< ) |
79 | 7, 78 | eqtri 2765 |
. . . 4
β’ π
= sup({π§ β β β£ seq0( + , (πβπ§)) β dom β }, β*,
< ) |
80 | 1 | fveq1i 6848 |
. . . . . . . . . . 11
β’ (πβπ§) = ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§) |
81 | | seqeq3 13918 |
. . . . . . . . . . 11
β’ ((πβπ§) = ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§) β seq0( + , (πβπ§)) = seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§))) |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . . 10
β’ seq0( + ,
(πβπ§)) = seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) |
83 | 82 | eleq1i 2829 |
. . . . . . . . 9
β’ (seq0( +
, (πβπ§)) β dom β β
seq0( + , ((π β
β β¦ (π β
β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β ) |
84 | 83 | rabbii 3416 |
. . . . . . . 8
β’ {π§ β β β£ seq0( +
, (πβπ§)) β dom β } = {π§ β β β£ seq0( +
, ((π β β
β¦ (π β
β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β } |
85 | 84 | supeq1i 9390 |
. . . . . . 7
β’
sup({π§ β
β β£ seq0( + , (πβπ§)) β dom β }, β*,
< ) = sup({π§ β
β β£ seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) |
86 | 7, 78, 85 | 3eqtrri 2770 |
. . . . . 6
β’
sup({π§ β
β β£ seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) = π
|
87 | 86 | eleq1i 2829 |
. . . . 5
β’
(sup({π§ β
β β£ seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) β β β π
β β) |
88 | 86 | oveq2i 7373 |
. . . . . 6
β’
((absβπ₯) +
sup({π§ β β
β£ seq0( + , ((π
β β β¦ (π
β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) = ((absβπ₯) +
π
) |
89 | 88 | oveq1i 7372 |
. . . . 5
β’
(((absβπ₯) +
sup({π§ β β
β£ seq0( + , ((π
β β β¦ (π
β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) / 2) = (((absβπ₯) + π
) / 2) |
90 | | eqid 2737 |
. . . . 5
β’
((absβπ₯) + 1)
= ((absβπ₯) +
1) |
91 | 87, 89, 90 | ifbieq12i 4518 |
. . . 4
β’
if(sup({π§ β
β β£ seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1)) = if(π
β β, (((absβπ₯) + π
) / 2), ((absβπ₯) + 1)) |
92 | | oveq1 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π β (π€βπ) = (πβπ)) |
93 | 92 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β ((πΉβπ) Β· (π€βπ)) = ((πΉβπ) Β· (πβπ))) |
94 | 93 | mpteq2dv 5212 |
. . . . . . . . . . . . . . 15
β’ (π€ = π β (π β β0 β¦ ((πΉβπ) Β· (π€βπ))) = (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
95 | 94 | cbvmptv 5223 |
. . . . . . . . . . . . . 14
β’ (π€ β β β¦ (π β β0
β¦ ((πΉβπ) Β· (π€βπ)))) = (π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ)))) |
96 | 95 | fveq1i 6848 |
. . . . . . . . . . . . 13
β’ ((π€ β β β¦ (π β β0
β¦ ((πΉβπ) Β· (π€βπ))))βπ§) = ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§) |
97 | | seqeq3 13918 |
. . . . . . . . . . . . 13
β’ (((π€ β β β¦ (π β β0
β¦ ((πΉβπ) Β· (π€βπ))))βπ§) = ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§) β seq0( + , ((π€ β β β¦ (π β β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) = seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§))) |
98 | 96, 97 | ax-mp 5 |
. . . . . . . . . . . 12
β’ seq0( + ,
((π€ β β β¦
(π β
β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) = seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) |
99 | 98 | eleq1i 2829 |
. . . . . . . . . . 11
β’ (seq0( +
, ((π€ β β
β¦ (π β
β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β β seq0( + ,
((π β β β¦
(π β
β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β ) |
100 | 99 | rabbii 3416 |
. . . . . . . . . 10
β’ {π§ β β β£ seq0( +
, ((π€ β β
β¦ (π β
β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β } = {π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β } |
101 | 100 | supeq1i 9390 |
. . . . . . . . 9
β’
sup({π§ β
β β£ seq0( + , ((π€ β β β¦ (π β β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< ) = sup({π§ β
β β£ seq0( + , ((π β β β¦ (π β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) |
102 | 101 | eleq1i 2829 |
. . . . . . . 8
β’
(sup({π§ β
β β£ seq0( + , ((π€ β β β¦ (π β β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< ) β β β sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) β β) |
103 | 101 | oveq2i 7373 |
. . . . . . . . 9
β’
((absβπ₯) +
sup({π§ β β
β£ seq0( + , ((π€
β β β¦ (π
β β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< )) = ((absβπ₯) +
sup({π§ β β
β£ seq0( + , ((π
β β β¦ (π
β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) |
104 | 103 | oveq1i 7372 |
. . . . . . . 8
β’
(((absβπ₯) +
sup({π§ β β
β£ seq0( + , ((π€
β β β¦ (π
β β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< )) / 2) = (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) / 2) |
105 | 102, 104,
90 | ifbieq12i 4518 |
. . . . . . 7
β’
if(sup({π§ β
β β£ seq0( + , ((π€ β β β¦ (π β β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π€ β β β¦ (π β β0
β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1)) = if(sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1)) |
106 | 105 | oveq2i 7373 |
. . . . . 6
β’
((absβπ₯) +
if(sup({π§ β β
β£ seq0( + , ((π€
β β β¦ (π
β β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π€ β β β¦ (π β β0
β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1))) = ((absβπ₯) + if(sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1))) |
107 | 106 | oveq1i 7372 |
. . . . 5
β’
(((absβπ₯) +
if(sup({π§ β β
β£ seq0( + , ((π€
β β β¦ (π
β β0 β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π€ β β β¦ (π β β0
β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1))) / 2) = (((absβπ₯) + if(sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1))) / 2) |
108 | 107 | oveq2i 7373 |
. . . 4
β’
(0(ballβ(abs β β ))(((absβπ₯) + if(sup({π§ β β β£ seq0( + , ((π€ β β β¦ (π β β0
β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π€ β β β¦ (π β β0
β¦ ((πΉβπ) Β· (π€βπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1))) / 2)) = (0(ballβ(abs β
β ))(((absβπ₯) +
if(sup({π§ β β
β£ seq0( + , ((π
β β β¦ (π
β β0 β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< ) β β, (((absβπ₯) + sup({π§ β β β£ seq0( + , ((π β β β¦ (π β β0
β¦ ((πΉβπ) Β· (πβπ))))βπ§)) β dom β }, β*,
< )) / 2), ((absβπ₯) + 1))) / 2)) |
109 | 1, 49, 62, 79, 3, 91, 108 | pserdv2 25805 |
. . 3
β’ (π β (β D π) = (π¦ β π· β¦ Ξ£π β β ((π Β· (πΉβπ)) Β· (π¦β(π β 1))))) |
110 | | cnvimass 6038 |
. . . . . . . 8
β’ (β‘abs β (0[,)π
)) β dom abs |
111 | 3, 110 | eqsstri 3983 |
. . . . . . 7
β’ π· β dom
abs |
112 | | absf 15229 |
. . . . . . . 8
β’
abs:ββΆβ |
113 | 112 | fdmi 6685 |
. . . . . . 7
β’ dom abs =
β |
114 | 111, 113 | sseqtri 3985 |
. . . . . 6
β’ π· β
β |
115 | 114 | sseli 3945 |
. . . . 5
β’ (π¦ β π· β π¦ β β) |
116 | | binomcxplem.e |
. . . . . . . . . 10
β’ πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) |
117 | 116 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β πΈ = (π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1)))))) |
118 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β β) β§ π = π¦) β§ π β β) β π = π¦) |
119 | 118 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β β) β§ π = π¦) β§ π β β) β (πβ(π β 1)) = (π¦β(π β 1))) |
120 | 119 | oveq2d 7378 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β β) β§ π = π¦) β§ π β β) β ((π Β· (πΉβπ)) Β· (πβ(π β 1))) = ((π Β· (πΉβπ)) Β· (π¦β(π β 1)))) |
121 | 120 | mpteq2dva 5210 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π = π¦) β (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1)))) = (π β β β¦ ((π Β· (πΉβπ)) Β· (π¦β(π β 1))))) |
122 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β π¦ β β) |
123 | | nnex 12166 |
. . . . . . . . . . 11
β’ β
β V |
124 | 123 | mptex 7178 |
. . . . . . . . . 10
β’ (π β β β¦ ((π Β· (πΉβπ)) Β· (π¦β(π β 1)))) β V |
125 | 124 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (π β β β¦ ((π Β· (πΉβπ)) Β· (π¦β(π β 1)))) β V) |
126 | 117, 121,
122, 125 | fvmptd 6960 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (πΈβπ¦) = (π β β β¦ ((π Β· (πΉβπ)) Β· (π¦β(π β 1))))) |
127 | 126 | adantr 482 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β β) β (πΈβπ¦) = (π β β β¦ ((π Β· (πΉβπ)) Β· (π¦β(π β 1))))) |
128 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π β β) β§ π = π) β π = π) |
129 | 128 | fveq2d 6851 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π β β) β§ π = π) β (πΉβπ) = (πΉβπ)) |
130 | 128, 129 | oveq12d 7380 |
. . . . . . . 8
β’ ((((π β§ π¦ β β) β§ π β β) β§ π = π) β (π Β· (πΉβπ)) = (π Β· (πΉβπ))) |
131 | 128 | oveq1d 7377 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π β β) β§ π = π) β (π β 1) = (π β 1)) |
132 | 131 | oveq2d 7378 |
. . . . . . . 8
β’ ((((π β§ π¦ β β) β§ π β β) β§ π = π) β (π¦β(π β 1)) = (π¦β(π β 1))) |
133 | 130, 132 | oveq12d 7380 |
. . . . . . 7
β’ ((((π β§ π¦ β β) β§ π β β) β§ π = π) β ((π Β· (πΉβπ)) Β· (π¦β(π β 1))) = ((π Β· (πΉβπ)) Β· (π¦β(π β 1)))) |
134 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β β) β π β β) |
135 | | ovexd 7397 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β β) β ((π Β· (πΉβπ)) Β· (π¦β(π β 1))) β V) |
136 | 127, 133,
134, 135 | fvmptd 6960 |
. . . . . 6
β’ (((π β§ π¦ β β) β§ π β β) β ((πΈβπ¦)βπ) = ((π Β· (πΉβπ)) Β· (π¦β(π β 1)))) |
137 | 136 | sumeq2dv 15595 |
. . . . 5
β’ ((π β§ π¦ β β) β Ξ£π β β ((πΈβπ¦)βπ) = Ξ£π β β ((π Β· (πΉβπ)) Β· (π¦β(π β 1)))) |
138 | 115, 137 | sylan2 594 |
. . . 4
β’ ((π β§ π¦ β π·) β Ξ£π β β ((πΈβπ¦)βπ) = Ξ£π β β ((π Β· (πΉβπ)) Β· (π¦β(π β 1)))) |
139 | 138 | mpteq2dva 5210 |
. . 3
β’ (π β (π¦ β π· β¦ Ξ£π β β ((πΈβπ¦)βπ)) = (π¦ β π· β¦ Ξ£π β β ((π Β· (πΉβπ)) Β· (π¦β(π β 1))))) |
140 | 109, 139 | eqtr4d 2780 |
. 2
β’ (π β (β D π) = (π¦ β π· β¦ Ξ£π β β ((πΈβπ¦)βπ))) |
141 | | nfcv 2908 |
. . . 4
β’
β²πβ |
142 | | nfmpt1 5218 |
. . . . . . 7
β’
β²π(π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) |
143 | 116, 142 | nfcxfr 2906 |
. . . . . 6
β’
β²ππΈ |
144 | 143, 27 | nffv 6857 |
. . . . 5
β’
β²π(πΈβπ¦) |
145 | | nfcv 2908 |
. . . . 5
β’
β²ππ |
146 | 144, 145 | nffv 6857 |
. . . 4
β’
β²π((πΈβπ¦)βπ) |
147 | 141, 146 | nfsum 15582 |
. . 3
β’
β²πΞ£π β β ((πΈβπ¦)βπ) |
148 | | nfcv 2908 |
. . 3
β’
β²π¦Ξ£π β β ((πΈβπ)βπ) |
149 | | simpl 484 |
. . . . . . 7
β’ ((π¦ = π β§ π β β) β π¦ = π) |
150 | 149 | fveq2d 6851 |
. . . . . 6
β’ ((π¦ = π β§ π β β) β (πΈβπ¦) = (πΈβπ)) |
151 | 150 | fveq1d 6849 |
. . . . 5
β’ ((π¦ = π β§ π β β) β ((πΈβπ¦)βπ) = ((πΈβπ)βπ)) |
152 | 151 | sumeq2dv 15595 |
. . . 4
β’ (π¦ = π β Ξ£π β β ((πΈβπ¦)βπ) = Ξ£π β β ((πΈβπ)βπ)) |
153 | | nfmpt1 5218 |
. . . . . . . . 9
β’
β²π(π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1)))) |
154 | 37, 153 | nfmpt 5217 |
. . . . . . . 8
β’
β²π(π β β β¦ (π β β β¦ ((π Β· (πΉβπ)) Β· (πβ(π β 1))))) |
155 | 116, 154 | nfcxfr 2906 |
. . . . . . 7
β’
β²ππΈ |
156 | | nfcv 2908 |
. . . . . . 7
β’
β²ππ |
157 | 155, 156 | nffv 6857 |
. . . . . 6
β’
β²π(πΈβπ) |
158 | | nfcv 2908 |
. . . . . 6
β’
β²ππ |
159 | 157, 158 | nffv 6857 |
. . . . 5
β’
β²π((πΈβπ)βπ) |
160 | | nfcv 2908 |
. . . . 5
β’
β²π((πΈβπ)βπ) |
161 | | fveq2 6847 |
. . . . 5
β’ (π = π β ((πΈβπ)βπ) = ((πΈβπ)βπ)) |
162 | 159, 160,
161 | cbvsumi 15589 |
. . . 4
β’
Ξ£π β
β ((πΈβπ)βπ) = Ξ£π β β ((πΈβπ)βπ) |
163 | 152, 162 | eqtrdi 2793 |
. . 3
β’ (π¦ = π β Ξ£π β β ((πΈβπ¦)βπ) = Ξ£π β β ((πΈβπ)βπ)) |
164 | 24, 23, 147, 148, 163 | cbvmptf 5219 |
. 2
β’ (π¦ β π· β¦ Ξ£π β β ((πΈβπ¦)βπ)) = (π β π· β¦ Ξ£π β β ((πΈβπ)βπ)) |
165 | 140, 164 | eqtrdi 2793 |
1
β’ (π β (β D π) = (π β π· β¦ Ξ£π β β ((πΈβπ)βπ))) |