Step | Hyp | Ref
| Expression |
1 | | nfv 1917 |
. . . . . 6
β’
β²π‘(π β§ π₯ β π) |
2 | | nfcv 2907 |
. . . . . 6
β’
β²π‘((π»βπ)βπ₯) |
3 | | dvnprodlem2.t |
. . . . . . . 8
β’ (π β π β Fin) |
4 | | dvnprodlem2.r |
. . . . . . . 8
β’ (π β π
β π) |
5 | | ssfi 9117 |
. . . . . . . 8
β’ ((π β Fin β§ π
β π) β π
β Fin) |
6 | 3, 4, 5 | syl2anc 584 |
. . . . . . 7
β’ (π β π
β Fin) |
7 | 6 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β π) β π
β Fin) |
8 | | dvnprodlem2.z |
. . . . . . 7
β’ (π β π β (π β π
)) |
9 | 8 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β π) β π β (π β π
)) |
10 | 8 | eldifbd 3923 |
. . . . . . 7
β’ (π β Β¬ π β π
) |
11 | 10 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β π) β Β¬ π β π
) |
12 | | simpl 483 |
. . . . . . . . 9
β’ ((π β§ π‘ β π
) β π) |
13 | 4 | sselda 3944 |
. . . . . . . . 9
β’ ((π β§ π‘ β π
) β π‘ β π) |
14 | | dvnprodlem2.h |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (π»βπ‘):πβΆβ) |
15 | 12, 13, 14 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ π‘ β π
) β (π»βπ‘):πβΆβ) |
16 | 15 | adantlr 713 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π‘ β π
) β (π»βπ‘):πβΆβ) |
17 | | simplr 767 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π‘ β π
) β π₯ β π) |
18 | 16, 17 | ffvelcdmd 7036 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π‘ β π
) β ((π»βπ‘)βπ₯) β β) |
19 | | fveq2 6842 |
. . . . . . 7
β’ (π‘ = π β (π»βπ‘) = (π»βπ)) |
20 | 19 | fveq1d 6844 |
. . . . . 6
β’ (π‘ = π β ((π»βπ‘)βπ₯) = ((π»βπ)βπ₯)) |
21 | | id 22 |
. . . . . . . . 9
β’ (π β π) |
22 | | eldifi 4086 |
. . . . . . . . . 10
β’ (π β (π β π
) β π β π) |
23 | 8, 22 | syl 17 |
. . . . . . . . 9
β’ (π β π β π) |
24 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
25 | | id 22 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π β§ π β π)) |
26 | | eleq1 2825 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (π‘ β π β π β π)) |
27 | 26 | anbi2d 629 |
. . . . . . . . . . . 12
β’ (π‘ = π β ((π β§ π‘ β π) β (π β§ π β π))) |
28 | 19 | feq1d 6653 |
. . . . . . . . . . . 12
β’ (π‘ = π β ((π»βπ‘):πβΆβ β (π»βπ):πβΆβ)) |
29 | 27, 28 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π‘ = π β (((π β§ π‘ β π) β (π»βπ‘):πβΆβ) β ((π β§ π β π) β (π»βπ):πβΆβ))) |
30 | 29, 14 | vtoclg 3525 |
. . . . . . . . . 10
β’ (π β π β ((π β§ π β π) β (π»βπ):πβΆβ)) |
31 | 24, 25, 30 | sylc 65 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π»βπ):πβΆβ) |
32 | 21, 23, 31 | syl2anc 584 |
. . . . . . . 8
β’ (π β (π»βπ):πβΆβ) |
33 | 32 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π»βπ):πβΆβ) |
34 | | simpr 485 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π₯ β π) |
35 | 33, 34 | ffvelcdmd 7036 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((π»βπ)βπ₯) β β) |
36 | 1, 2, 7, 9, 11, 18, 20, 35 | fprodsplitsn 15872 |
. . . . 5
β’ ((π β§ π₯ β π) β βπ‘ β (π
βͺ {π})((π»βπ‘)βπ₯) = (βπ‘ β π
((π»βπ‘)βπ₯) Β· ((π»βπ)βπ₯))) |
37 | 36 | mpteq2dva 5205 |
. . . 4
β’ (π β (π₯ β π β¦ βπ‘ β (π
βͺ {π})((π»βπ‘)βπ₯)) = (π₯ β π β¦ (βπ‘ β π
((π»βπ‘)βπ₯) Β· ((π»βπ)βπ₯)))) |
38 | 37 | oveq2d 7373 |
. . 3
β’ (π β (π Dπ (π₯ β π β¦ βπ‘ β (π
βͺ {π})((π»βπ‘)βπ₯))) = (π Dπ (π₯ β π β¦ (βπ‘ β π
((π»βπ‘)βπ₯) Β· ((π»βπ)βπ₯))))) |
39 | 38 | fveq1d 6844 |
. 2
β’ (π β ((π Dπ (π₯ β π β¦ βπ‘ β (π
βͺ {π})((π»βπ‘)βπ₯)))βπ½) = ((π Dπ (π₯ β π β¦ (βπ‘ β π
((π»βπ‘)βπ₯) Β· ((π»βπ)βπ₯))))βπ½)) |
40 | | dvnprodlem2.s |
. . 3
β’ (π β π β {β, β}) |
41 | | dvnprodlem2.x |
. . 3
β’ (π β π β
((TopOpenββfld) βΎt π)) |
42 | 1, 7, 18 | fprodclf 15875 |
. . 3
β’ ((π β§ π₯ β π) β βπ‘ β π
((π»βπ‘)βπ₯) β β) |
43 | | dvnprodlem2.j |
. . . 4
β’ (π β π½ β (0...π)) |
44 | | elfznn0 13534 |
. . . 4
β’ (π½ β (0...π) β π½ β
β0) |
45 | 43, 44 | syl 17 |
. . 3
β’ (π β π½ β
β0) |
46 | | eqid 2736 |
. . 3
β’ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)) = (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)) |
47 | | eqid 2736 |
. . 3
β’ (π₯ β π β¦ ((π»βπ)βπ₯)) = (π₯ β π β¦ ((π»βπ)βπ₯)) |
48 | | dvnprodlem2.c |
. . . . . . . . . 10
β’ πΆ = (π β π« π β¦ (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π})) |
49 | | oveq2 7365 |
. . . . . . . . . . . . 13
β’ (π = π
β ((0...π) βm π ) = ((0...π) βm π
)) |
50 | | rabeq 3421 |
. . . . . . . . . . . . 13
β’
(((0...π)
βm π ) =
((0...π) βm
π
) β {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π (πβπ‘) = π}) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . 12
β’ (π = π
β {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π (πβπ‘) = π}) |
52 | | sumeq1 15573 |
. . . . . . . . . . . . . 14
β’ (π = π
β Ξ£π‘ β π (πβπ‘) = Ξ£π‘ β π
(πβπ‘)) |
53 | 52 | eqeq1d 2738 |
. . . . . . . . . . . . 13
β’ (π = π
β (Ξ£π‘ β π (πβπ‘) = π β Ξ£π‘ β π
(πβπ‘) = π)) |
54 | 53 | rabbidv 3415 |
. . . . . . . . . . . 12
β’ (π = π
β {π β ((0...π) βm π
) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
55 | 51, 54 | eqtrd 2776 |
. . . . . . . . . . 11
β’ (π = π
β {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
56 | 55 | mpteq2dv 5207 |
. . . . . . . . . 10
β’ (π = π
β (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π}) = (π β β0 β¦ {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π})) |
57 | | ssexg 5280 |
. . . . . . . . . . . . . 14
β’ ((π
β π β§ π β Fin) β π
β V) |
58 | 4, 3, 57 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (π β π
β V) |
59 | | elpwg 4563 |
. . . . . . . . . . . . 13
β’ (π
β V β (π
β π« π β π
β π)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π
β π« π β π
β π)) |
61 | 4, 60 | mpbird 256 |
. . . . . . . . . . 11
β’ (π β π
β π« π) |
62 | 61 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π½)) β π
β π« π) |
63 | | nn0ex 12419 |
. . . . . . . . . . . 12
β’
β0 β V |
64 | 63 | mptex 7173 |
. . . . . . . . . . 11
β’ (π β β0
β¦ {π β
((0...π) βm
π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) β V |
65 | 64 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π½)) β (π β β0 β¦ {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) β V) |
66 | 48, 56, 62, 65 | fvmptd3 6971 |
. . . . . . . . 9
β’ ((π β§ π β (0...π½)) β (πΆβπ
) = (π β β0 β¦ {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π})) |
67 | | oveq2 7365 |
. . . . . . . . . . . . 13
β’ (π = π β (0...π) = (0...π)) |
68 | 67 | oveq1d 7372 |
. . . . . . . . . . . 12
β’ (π = π β ((0...π) βm π
) = ((0...π) βm π
)) |
69 | | rabeq 3421 |
. . . . . . . . . . . 12
β’
(((0...π)
βm π
) =
((0...π) βm
π
) β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . 11
β’ (π = π β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
71 | | eqeq2 2748 |
. . . . . . . . . . . 12
β’ (π = π β (Ξ£π‘ β π
(πβπ‘) = π β Ξ£π‘ β π
(πβπ‘) = π)) |
72 | 71 | rabbidv 3415 |
. . . . . . . . . . 11
β’ (π = π β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
73 | 70, 72 | eqtrd 2776 |
. . . . . . . . . 10
β’ (π = π β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
74 | 73 | adantl 482 |
. . . . . . . . 9
β’ (((π β§ π β (0...π½)) β§ π = π) β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} = {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
75 | | elfznn0 13534 |
. . . . . . . . . 10
β’ (π β (0...π½) β π β β0) |
76 | 75 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π β (0...π½)) β π β β0) |
77 | | fzfid 13878 |
. . . . . . . . . . . 12
β’ (π β (0...π) β Fin) |
78 | | mapfi 9292 |
. . . . . . . . . . . 12
β’
(((0...π) β Fin
β§ π
β Fin) β
((0...π) βm
π
) β
Fin) |
79 | 77, 6, 78 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β ((0...π) βm π
) β Fin) |
80 | 79 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π½)) β ((0...π) βm π
) β Fin) |
81 | | ssrab2 4037 |
. . . . . . . . . . 11
β’ {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} β ((0...π) βm π
) |
82 | 81 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π½)) β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} β ((0...π) βm π
)) |
83 | 80, 82 | ssexd 5281 |
. . . . . . . . 9
β’ ((π β§ π β (0...π½)) β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} β V) |
84 | 66, 74, 76, 83 | fvmptd 6955 |
. . . . . . . 8
β’ ((π β§ π β (0...π½)) β ((πΆβπ
)βπ) = {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
85 | | ssfi 9117 |
. . . . . . . . . 10
β’
((((0...π)
βm π
)
β Fin β§ {π β
((0...π) βm
π
) β£ Ξ£π‘ β π
(πβπ‘) = π} β ((0...π) βm π
)) β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} β Fin) |
86 | 79, 81, 85 | sylancl 586 |
. . . . . . . . 9
β’ (π β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} β Fin) |
87 | 86 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β (0...π½)) β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} β Fin) |
88 | 84, 87 | eqeltrd 2837 |
. . . . . . 7
β’ ((π β§ π β (0...π½)) β ((πΆβπ
)βπ) β Fin) |
89 | 88 | adantr 481 |
. . . . . 6
β’ (((π β§ π β (0...π½)) β§ π₯ β π) β ((πΆβπ
)βπ) β Fin) |
90 | 75 | faccld 14184 |
. . . . . . . . . . 11
β’ (π β (0...π½) β (!βπ) β β) |
91 | 90 | nncnd 12169 |
. . . . . . . . . 10
β’ (π β (0...π½) β (!βπ) β β) |
92 | 91 | ad2antlr 725 |
. . . . . . . . 9
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β (!βπ) β β) |
93 | 6 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΆβπ
)βπ)) β π
β Fin) |
94 | 93 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β π
β Fin) |
95 | | elfznn0 13534 |
. . . . . . . . . . . . . . 15
β’ (π§ β (0...π) β π§ β β0) |
96 | 95 | ssriv 3948 |
. . . . . . . . . . . . . 14
β’
(0...π) β
β0 |
97 | 96 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (0...π) β
β0) |
98 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β π β ((πΆβπ
)βπ)) |
99 | 84 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π½)) β (π β ((πΆβπ
)βπ) β π β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π})) |
100 | 99 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β (π β ((πΆβπ
)βπ) β π β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π})) |
101 | 98, 100 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β π β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π}) |
102 | 81 | sseli 3940 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π β ((0...π) βm π
) β£ Ξ£π‘ β π
(πβπ‘) = π} β π β ((0...π) βm π
)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β π β ((0...π) βm π
)) |
104 | | elmapi 8787 |
. . . . . . . . . . . . . . . 16
β’ (π β ((0...π) βm π
) β π:π
βΆ(0...π)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β π:π
βΆ(0...π)) |
106 | 105 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β π:π
βΆ(0...π)) |
107 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β π‘ β π
) |
108 | 106, 107 | ffvelcdmd 7036 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (πβπ‘) β (0...π)) |
109 | 97, 108 | sseldd 3945 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (πβπ‘) β
β0) |
110 | 109 | faccld 14184 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (!β(πβπ‘)) β β) |
111 | 110 | nncnd 12169 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (!β(πβπ‘)) β β) |
112 | 94, 111 | fprodcl 15835 |
. . . . . . . . 9
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β βπ‘ β π
(!β(πβπ‘)) β β) |
113 | 110 | nnne0d 12203 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (!β(πβπ‘)) β 0) |
114 | 94, 111, 113 | fprodn0 15862 |
. . . . . . . . 9
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β βπ‘ β π
(!β(πβπ‘)) β 0) |
115 | 92, 112, 114 | divcld 11931 |
. . . . . . . 8
β’ (((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β ((!βπ) / βπ‘ β π
(!β(πβπ‘))) β β) |
116 | 115 | adantlr 713 |
. . . . . . 7
β’ ((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β ((!βπ) / βπ‘ β π
(!β(πβπ‘))) β β) |
117 | 94 | adantlr 713 |
. . . . . . . 8
β’ ((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β π
β Fin) |
118 | 21 | ad4antr 730 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β π) |
119 | 118, 13 | sylancom 588 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β π‘ β π) |
120 | | elfzuz3 13438 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π½) β π½ β (β€β₯βπ)) |
121 | | fzss2 13481 |
. . . . . . . . . . . . . . . 16
β’ (π½ β
(β€β₯βπ) β (0...π) β (0...π½)) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β (0...π) β (0...π½)) |
123 | 122 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π½)) β (0...π) β (0...π½)) |
124 | 45 | nn0zd 12525 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π½ β β€) |
125 | | dvnprodlem2.n |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β
β0) |
126 | 125 | nn0zd 12525 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β€) |
127 | | elfzle2 13445 |
. . . . . . . . . . . . . . . . . . 19
β’ (π½ β (0...π) β π½ β€ π) |
128 | 43, 127 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π½ β€ π) |
129 | 124, 126,
128 | 3jca 1128 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π½ β β€ β§ π β β€ β§ π½ β€ π)) |
130 | | eluz2 12769 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯βπ½) β (π½ β β€ β§ π β β€ β§ π½ β€ π)) |
131 | 129, 130 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (β€β₯βπ½)) |
132 | | fzss2 13481 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ½) β (0...π½) β (0...π)) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β (0...π)) |
134 | 133 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π½)) β (0...π½) β (0...π)) |
135 | 123, 134 | sstrd 3954 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π½)) β (0...π) β (0...π)) |
136 | 135 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (0...π) β (0...π)) |
137 | 136, 108 | sseldd 3945 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (πβπ‘) β (0...π)) |
138 | 137 | adantllr 717 |
. . . . . . . . . 10
β’
(((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (πβπ‘) β (0...π)) |
139 | | fvex 6855 |
. . . . . . . . . . 11
β’ (πβπ‘) β V |
140 | | eleq1 2825 |
. . . . . . . . . . . . 13
β’ (π = (πβπ‘) β (π β (0...π) β (πβπ‘) β (0...π))) |
141 | 140 | 3anbi3d 1442 |
. . . . . . . . . . . 12
β’ (π = (πβπ‘) β ((π β§ π‘ β π β§ π β (0...π)) β (π β§ π‘ β π β§ (πβπ‘) β (0...π)))) |
142 | | fveq2 6842 |
. . . . . . . . . . . . 13
β’ (π = (πβπ‘) β ((π Dπ (π»βπ‘))βπ) = ((π Dπ (π»βπ‘))β(πβπ‘))) |
143 | 142 | feq1d 6653 |
. . . . . . . . . . . 12
β’ (π = (πβπ‘) β (((π Dπ (π»βπ‘))βπ):πβΆβ β ((π Dπ (π»βπ‘))β(πβπ‘)):πβΆβ)) |
144 | 141, 143 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π = (πβπ‘) β (((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) β ((π β§ π‘ β π β§ (πβπ‘) β (0...π)) β ((π Dπ (π»βπ‘))β(πβπ‘)):πβΆβ))) |
145 | | dvnprodlem2.dvnh |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) |
146 | 139, 144,
145 | vtocl 3518 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π β§ (πβπ‘) β (0...π)) β ((π Dπ (π»βπ‘))β(πβπ‘)):πβΆβ) |
147 | 118, 119,
138, 146 | syl3anc 1371 |
. . . . . . . . 9
β’
(((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β ((π Dπ (π»βπ‘))β(πβπ‘)):πβΆβ) |
148 | | simpllr 774 |
. . . . . . . . 9
β’
(((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β π₯ β π) |
149 | 147, 148 | ffvelcdmd 7036 |
. . . . . . . 8
β’
(((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β§ π‘ β π
) β (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) β β) |
150 | 117, 149 | fprodcl 15835 |
. . . . . . 7
β’ ((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) β β) |
151 | 116, 150 | mulcld 11175 |
. . . . . 6
β’ ((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β (((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) β β) |
152 | 89, 151 | fsumcl 15618 |
. . . . 5
β’ (((π β§ π β (0...π½)) β§ π₯ β π) β Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) β β) |
153 | 152 | fmpttd 7063 |
. . . 4
β’ ((π β§ π β (0...π½)) β (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))):πβΆβ) |
154 | | dvnprodlem2.ind |
. . . . . . 7
β’ (π β βπ β (0...π)((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
155 | 154 | adantr 481 |
. . . . . 6
β’ ((π β§ π β (0...π½)) β βπ β (0...π)((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
156 | | 0zd 12511 |
. . . . . . 7
β’ ((π β§ π β (0...π½)) β 0 β β€) |
157 | 126 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β (0...π½)) β π β β€) |
158 | | elfzelz 13441 |
. . . . . . . 8
β’ (π β (0...π½) β π β β€) |
159 | 158 | adantl 482 |
. . . . . . 7
β’ ((π β§ π β (0...π½)) β π β β€) |
160 | | elfzle1 13444 |
. . . . . . . 8
β’ (π β (0...π½) β 0 β€ π) |
161 | 160 | adantl 482 |
. . . . . . 7
β’ ((π β§ π β (0...π½)) β 0 β€ π) |
162 | 159 | zred 12607 |
. . . . . . . 8
β’ ((π β§ π β (0...π½)) β π β β) |
163 | 45 | nn0red 12474 |
. . . . . . . . 9
β’ (π β π½ β β) |
164 | 163 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β (0...π½)) β π½ β β) |
165 | 157 | zred 12607 |
. . . . . . . 8
β’ ((π β§ π β (0...π½)) β π β β) |
166 | | elfzle2 13445 |
. . . . . . . . 9
β’ (π β (0...π½) β π β€ π½) |
167 | 166 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π½)) β π β€ π½) |
168 | 128 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β (0...π½)) β π½ β€ π) |
169 | 162, 164,
165, 167, 168 | letrd 11312 |
. . . . . . 7
β’ ((π β§ π β (0...π½)) β π β€ π) |
170 | 156, 157,
159, 161, 169 | elfzd 13432 |
. . . . . 6
β’ ((π β§ π β (0...π½)) β π β (0...π)) |
171 | | rspa 3231 |
. . . . . 6
β’
((βπ β
(0...π)((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) β§ π β (0...π)) β ((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
172 | 155, 170,
171 | syl2anc 584 |
. . . . 5
β’ ((π β§ π β (0...π½)) β ((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
173 | 172 | feq1d 6653 |
. . . 4
β’ ((π β§ π β (0...π½)) β (((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ):πβΆβ β (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))):πβΆβ)) |
174 | 153, 173 | mpbird 256 |
. . 3
β’ ((π β§ π β (0...π½)) β ((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ):πβΆβ) |
175 | 23 | adantr 481 |
. . . . 5
β’ ((π β§ π β (0...π½)) β π β π) |
176 | | simpl 483 |
. . . . . 6
β’ ((π β§ π β (0...π½)) β π) |
177 | 176, 175,
170 | 3jca 1128 |
. . . . 5
β’ ((π β§ π β (0...π½)) β (π β§ π β π β§ π β (0...π))) |
178 | 26 | 3anbi2d 1441 |
. . . . . . 7
β’ (π‘ = π β ((π β§ π‘ β π β§ π β (0...π)) β (π β§ π β π β§ π β (0...π)))) |
179 | 19 | oveq2d 7373 |
. . . . . . . . 9
β’ (π‘ = π β (π Dπ (π»βπ‘)) = (π Dπ (π»βπ))) |
180 | 179 | fveq1d 6844 |
. . . . . . . 8
β’ (π‘ = π β ((π Dπ (π»βπ‘))βπ) = ((π Dπ (π»βπ))βπ)) |
181 | 180 | feq1d 6653 |
. . . . . . 7
β’ (π‘ = π β (((π Dπ (π»βπ‘))βπ):πβΆβ β ((π Dπ (π»βπ))βπ):πβΆβ)) |
182 | 178, 181 | imbi12d 344 |
. . . . . 6
β’ (π‘ = π β (((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) β ((π β§ π β π β§ π β (0...π)) β ((π Dπ (π»βπ))βπ):πβΆβ))) |
183 | | eleq1 2825 |
. . . . . . . . 9
β’ (π = π β (π β (0...π) β π β (0...π))) |
184 | 183 | 3anbi3d 1442 |
. . . . . . . 8
β’ (π = π β ((π β§ π‘ β π β§ π β (0...π)) β (π β§ π‘ β π β§ π β (0...π)))) |
185 | | fveq2 6842 |
. . . . . . . . 9
β’ (π = π β ((π Dπ (π»βπ‘))βπ) = ((π Dπ (π»βπ‘))βπ)) |
186 | 185 | feq1d 6653 |
. . . . . . . 8
β’ (π = π β (((π Dπ (π»βπ‘))βπ):πβΆβ β ((π Dπ (π»βπ‘))βπ):πβΆβ)) |
187 | 184, 186 | imbi12d 344 |
. . . . . . 7
β’ (π = π β (((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) β ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ))) |
188 | 187, 145 | chvarvv 2002 |
. . . . . 6
β’ ((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) |
189 | 182, 188 | vtoclg 3525 |
. . . . 5
β’ (π β π β ((π β§ π β π β§ π β (0...π)) β ((π Dπ (π»βπ))βπ):πβΆβ)) |
190 | 175, 177,
189 | sylc 65 |
. . . 4
β’ ((π β§ π β (0...π½)) β ((π Dπ (π»βπ))βπ):πβΆβ) |
191 | 32 | feqmptd 6910 |
. . . . . . . . 9
β’ (π β (π»βπ) = (π₯ β π β¦ ((π»βπ)βπ₯))) |
192 | 191 | eqcomd 2742 |
. . . . . . . 8
β’ (π β (π₯ β π β¦ ((π»βπ)βπ₯)) = (π»βπ)) |
193 | 192 | oveq2d 7373 |
. . . . . . 7
β’ (π β (π Dπ (π₯ β π β¦ ((π»βπ)βπ₯))) = (π Dπ (π»βπ))) |
194 | 193 | fveq1d 6844 |
. . . . . 6
β’ (π β ((π Dπ (π₯ β π β¦ ((π»βπ)βπ₯)))βπ) = ((π Dπ (π»βπ))βπ)) |
195 | 194 | adantr 481 |
. . . . 5
β’ ((π β§ π β (0...π½)) β ((π Dπ (π₯ β π β¦ ((π»βπ)βπ₯)))βπ) = ((π Dπ (π»βπ))βπ)) |
196 | 195 | feq1d 6653 |
. . . 4
β’ ((π β§ π β (0...π½)) β (((π Dπ (π₯ β π β¦ ((π»βπ)βπ₯)))βπ):πβΆβ β ((π Dπ (π»βπ))βπ):πβΆβ)) |
197 | 190, 196 | mpbird 256 |
. . 3
β’ ((π β§ π β (0...π½)) β ((π Dπ (π₯ β π β¦ ((π»βπ)βπ₯)))βπ):πβΆβ) |
198 | | fveq2 6842 |
. . . . . . . 8
β’ (π¦ = π₯ β ((π»βπ‘)βπ¦) = ((π»βπ‘)βπ₯)) |
199 | 198 | prodeq2ad 43823 |
. . . . . . 7
β’ (π¦ = π₯ β βπ‘ β π
((π»βπ‘)βπ¦) = βπ‘ β π
((π»βπ‘)βπ₯)) |
200 | 199 | cbvmptv 5218 |
. . . . . 6
β’ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)) = (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)) |
201 | 200 | oveq2i 7368 |
. . . . 5
β’ (π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦))) = (π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯))) |
202 | 201 | fveq1i 6843 |
. . . 4
β’ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ) = ((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ) |
203 | 202 | mpteq2i 5210 |
. . 3
β’ (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ)) = (π β (0...π½) β¦ ((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ)) |
204 | | fveq2 6842 |
. . . . . . 7
β’ (π¦ = π₯ β ((π»βπ)βπ¦) = ((π»βπ)βπ₯)) |
205 | 204 | cbvmptv 5218 |
. . . . . 6
β’ (π¦ β π β¦ ((π»βπ)βπ¦)) = (π₯ β π β¦ ((π»βπ)βπ₯)) |
206 | 205 | oveq2i 7368 |
. . . . 5
β’ (π Dπ (π¦ β π β¦ ((π»βπ)βπ¦))) = (π Dπ (π₯ β π β¦ ((π»βπ)βπ₯))) |
207 | 206 | fveq1i 6843 |
. . . 4
β’ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ) = ((π Dπ (π₯ β π β¦ ((π»βπ)βπ₯)))βπ) |
208 | 207 | mpteq2i 5210 |
. . 3
β’ (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ)) = (π β (0...π½) β¦ ((π Dπ (π₯ β π β¦ ((π»βπ)βπ₯)))βπ)) |
209 | 40, 41, 42, 35, 45, 46, 47, 174, 197, 203, 208 | dvnmul 44174 |
. 2
β’ (π β ((π Dπ (π₯ β π β¦ (βπ‘ β π
((π»βπ‘)βπ₯) Β· ((π»βπ)βπ₯))))βπ½) = (π₯ β π β¦ Ξ£π β (0...π½)((π½Cπ) Β· ((((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) Β· (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π))βπ₯))))) |
210 | 202 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π½)) β ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ) = ((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ)) |
211 | 154 | r19.21bi 3234 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...π)) β ((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
212 | 176, 170,
211 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π½)) β ((π Dπ (π₯ β π β¦ βπ‘ β π
((π»βπ‘)βπ₯)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
213 | 210, 212 | eqtrd 2776 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π½)) β ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
214 | 213 | mpteq2dva 5205 |
. . . . . . . . . . . 12
β’ (π β (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ)) = (π β (0...π½) β¦ (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))))) |
215 | | mptexg 7171 |
. . . . . . . . . . . . . 14
β’ (π β
((TopOpenββfld) βΎt π) β (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) β V) |
216 | 41, 215 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) β V) |
217 | 216 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π½)) β (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) β V) |
218 | 214, 217 | fvmpt2d 6961 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π½)) β ((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
219 | 218 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
220 | 219 | fveq1d 6844 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) = ((π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))βπ₯)) |
221 | 34 | adantr 481 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β π₯ β π) |
222 | 152 | an32s 650 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) β β) |
223 | | eqid 2736 |
. . . . . . . . . . 11
β’ (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) = (π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
224 | 223 | fvmpt2 6959 |
. . . . . . . . . 10
β’ ((π₯ β π β§ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) β β) β ((π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))βπ₯) = Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
225 | 221, 222,
224 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((π₯ β π β¦ Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))βπ₯) = Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
226 | 220, 225 | eqtrd 2776 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) = Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
227 | | fveq2 6842 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ) = ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ)) |
228 | 227 | cbvmptv 5218 |
. . . . . . . . . . . . . 14
β’ (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ)) = (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ)) |
229 | 228 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ)) = (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))) |
230 | 206, 193 | eqtrid 2788 |
. . . . . . . . . . . . . . 15
β’ (π β (π Dπ (π¦ β π β¦ ((π»βπ)βπ¦))) = (π Dπ (π»βπ))) |
231 | 230 | fveq1d 6844 |
. . . . . . . . . . . . . 14
β’ (π β ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ) = ((π Dπ (π»βπ))βπ)) |
232 | 231 | mpteq2dv 5207 |
. . . . . . . . . . . . 13
β’ (π β (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ)) = (π β (0...π½) β¦ ((π Dπ (π»βπ))βπ))) |
233 | 229, 232 | eqtrd 2776 |
. . . . . . . . . . . 12
β’ (π β (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ)) = (π β (0...π½) β¦ ((π Dπ (π»βπ))βπ))) |
234 | 233 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π½)) β (π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ)) = (π β (0...π½) β¦ ((π Dπ (π»βπ))βπ))) |
235 | | fveq2 6842 |
. . . . . . . . . . . 12
β’ (π = (π½ β π) β ((π Dπ (π»βπ))βπ) = ((π Dπ (π»βπ))β(π½ β π))) |
236 | 235 | adantl 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π½)) β§ π = (π½ β π)) β ((π Dπ (π»βπ))βπ) = ((π Dπ (π»βπ))β(π½ β π))) |
237 | | 0zd 12511 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β 0 β β€) |
238 | | elfzel2 13439 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β π½ β β€) |
239 | 238, 158 | zsubcld 12612 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β (π½ β π) β β€) |
240 | 237, 238,
239 | 3jca 1128 |
. . . . . . . . . . . . . 14
β’ (π β (0...π½) β (0 β β€ β§ π½ β β€ β§ (π½ β π) β β€)) |
241 | 238 | zred 12607 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π½) β π½ β β) |
242 | 75 | nn0red 12474 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π½) β π β β) |
243 | 241, 242 | subge0d 11745 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β (0 β€ (π½ β π) β π β€ π½)) |
244 | 166, 243 | mpbird 256 |
. . . . . . . . . . . . . 14
β’ (π β (0...π½) β 0 β€ (π½ β π)) |
245 | 241, 242 | subge02d 11747 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β (0 β€ π β (π½ β π) β€ π½)) |
246 | 160, 245 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β (0...π½) β (π½ β π) β€ π½) |
247 | 240, 244,
246 | jca32 516 |
. . . . . . . . . . . . 13
β’ (π β (0...π½) β ((0 β β€ β§ π½ β β€ β§ (π½ β π) β β€) β§ (0 β€ (π½ β π) β§ (π½ β π) β€ π½))) |
248 | 247 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π½)) β ((0 β β€ β§ π½ β β€ β§ (π½ β π) β β€) β§ (0 β€ (π½ β π) β§ (π½ β π) β€ π½))) |
249 | | elfz2 13431 |
. . . . . . . . . . . 12
β’ ((π½ β π) β (0...π½) β ((0 β β€ β§ π½ β β€ β§ (π½ β π) β β€) β§ (0 β€ (π½ β π) β§ (π½ β π) β€ π½))) |
250 | 248, 249 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π½)) β (π½ β π) β (0...π½)) |
251 | | fvex 6855 |
. . . . . . . . . . . 12
β’ ((π Dπ (π»βπ))β(π½ β π)) β V |
252 | 251 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π½)) β ((π Dπ (π»βπ))β(π½ β π)) β V) |
253 | 234, 236,
250, 252 | fvmptd 6955 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π½)) β ((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π)) = ((π Dπ (π»βπ))β(π½ β π))) |
254 | 253 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π)) = ((π Dπ (π»βπ))β(π½ β π))) |
255 | 254 | fveq1d 6844 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π))βπ₯) = (((π Dπ (π»βπ))β(π½ β π))βπ₯)) |
256 | 226, 255 | oveq12d 7375 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) Β· (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π))βπ₯)) = (Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯))) |
257 | 256 | oveq2d 7373 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((π½Cπ) Β· ((((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) Β· (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π))βπ₯))) = ((π½Cπ) Β· (Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)))) |
258 | 88 | adantlr 713 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((πΆβπ
)βπ) β Fin) |
259 | | ovex 7390 |
. . . . . . . . . . . 12
β’ (π½ β π) β V |
260 | | eleq1 2825 |
. . . . . . . . . . . . . 14
β’ (π = (π½ β π) β (π β (0...π½) β (π½ β π) β (0...π½))) |
261 | 260 | anbi2d 629 |
. . . . . . . . . . . . 13
β’ (π = (π½ β π) β ((π β§ π β (0...π½)) β (π β§ (π½ β π) β (0...π½)))) |
262 | 235 | feq1d 6653 |
. . . . . . . . . . . . 13
β’ (π = (π½ β π) β (((π Dπ (π»βπ))βπ):πβΆβ β ((π Dπ (π»βπ))β(π½ β π)):πβΆβ)) |
263 | 261, 262 | imbi12d 344 |
. . . . . . . . . . . 12
β’ (π = (π½ β π) β (((π β§ π β (0...π½)) β ((π Dπ (π»βπ))βπ):πβΆβ) β ((π β§ (π½ β π) β (0...π½)) β ((π Dπ (π»βπ))β(π½ β π)):πβΆβ))) |
264 | | eleq1 2825 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π β (0...π½) β π β (0...π½))) |
265 | 264 | anbi2d 629 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π β§ π β (0...π½)) β (π β§ π β (0...π½)))) |
266 | | fveq2 6842 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π Dπ (π»βπ))βπ) = ((π Dπ (π»βπ))βπ)) |
267 | 266 | feq1d 6653 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π Dπ (π»βπ))βπ):πβΆβ β ((π Dπ (π»βπ))βπ):πβΆβ)) |
268 | 265, 267 | imbi12d 344 |
. . . . . . . . . . . . 13
β’ (π = π β (((π β§ π β (0...π½)) β ((π Dπ (π»βπ))βπ):πβΆβ) β ((π β§ π β (0...π½)) β ((π Dπ (π»βπ))βπ):πβΆβ))) |
269 | 268, 190 | chvarvv 2002 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π½)) β ((π Dπ (π»βπ))βπ):πβΆβ) |
270 | 259, 263,
269 | vtocl 3518 |
. . . . . . . . . . 11
β’ ((π β§ (π½ β π) β (0...π½)) β ((π Dπ (π»βπ))β(π½ β π)):πβΆβ) |
271 | 176, 250,
270 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π½)) β ((π Dπ (π»βπ))β(π½ β π)):πβΆβ) |
272 | 271 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((π Dπ (π»βπ))β(π½ β π)):πβΆβ) |
273 | 272, 221 | ffvelcdmd 7036 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β (((π Dπ (π»βπ))β(π½ β π))βπ₯) β β) |
274 | | anass 469 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π½)) β§ π₯ β π) β (π β§ (π β (0...π½) β§ π₯ β π))) |
275 | | ancom 461 |
. . . . . . . . . . . . . 14
β’ ((π β (0...π½) β§ π₯ β π) β (π₯ β π β§ π β (0...π½))) |
276 | 275 | anbi2i 623 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (0...π½) β§ π₯ β π)) β (π β§ (π₯ β π β§ π β (0...π½)))) |
277 | | anass 469 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β (π β§ (π₯ β π β§ π β (0...π½)))) |
278 | 277 | bicomi 223 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π β§ π β (0...π½))) β ((π β§ π₯ β π) β§ π β (0...π½))) |
279 | 276, 278 | bitri 274 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (0...π½) β§ π₯ β π)) β ((π β§ π₯ β π) β§ π β (0...π½))) |
280 | 274, 279 | bitri 274 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π½)) β§ π₯ β π) β ((π β§ π₯ β π) β§ π β (0...π½))) |
281 | 280 | anbi1i 624 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β (((π β§ π₯ β π) β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ))) |
282 | 281 | imbi1i 349 |
. . . . . . . . 9
β’
(((((π β§ π β (0...π½)) β§ π₯ β π) β§ π β ((πΆβπ
)βπ)) β (((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) β β) β ((((π β§ π₯ β π) β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β (((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) β β)) |
283 | 151, 282 | mpbi 229 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β (((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) β β) |
284 | 258, 273,
283 | fsummulc1 15670 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β (Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)) = Ξ£π β ((πΆβπ
)βπ)((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯))) |
285 | 284 | oveq2d 7373 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((π½Cπ) Β· (Ξ£π β ((πΆβπ
)βπ)(((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯))) = ((π½Cπ) Β· Ξ£π β ((πΆβπ
)βπ)((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)))) |
286 | 176, 45 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π½)) β π½ β
β0) |
287 | 286, 159 | bccld 43539 |
. . . . . . . . 9
β’ ((π β§ π β (0...π½)) β (π½Cπ) β
β0) |
288 | 287 | nn0cnd 12475 |
. . . . . . . 8
β’ ((π β§ π β (0...π½)) β (π½Cπ) β β) |
289 | 288 | adantlr 713 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β (π½Cπ) β β) |
290 | 273 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π₯ β π) β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β (((π Dπ (π»βπ))β(π½ β π))βπ₯) β β) |
291 | 283, 290 | mulcld 11175 |
. . . . . . 7
β’ ((((π β§ π₯ β π) β§ π β (0...π½)) β§ π β ((πΆβπ
)βπ)) β ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)) β β) |
292 | 258, 289,
291 | fsummulc2 15669 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((π½Cπ) Β· Ξ£π β ((πΆβπ
)βπ)((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯))) = Ξ£π β ((πΆβπ
)βπ)((π½Cπ) Β· ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)))) |
293 | 257, 285,
292 | 3eqtrd 2780 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π β (0...π½)) β ((π½Cπ) Β· ((((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) Β· (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π))βπ₯))) = Ξ£π β ((πΆβπ
)βπ)((π½Cπ) Β· ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)))) |
294 | 293 | sumeq2dv 15588 |
. . . 4
β’ ((π β§ π₯ β π) β Ξ£π β (0...π½)((π½Cπ) Β· ((((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) Β· (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π))βπ₯))) = Ξ£π β (0...π½)Ξ£π β ((πΆβπ
)βπ)((π½Cπ) Β· ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)))) |
295 | | vex 3449 |
. . . . . . . 8
β’ π β V |
296 | | vex 3449 |
. . . . . . . 8
β’ π β V |
297 | 295, 296 | op1std 7931 |
. . . . . . 7
β’ (π = β¨π, πβ© β (1st βπ) = π) |
298 | 297 | oveq2d 7373 |
. . . . . 6
β’ (π = β¨π, πβ© β (π½C(1st βπ)) = (π½Cπ)) |
299 | 297 | fveq2d 6846 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β (!β(1st
βπ)) = (!βπ)) |
300 | 295, 296 | op2ndd 7932 |
. . . . . . . . . . . 12
β’ (π = β¨π, πβ© β (2nd βπ) = π) |
301 | 300 | fveq1d 6844 |
. . . . . . . . . . 11
β’ (π = β¨π, πβ© β ((2nd βπ)βπ‘) = (πβπ‘)) |
302 | 301 | fveq2d 6846 |
. . . . . . . . . 10
β’ (π = β¨π, πβ© β (!β((2nd
βπ)βπ‘)) = (!β(πβπ‘))) |
303 | 302 | prodeq2ad 43823 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β βπ‘ β π
(!β((2nd βπ)βπ‘)) = βπ‘ β π
(!β(πβπ‘))) |
304 | 299, 303 | oveq12d 7375 |
. . . . . . . 8
β’ (π = β¨π, πβ© β ((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) = ((!βπ) / βπ‘ β π
(!β(πβπ‘)))) |
305 | 301 | fveq2d 6846 |
. . . . . . . . . 10
β’ (π = β¨π, πβ© β ((π Dπ (π»βπ‘))β((2nd βπ)βπ‘)) = ((π Dπ (π»βπ‘))β(πβπ‘))) |
306 | 305 | fveq1d 6844 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β (((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯) = (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
307 | 306 | prodeq2ad 43823 |
. . . . . . . 8
β’ (π = β¨π, πβ© β βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯) = βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
308 | 304, 307 | oveq12d 7375 |
. . . . . . 7
β’ (π = β¨π, πβ© β (((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) = (((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
309 | 297 | oveq2d 7373 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β (π½ β (1st βπ)) = (π½ β π)) |
310 | 309 | fveq2d 6846 |
. . . . . . . 8
β’ (π = β¨π, πβ© β ((π Dπ (π»βπ))β(π½ β (1st βπ))) = ((π Dπ (π»βπ))β(π½ β π))) |
311 | 310 | fveq1d 6844 |
. . . . . . 7
β’ (π = β¨π, πβ© β (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯) = (((π Dπ (π»βπ))β(π½ β π))βπ₯)) |
312 | 308, 311 | oveq12d 7375 |
. . . . . 6
β’ (π = β¨π, πβ© β ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯)) = ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯))) |
313 | 298, 312 | oveq12d 7375 |
. . . . 5
β’ (π = β¨π, πβ© β ((π½C(1st βπ)) Β· ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯))) = ((π½Cπ) Β· ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)))) |
314 | | fzfid 13878 |
. . . . 5
β’ ((π β§ π₯ β π) β (0...π½) β Fin) |
315 | 289 | adantrr 715 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (π β (0...π½) β§ π β ((πΆβπ
)βπ))) β (π½Cπ) β β) |
316 | 291 | anasss 467 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ (π β (0...π½) β§ π β ((πΆβπ
)βπ))) β ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯)) β β) |
317 | 315, 316 | mulcld 11175 |
. . . . 5
β’ (((π β§ π₯ β π) β§ (π β (0...π½) β§ π β ((πΆβπ
)βπ))) β ((π½Cπ) Β· ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯))) β β) |
318 | 313, 314,
258, 317 | fsum2d 15656 |
. . . 4
β’ ((π β§ π₯ β π) β Ξ£π β (0...π½)Ξ£π β ((πΆβπ
)βπ)((π½Cπ) Β· ((((!βπ) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β π))βπ₯))) = Ξ£π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))((π½C(1st βπ)) Β· ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯)))) |
319 | | ovex 7390 |
. . . . . . . . 9
β’ (π½ β (πβπ)) β V |
320 | 296 | resex 5985 |
. . . . . . . . 9
β’ (π βΎ π
) β V |
321 | 319, 320 | op1std 7931 |
. . . . . . . 8
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (1st βπ) = (π½ β (πβπ))) |
322 | 321 | oveq2d 7373 |
. . . . . . 7
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (π½C(1st βπ)) = (π½C(π½ β (πβπ)))) |
323 | 321 | fveq2d 6846 |
. . . . . . . . . 10
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (!β(1st
βπ)) =
(!β(π½ β (πβπ)))) |
324 | 319, 320 | op2ndd 7932 |
. . . . . . . . . . . . 13
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (2nd βπ) = (π βΎ π
)) |
325 | 324 | fveq1d 6844 |
. . . . . . . . . . . 12
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β ((2nd βπ)βπ‘) = ((π βΎ π
)βπ‘)) |
326 | 325 | fveq2d 6846 |
. . . . . . . . . . 11
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (!β((2nd
βπ)βπ‘)) = (!β((π βΎ π
)βπ‘))) |
327 | 326 | prodeq2ad 43823 |
. . . . . . . . . 10
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β βπ‘ β π
(!β((2nd βπ)βπ‘)) = βπ‘ β π
(!β((π βΎ π
)βπ‘))) |
328 | 323, 327 | oveq12d 7375 |
. . . . . . . . 9
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β ((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) = ((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘)))) |
329 | 325 | fveq2d 6846 |
. . . . . . . . . . 11
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β ((π Dπ (π»βπ‘))β((2nd βπ)βπ‘)) = ((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))) |
330 | 329 | fveq1d 6844 |
. . . . . . . . . 10
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯) = (((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) |
331 | 330 | prodeq2ad 43823 |
. . . . . . . . 9
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯) = βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) |
332 | 328, 331 | oveq12d 7375 |
. . . . . . . 8
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) = (((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯))) |
333 | 321 | oveq2d 7373 |
. . . . . . . . . 10
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (π½ β (1st βπ)) = (π½ β (π½ β (πβπ)))) |
334 | 333 | fveq2d 6846 |
. . . . . . . . 9
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β ((π Dπ (π»βπ))β(π½ β (1st βπ))) = ((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))) |
335 | 334 | fveq1d 6844 |
. . . . . . . 8
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯) = (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯)) |
336 | 332, 335 | oveq12d 7375 |
. . . . . . 7
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯)) = ((((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯))) |
337 | 322, 336 | oveq12d 7375 |
. . . . . 6
β’ (π = β¨(π½ β (πβπ)), (π βΎ π
)β© β ((π½C(1st βπ)) Β· ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯))) = ((π½C(π½ β (πβπ))) Β· ((((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯)))) |
338 | | oveq2 7365 |
. . . . . . . . . . . . 13
β’ (π = (π
βͺ {π}) β ((0...π) βm π ) = ((0...π) βm (π
βͺ {π}))) |
339 | | rabeq 3421 |
. . . . . . . . . . . . 13
β’
(((0...π)
βm π ) =
((0...π) βm
(π
βͺ {π})) β {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β π (πβπ‘) = π}) |
340 | 338, 339 | syl 17 |
. . . . . . . . . . . 12
β’ (π = (π
βͺ {π}) β {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β π (πβπ‘) = π}) |
341 | | sumeq1 15573 |
. . . . . . . . . . . . . 14
β’ (π = (π
βͺ {π}) β Ξ£π‘ β π (πβπ‘) = Ξ£π‘ β (π
βͺ {π})(πβπ‘)) |
342 | 341 | eqeq1d 2738 |
. . . . . . . . . . . . 13
β’ (π = (π
βͺ {π}) β (Ξ£π‘ β π (πβπ‘) = π β Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π)) |
343 | 342 | rabbidv 3415 |
. . . . . . . . . . . 12
β’ (π = (π
βͺ {π}) β {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π}) |
344 | 340, 343 | eqtrd 2776 |
. . . . . . . . . . 11
β’ (π = (π
βͺ {π}) β {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π} = {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π}) |
345 | 344 | mpteq2dv 5207 |
. . . . . . . . . 10
β’ (π = (π
βͺ {π}) β (π β β0 β¦ {π β ((0...π) βm π ) β£ Ξ£π‘ β π (πβπ‘) = π}) = (π β β0 β¦ {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π})) |
346 | 23 | snssd 4769 |
. . . . . . . . . . . 12
β’ (π β {π} β π) |
347 | 4, 346 | unssd 4146 |
. . . . . . . . . . 11
β’ (π β (π
βͺ {π}) β π) |
348 | 3, 347 | ssexd 5281 |
. . . . . . . . . . . 12
β’ (π β (π
βͺ {π}) β V) |
349 | | elpwg 4563 |
. . . . . . . . . . . 12
β’ ((π
βͺ {π}) β V β ((π
βͺ {π}) β π« π β (π
βͺ {π}) β π)) |
350 | 348, 349 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((π
βͺ {π}) β π« π β (π
βͺ {π}) β π)) |
351 | 347, 350 | mpbird 256 |
. . . . . . . . . 10
β’ (π β (π
βͺ {π}) β π« π) |
352 | 63 | mptex 7173 |
. . . . . . . . . . 11
β’ (π β β0
β¦ {π β
((0...π) βm
(π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π}) β V |
353 | 352 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π β β0 β¦ {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π}) β V) |
354 | 48, 345, 351, 353 | fvmptd3 6971 |
. . . . . . . . 9
β’ (π β (πΆβ(π
βͺ {π})) = (π β β0 β¦ {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π})) |
355 | | oveq2 7365 |
. . . . . . . . . . . . 13
β’ (π = π½ β (0...π) = (0...π½)) |
356 | 355 | oveq1d 7372 |
. . . . . . . . . . . 12
β’ (π = π½ β ((0...π) βm (π
βͺ {π})) = ((0...π½) βm (π
βͺ {π}))) |
357 | | rabeq 3421 |
. . . . . . . . . . . 12
β’
(((0...π)
βm (π
βͺ
{π})) = ((0...π½) βm (π
βͺ {π})) β {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π} = {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π}) |
358 | 356, 357 | syl 17 |
. . . . . . . . . . 11
β’ (π = π½ β {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π} = {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π}) |
359 | | eqeq2 2748 |
. . . . . . . . . . . 12
β’ (π = π½ β (Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π β Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½)) |
360 | 359 | rabbidv 3415 |
. . . . . . . . . . 11
β’ (π = π½ β {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π} = {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½}) |
361 | 358, 360 | eqtrd 2776 |
. . . . . . . . . 10
β’ (π = π½ β {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π} = {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½}) |
362 | 361 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π = π½) β {π β ((0...π) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π} = {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½}) |
363 | | ovex 7390 |
. . . . . . . . . . 11
β’
((0...π½)
βm (π
βͺ
{π})) β
V |
364 | 363 | rabex 5289 |
. . . . . . . . . 10
β’ {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½} β V |
365 | 364 | a1i 11 |
. . . . . . . . 9
β’ (π β {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½} β V) |
366 | 354, 362,
45, 365 | fvmptd 6955 |
. . . . . . . 8
β’ (π β ((πΆβ(π
βͺ {π}))βπ½) = {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½}) |
367 | | fzfid 13878 |
. . . . . . . . . 10
β’ (π β (0...π½) β Fin) |
368 | | snfi 8988 |
. . . . . . . . . . . 12
β’ {π} β Fin |
369 | 368 | a1i 11 |
. . . . . . . . . . 11
β’ (π β {π} β Fin) |
370 | | unfi 9116 |
. . . . . . . . . . 11
β’ ((π
β Fin β§ {π} β Fin) β (π
βͺ {π}) β Fin) |
371 | 6, 369, 370 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β (π
βͺ {π}) β Fin) |
372 | | mapfi 9292 |
. . . . . . . . . 10
β’
(((0...π½) β Fin
β§ (π
βͺ {π}) β Fin) β
((0...π½) βm
(π
βͺ {π})) β Fin) |
373 | 367, 371,
372 | syl2anc 584 |
. . . . . . . . 9
β’ (π β ((0...π½) βm (π
βͺ {π})) β Fin) |
374 | | ssrab2 4037 |
. . . . . . . . . 10
β’ {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½} β ((0...π½) βm (π
βͺ {π})) |
375 | 374 | a1i 11 |
. . . . . . . . 9
β’ (π β {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½} β ((0...π½) βm (π
βͺ {π}))) |
376 | | ssfi 9117 |
. . . . . . . . 9
β’
((((0...π½)
βm (π
βͺ
{π})) β Fin β§
{π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½} β ((0...π½) βm (π
βͺ {π}))) β {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½} β Fin) |
377 | 373, 375,
376 | syl2anc 584 |
. . . . . . . 8
β’ (π β {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½} β Fin) |
378 | 366, 377 | eqeltrd 2837 |
. . . . . . 7
β’ (π β ((πΆβ(π
βͺ {π}))βπ½) β Fin) |
379 | 378 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((πΆβ(π
βͺ {π}))βπ½) β Fin) |
380 | | dvnprodlem2.d |
. . . . . . . 8
β’ π· = (π β ((πΆβ(π
βͺ {π}))βπ½) β¦ β¨(π½ β (πβπ)), (π βΎ π
)β©) |
381 | 48, 45, 380, 3, 23, 10, 347 | dvnprodlem1 44177 |
. . . . . . 7
β’ (π β π·:((πΆβ(π
βͺ {π}))βπ½)β1-1-ontoββͺ π β (0...π½)({π} Γ ((πΆβπ
)βπ))) |
382 | 381 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β π) β π·:((πΆβ(π
βͺ {π}))βπ½)β1-1-ontoββͺ π β (0...π½)({π} Γ ((πΆβπ
)βπ))) |
383 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π β ((πΆβ(π
βͺ {π}))βπ½)) |
384 | | opex 5421 |
. . . . . . . . 9
β’
β¨(π½ β
(πβπ)), (π βΎ π
)β© β V |
385 | 384 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β β¨(π½ β (πβπ)), (π βΎ π
)β© β V) |
386 | 380 | fvmpt2 6959 |
. . . . . . . 8
β’ ((π β ((πΆβ(π
βͺ {π}))βπ½) β§ β¨(π½ β (πβπ)), (π βΎ π
)β© β V) β (π·βπ) = β¨(π½ β (πβπ)), (π βΎ π
)β©) |
387 | 383, 385,
386 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π·βπ) = β¨(π½ β (πβπ)), (π βΎ π
)β©) |
388 | 387 | adantlr 713 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π·βπ) = β¨(π½ β (πβπ)), (π βΎ π
)β©) |
389 | 45 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β π½ β
β0) |
390 | | eliun 4958 |
. . . . . . . . . . . . . 14
β’ (π β βͺ π β (0...π½)({π} Γ ((πΆβπ
)βπ)) β βπ β (0...π½)π β ({π} Γ ((πΆβπ
)βπ))) |
391 | 390 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β βͺ π β (0...π½)({π} Γ ((πΆβπ
)βπ)) β βπ β (0...π½)π β ({π} Γ ((πΆβπ
)βπ))) |
392 | 391 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β βπ β (0...π½)π β ({π} Γ ((πΆβπ
)βπ))) |
393 | | nfv 1917 |
. . . . . . . . . . . . . 14
β’
β²ππ |
394 | | nfcv 2907 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
395 | | nfiu1 4988 |
. . . . . . . . . . . . . . 15
β’
β²πβͺ π β (0...π½)({π} Γ ((πΆβπ
)βπ)) |
396 | 394, 395 | nfel 2921 |
. . . . . . . . . . . . . 14
β’
β²π π β βͺ π β (0...π½)({π} Γ ((πΆβπ
)βπ)) |
397 | 393, 396 | nfan 1902 |
. . . . . . . . . . . . 13
β’
β²π(π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) |
398 | | nfv 1917 |
. . . . . . . . . . . . 13
β’
β²π(1st βπ) β (0...π½) |
399 | | xp1st 7953 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ({π} Γ ((πΆβπ
)βπ)) β (1st βπ) β {π}) |
400 | | elsni 4603 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ) β {π} β (1st βπ) = π) |
401 | 399, 400 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β ({π} Γ ((πΆβπ
)βπ)) β (1st βπ) = π) |
402 | 401 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β (1st βπ) = π) |
403 | | simpl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β π β (0...π½)) |
404 | 402, 403 | eqeltrd 2837 |
. . . . . . . . . . . . . . 15
β’ ((π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β (1st βπ) β (0...π½)) |
405 | 404 | ex 413 |
. . . . . . . . . . . . . 14
β’ (π β (0...π½) β (π β ({π} Γ ((πΆβπ
)βπ)) β (1st βπ) β (0...π½))) |
406 | 405 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π β (0...π½) β (π β ({π} Γ ((πΆβπ
)βπ)) β (1st βπ) β (0...π½)))) |
407 | 397, 398,
406 | rexlimd 3249 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (βπ β (0...π½)π β ({π} Γ ((πΆβπ
)βπ)) β (1st βπ) β (0...π½))) |
408 | 392, 407 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (1st βπ) β (0...π½)) |
409 | | elfzelz 13441 |
. . . . . . . . . . 11
β’
((1st βπ) β (0...π½) β (1st βπ) β
β€) |
410 | 408, 409 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (1st βπ) β
β€) |
411 | 389, 410 | bccld 43539 |
. . . . . . . . 9
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π½C(1st βπ)) β
β0) |
412 | 411 | nn0cnd 12475 |
. . . . . . . 8
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π½C(1st βπ)) β β) |
413 | 412 | adantlr 713 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π½C(1st βπ)) β β) |
414 | | elfznn0 13534 |
. . . . . . . . . . . . . 14
β’
((1st βπ) β (0...π½) β (1st βπ) β
β0) |
415 | 408, 414 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (1st βπ) β
β0) |
416 | 415 | faccld 14184 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (!β(1st
βπ)) β
β) |
417 | 416 | nncnd 12169 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (!β(1st
βπ)) β
β) |
418 | 417 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (!β(1st
βπ)) β
β) |
419 | 6 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β π
β Fin) |
420 | | nfv 1917 |
. . . . . . . . . . . . . . . 16
β’
β²π(2nd βπ):π
βΆ(0...π½) |
421 | 84, 82 | eqsstrd 3982 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0...π½)) β ((πΆβπ
)βπ) β ((0...π) βm π
)) |
422 | | ovex 7390 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(0...π½) β
V |
423 | 422 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0...π½) β (0...π½) β V) |
424 | | mapss 8827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((0...π½) β V
β§ (0...π) β
(0...π½)) β ((0...π) βm π
) β ((0...π½) βm π
)) |
425 | 423, 122,
424 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π½) β ((0...π) βm π
) β ((0...π½) βm π
)) |
426 | 425 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0...π½)) β ((0...π) βm π
) β ((0...π½) βm π
)) |
427 | 421, 426 | sstrd 3954 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0...π½)) β ((πΆβπ
)βπ) β ((0...π½) βm π
)) |
428 | 427 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β ((πΆβπ
)βπ) β ((0...π½) βm π
)) |
429 | | xp2nd 7954 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ({π} Γ ((πΆβπ
)βπ)) β (2nd βπ) β ((πΆβπ
)βπ)) |
430 | 429 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β (2nd βπ) β ((πΆβπ
)βπ)) |
431 | 428, 430 | sseldd 3945 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β (2nd βπ) β ((0...π½) βm π
)) |
432 | | elmapi 8787 |
. . . . . . . . . . . . . . . . . . 19
β’
((2nd βπ) β ((0...π½) βm π
) β (2nd βπ):π
βΆ(0...π½)) |
433 | 431, 432 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β (2nd βπ):π
βΆ(0...π½)) |
434 | 433 | 3exp 1119 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (0...π½) β (π β ({π} Γ ((πΆβπ
)βπ)) β (2nd βπ):π
βΆ(0...π½)))) |
435 | 434 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π β (0...π½) β (π β ({π} Γ ((πΆβπ
)βπ)) β (2nd βπ):π
βΆ(0...π½)))) |
436 | 397, 420,
435 | rexlimd 3249 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (βπ β (0...π½)π β ({π} Γ ((πΆβπ
)βπ)) β (2nd βπ):π
βΆ(0...π½))) |
437 | 392, 436 | mpd 15 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (2nd βπ):π
βΆ(0...π½)) |
438 | 437 | ffvelcdmda 7035 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β ((2nd βπ)βπ‘) β (0...π½)) |
439 | | elfznn0 13534 |
. . . . . . . . . . . . . . 15
β’
(((2nd βπ)βπ‘) β (0...π½) β ((2nd βπ)βπ‘) β
β0) |
440 | 439 | faccld 14184 |
. . . . . . . . . . . . . 14
β’
(((2nd βπ)βπ‘) β (0...π½) β (!β((2nd
βπ)βπ‘)) β
β) |
441 | 440 | nncnd 12169 |
. . . . . . . . . . . . 13
β’
(((2nd βπ)βπ‘) β (0...π½) β (!β((2nd
βπ)βπ‘)) β
β) |
442 | 438, 441 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β (!β((2nd
βπ)βπ‘)) β
β) |
443 | 419, 442 | fprodcl 15835 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β βπ‘ β π
(!β((2nd βπ)βπ‘)) β β) |
444 | 443 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β βπ‘ β π
(!β((2nd βπ)βπ‘)) β β) |
445 | 438, 440 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β (!β((2nd
βπ)βπ‘)) β
β) |
446 | | nnne0 12187 |
. . . . . . . . . . . . 13
β’
((!β((2nd βπ)βπ‘)) β β β
(!β((2nd βπ)βπ‘)) β 0) |
447 | 445, 446 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β (!β((2nd
βπ)βπ‘)) β 0) |
448 | 419, 442,
447 | fprodn0 15862 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β βπ‘ β π
(!β((2nd βπ)βπ‘)) β 0) |
449 | 448 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β βπ‘ β π
(!β((2nd βπ)βπ‘)) β 0) |
450 | 418, 444,
449 | divcld 11931 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β ((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) β β) |
451 | 7 | adantr 481 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β π
β Fin) |
452 | | simpll 765 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β π) |
453 | 452, 13 | sylancom 588 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β π‘ β π) |
454 | 452, 133 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β (0...π½) β (0...π)) |
455 | 454, 438 | sseldd 3945 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β ((2nd βπ)βπ‘) β (0...π)) |
456 | 452, 453,
455 | 3jca 1128 |
. . . . . . . . . . . . 13
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β (π β§ π‘ β π β§ ((2nd βπ)βπ‘) β (0...π))) |
457 | | eleq1 2825 |
. . . . . . . . . . . . . . . 16
β’ (π = ((2nd βπ)βπ‘) β (π β (0...π) β ((2nd βπ)βπ‘) β (0...π))) |
458 | 457 | 3anbi3d 1442 |
. . . . . . . . . . . . . . 15
β’ (π = ((2nd βπ)βπ‘) β ((π β§ π‘ β π β§ π β (0...π)) β (π β§ π‘ β π β§ ((2nd βπ)βπ‘) β (0...π)))) |
459 | | fveq2 6842 |
. . . . . . . . . . . . . . . 16
β’ (π = ((2nd βπ)βπ‘) β ((π Dπ (π»βπ‘))βπ) = ((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))) |
460 | 459 | feq1d 6653 |
. . . . . . . . . . . . . . 15
β’ (π = ((2nd βπ)βπ‘) β (((π Dπ (π»βπ‘))βπ):πβΆβ β ((π Dπ (π»βπ‘))β((2nd βπ)βπ‘)):πβΆβ)) |
461 | 458, 460 | imbi12d 344 |
. . . . . . . . . . . . . 14
β’ (π = ((2nd βπ)βπ‘) β (((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) β ((π β§ π‘ β π β§ ((2nd βπ)βπ‘) β (0...π)) β ((π Dπ (π»βπ‘))β((2nd βπ)βπ‘)):πβΆβ))) |
462 | 461, 145 | vtoclg 3525 |
. . . . . . . . . . . . 13
β’
(((2nd βπ)βπ‘) β (0...π½) β ((π β§ π‘ β π β§ ((2nd βπ)βπ‘) β (0...π)) β ((π Dπ (π»βπ‘))β((2nd βπ)βπ‘)):πβΆβ)) |
463 | 438, 456,
462 | sylc 65 |
. . . . . . . . . . . 12
β’ (((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β ((π Dπ (π»βπ‘))β((2nd βπ)βπ‘)):πβΆβ) |
464 | 463 | adantllr 717 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β ((π Dπ (π»βπ‘))β((2nd βπ)βπ‘)):πβΆβ) |
465 | 17 | adantlr 713 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β π₯ β π) |
466 | 464, 465 | ffvelcdmd 7036 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β§ π‘ β π
) β (((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯) β β) |
467 | 451, 466 | fprodcl 15835 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯) β β) |
468 | 450, 467 | mulcld 11175 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) β β) |
469 | | nfv 1917 |
. . . . . . . . . . . . 13
β’
β²π(π½ β (1st
βπ)) β
(0...π½) |
470 | | simp1 1136 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β π) |
471 | 404 | 3adant1 1130 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β (1st βπ) β (0...π½)) |
472 | | fznn0sub2 13548 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ) β (0...π½) β (π½ β (1st βπ)) β (0...π½)) |
473 | 472 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (1st
βπ) β (0...π½)) β (π½ β (1st βπ)) β (0...π½)) |
474 | 470, 471,
473 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...π½) β§ π β ({π} Γ ((πΆβπ
)βπ))) β (π½ β (1st βπ)) β (0...π½)) |
475 | 474 | 3exp 1119 |
. . . . . . . . . . . . . 14
β’ (π β (π β (0...π½) β (π β ({π} Γ ((πΆβπ
)βπ)) β (π½ β (1st βπ)) β (0...π½)))) |
476 | 475 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π β (0...π½) β (π β ({π} Γ ((πΆβπ
)βπ)) β (π½ β (1st βπ)) β (0...π½)))) |
477 | 397, 469,
476 | rexlimd 3249 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (βπ β (0...π½)π β ({π} Γ ((πΆβπ
)βπ)) β (π½ β (1st βπ)) β (0...π½))) |
478 | 392, 477 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π½ β (1st βπ)) β (0...π½)) |
479 | | simpl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β π) |
480 | 479, 23 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β π β π) |
481 | 479, 133 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (0...π½) β (0...π)) |
482 | 481, 478 | sseldd 3945 |
. . . . . . . . . . . 12
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π½ β (1st βπ)) β (0...π)) |
483 | 479, 480,
482 | 3jca 1128 |
. . . . . . . . . . 11
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (π β§ π β π β§ (π½ β (1st βπ)) β (0...π))) |
484 | | eleq1 2825 |
. . . . . . . . . . . . . 14
β’ (π = (π½ β (1st βπ)) β (π β (0...π) β (π½ β (1st βπ)) β (0...π))) |
485 | 484 | 3anbi3d 1442 |
. . . . . . . . . . . . 13
β’ (π = (π½ β (1st βπ)) β ((π β§ π β π β§ π β (0...π)) β (π β§ π β π β§ (π½ β (1st βπ)) β (0...π)))) |
486 | | fveq2 6842 |
. . . . . . . . . . . . . 14
β’ (π = (π½ β (1st βπ)) β ((π Dπ (π»βπ))βπ) = ((π Dπ (π»βπ))β(π½ β (1st βπ)))) |
487 | 486 | feq1d 6653 |
. . . . . . . . . . . . 13
β’ (π = (π½ β (1st βπ)) β (((π Dπ (π»βπ))βπ):πβΆβ β ((π Dπ (π»βπ))β(π½ β (1st βπ))):πβΆβ)) |
488 | 485, 487 | imbi12d 344 |
. . . . . . . . . . . 12
β’ (π = (π½ β (1st βπ)) β (((π β§ π β π β§ π β (0...π)) β ((π Dπ (π»βπ))βπ):πβΆβ) β ((π β§ π β π β§ (π½ β (1st βπ)) β (0...π)) β ((π Dπ (π»βπ))β(π½ β (1st βπ))):πβΆβ))) |
489 | | simp2 1137 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (0...π)) β π β π) |
490 | | id 22 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (0...π)) β (π β§ π β π β§ π β (0...π))) |
491 | 26 | 3anbi2d 1441 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β ((π β§ π‘ β π β§ π β (0...π)) β (π β§ π β π β§ π β (0...π)))) |
492 | 179 | fveq1d 6844 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = π β ((π Dπ (π»βπ‘))βπ) = ((π Dπ (π»βπ))βπ)) |
493 | 492 | feq1d 6653 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β (((π Dπ (π»βπ‘))βπ):πβΆβ β ((π Dπ (π»βπ))βπ):πβΆβ)) |
494 | 491, 493 | imbi12d 344 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β (((π β§ π‘ β π β§ π β (0...π)) β ((π Dπ (π»βπ‘))βπ):πβΆβ) β ((π β§ π β π β§ π β (0...π)) β ((π Dπ (π»βπ))βπ):πβΆβ))) |
495 | 494, 145 | vtoclg 3525 |
. . . . . . . . . . . . 13
β’ (π β π β ((π β§ π β π β§ π β (0...π)) β ((π Dπ (π»βπ))βπ):πβΆβ)) |
496 | 489, 490,
495 | sylc 65 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β (0...π)) β ((π Dπ (π»βπ))βπ):πβΆβ) |
497 | 488, 496 | vtoclg 3525 |
. . . . . . . . . . 11
β’ ((π½ β (1st
βπ)) β
(0...π½) β ((π β§ π β π β§ (π½ β (1st βπ)) β (0...π)) β ((π Dπ (π»βπ))β(π½ β (1st βπ))):πβΆβ)) |
498 | 478, 483,
497 | sylc 65 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β ((π Dπ (π»βπ))β(π½ β (1st βπ))):πβΆβ) |
499 | 498 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β ((π Dπ (π»βπ))β(π½ β (1st βπ))):πβΆβ) |
500 | 34 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β π₯ β π) |
501 | 499, 500 | ffvelcdmd 7036 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯) β β) |
502 | 468, 501 | mulcld 11175 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯)) β β) |
503 | 413, 502 | mulcld 11175 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))) β ((π½C(1st βπ)) Β· ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯))) β β) |
504 | 337, 379,
382, 388, 503 | fsumf1o 15608 |
. . . . 5
β’ ((π β§ π₯ β π) β Ξ£π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))((π½C(1st βπ)) Β· ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯))) = Ξ£π β ((πΆβ(π
βͺ {π}))βπ½)((π½C(π½ β (πβπ))) Β· ((((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯)))) |
505 | | simpl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π) |
506 | 366 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((πΆβ(π
βͺ {π}))βπ½) = {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½}) |
507 | 383, 506 | eleqtrd 2839 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π β {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½}) |
508 | 374 | sseli 3940 |
. . . . . . . . . . . . . . 15
β’ (π β {π β ((0...π½) βm (π
βͺ {π})) β£ Ξ£π‘ β (π
βͺ {π})(πβπ‘) = π½} β π β ((0...π½) βm (π
βͺ {π}))) |
509 | 507, 508 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π β ((0...π½) βm (π
βͺ {π}))) |
510 | | elmapi 8787 |
. . . . . . . . . . . . . 14
β’ (π β ((0...π½) βm (π
βͺ {π})) β π:(π
βͺ {π})βΆ(0...π½)) |
511 | 509, 510 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π:(π
βͺ {π})βΆ(0...π½)) |
512 | | snidg 4620 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β {π}) |
513 | 23, 512 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β {π}) |
514 | | elun2 4137 |
. . . . . . . . . . . . . . 15
β’ (π β {π} β π β (π
βͺ {π})) |
515 | 513, 514 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β (π
βͺ {π})) |
516 | 515 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π β (π
βͺ {π})) |
517 | 511, 516 | ffvelcdmd 7036 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (πβπ) β (0...π½)) |
518 | | 0zd 12511 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) β (0...π½)) β 0 β β€) |
519 | 124 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) β (0...π½)) β π½ β β€) |
520 | | fzssz 13443 |
. . . . . . . . . . . . . . . 16
β’
(0...π½) β
β€ |
521 | 520 | sseli 3940 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β (0...π½) β (πβπ) β β€) |
522 | 521 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβπ) β (0...π½)) β (πβπ) β β€) |
523 | 519, 522 | zsubcld 12612 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) β (0...π½)) β (π½ β (πβπ)) β β€) |
524 | | elfzle2 13445 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β (0...π½) β (πβπ) β€ π½) |
525 | 524 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβπ) β (0...π½)) β (πβπ) β€ π½) |
526 | 163 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (πβπ) β (0...π½)) β π½ β β) |
527 | 522 | zred 12607 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (πβπ) β (0...π½)) β (πβπ) β β) |
528 | 526, 527 | subge0d 11745 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβπ) β (0...π½)) β (0 β€ (π½ β (πβπ)) β (πβπ) β€ π½)) |
529 | 525, 528 | mpbird 256 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) β (0...π½)) β 0 β€ (π½ β (πβπ))) |
530 | | elfzle1 13444 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β (0...π½) β 0 β€ (πβπ)) |
531 | 530 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβπ) β (0...π½)) β 0 β€ (πβπ)) |
532 | 526, 527 | subge02d 11747 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβπ) β (0...π½)) β (0 β€ (πβπ) β (π½ β (πβπ)) β€ π½)) |
533 | 531, 532 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβπ) β (0...π½)) β (π½ β (πβπ)) β€ π½) |
534 | 518, 519,
523, 529, 533 | elfzd 13432 |
. . . . . . . . . . . 12
β’ ((π β§ (πβπ) β (0...π½)) β (π½ β (πβπ)) β (0...π½)) |
535 | 505, 517,
534 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π½ β (πβπ)) β (0...π½)) |
536 | | bcval2 14205 |
. . . . . . . . . . 11
β’ ((π½ β (πβπ)) β (0...π½) β (π½C(π½ β (πβπ))) = ((!βπ½) / ((!β(π½ β (π½ β (πβπ)))) Β· (!β(π½ β (πβπ)))))) |
537 | 535, 536 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π½C(π½ β (πβπ))) = ((!βπ½) / ((!β(π½ β (π½ β (πβπ)))) Β· (!β(π½ β (πβπ)))))) |
538 | 163 | recnd 11183 |
. . . . . . . . . . . . . . 15
β’ (π β π½ β β) |
539 | 538 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π½ β β) |
540 | | zsscn 12507 |
. . . . . . . . . . . . . . . . 17
β’ β€
β β |
541 | 520, 540 | sstri 3953 |
. . . . . . . . . . . . . . . 16
β’
(0...π½) β
β |
542 | 541 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (0...π½) β β) |
543 | 542, 517 | sseldd 3945 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (πβπ) β β) |
544 | 539, 543 | nncand 11517 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π½ β (π½ β (πβπ))) = (πβπ)) |
545 | 544 | fveq2d 6846 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(π½ β (π½ β (πβπ)))) = (!β(πβπ))) |
546 | 545 | oveq1d 7372 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((!β(π½ β (π½ β (πβπ)))) Β· (!β(π½ β (πβπ)))) = ((!β(πβπ)) Β· (!β(π½ β (πβπ))))) |
547 | 546 | oveq2d 7373 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((!βπ½) / ((!β(π½ β (π½ β (πβπ)))) Β· (!β(π½ β (πβπ))))) = ((!βπ½) / ((!β(πβπ)) Β· (!β(π½ β (πβπ)))))) |
548 | 45 | faccld 14184 |
. . . . . . . . . . . . . 14
β’ (π β (!βπ½) β β) |
549 | 548 | nncnd 12169 |
. . . . . . . . . . . . 13
β’ (π β (!βπ½) β β) |
550 | 549 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!βπ½) β β) |
551 | | elfznn0 13534 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β (0...π½) β (πβπ) β
β0) |
552 | 517, 551 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (πβπ) β
β0) |
553 | 552 | faccld 14184 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(πβπ)) β β) |
554 | 553 | nncnd 12169 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(πβπ)) β β) |
555 | | elfznn0 13534 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (πβπ)) β (0...π½) β (π½ β (πβπ)) β
β0) |
556 | 535, 555 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π½ β (πβπ)) β
β0) |
557 | 556 | faccld 14184 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(π½ β (πβπ))) β β) |
558 | 557 | nncnd 12169 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(π½ β (πβπ))) β β) |
559 | 553 | nnne0d 12203 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(πβπ)) β 0) |
560 | 557 | nnne0d 12203 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(π½ β (πβπ))) β 0) |
561 | 550, 554,
558, 559, 560 | divdiv1d 11962 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) / (!β(πβπ))) / (!β(π½ β (πβπ)))) = ((!βπ½) / ((!β(πβπ)) Β· (!β(π½ β (πβπ)))))) |
562 | 561 | eqcomd 2742 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((!βπ½) / ((!β(πβπ)) Β· (!β(π½ β (πβπ))))) = (((!βπ½) / (!β(πβπ))) / (!β(π½ β (πβπ))))) |
563 | 537, 547,
562 | 3eqtrd 2780 |
. . . . . . . . 9
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π½C(π½ β (πβπ))) = (((!βπ½) / (!β(πβπ))) / (!β(π½ β (πβπ))))) |
564 | 563 | adantlr 713 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π½C(π½ β (πβπ))) = (((!βπ½) / (!β(πβπ))) / (!β(π½ β (πβπ))))) |
565 | | fvres 6861 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ β π
β ((π βΎ π
)βπ‘) = (πβπ‘)) |
566 | 565 | fveq2d 6846 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β π
β (!β((π βΎ π
)βπ‘)) = (!β(πβπ‘))) |
567 | 566 | prodeq2i 15802 |
. . . . . . . . . . . . . . 15
β’
βπ‘ β
π
(!β((π βΎ π
)βπ‘)) = βπ‘ β π
(!β(πβπ‘)) |
568 | 567 | oveq2i 7368 |
. . . . . . . . . . . . . 14
β’
((!β(π½ β
(πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) = ((!β(π½ β (πβπ))) / βπ‘ β π
(!β(πβπ‘))) |
569 | 565 | fveq2d 6846 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β π
β ((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘)) = ((π Dπ (π»βπ‘))β(πβπ‘))) |
570 | 569 | fveq1d 6844 |
. . . . . . . . . . . . . . 15
β’ (π‘ β π
β (((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯) = (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
571 | 570 | prodeq2i 15802 |
. . . . . . . . . . . . . 14
β’
βπ‘ β
π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯) = βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) |
572 | 568, 571 | oveq12i 7369 |
. . . . . . . . . . . . 13
β’
(((!β(π½
β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) = (((!β(π½ β (πβπ))) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
573 | 572 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) = (((!β(π½ β (πβπ))) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
574 | 573 | adantlr 713 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) = (((!β(π½ β (πβπ))) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
575 | 558 | adantlr 713 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(π½ β (πβπ))) β β) |
576 | 505, 6 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π
β Fin) |
577 | 75 | ssriv 3948 |
. . . . . . . . . . . . . . . . . 18
β’
(0...π½) β
β0 |
578 | 577 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β (0...π½) β
β0) |
579 | 511 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β π:(π
βͺ {π})βΆ(0...π½)) |
580 | | elun1 4136 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β π
β π‘ β (π
βͺ {π})) |
581 | 580 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β π‘ β (π
βͺ {π})) |
582 | 579, 581 | ffvelcdmd 7036 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β (πβπ‘) β (0...π½)) |
583 | 578, 582 | sseldd 3945 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β (πβπ‘) β
β0) |
584 | 583 | faccld 14184 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β (!β(πβπ‘)) β β) |
585 | 584 | nncnd 12169 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β (!β(πβπ‘)) β β) |
586 | 576, 585 | fprodcl 15835 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β π
(!β(πβπ‘)) β β) |
587 | 586 | adantlr 713 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β π
(!β(πβπ‘)) β β) |
588 | 7 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π
β Fin) |
589 | 505 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β π) |
590 | 505, 13 | sylan 580 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β π‘ β π) |
591 | 589, 133 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β (0...π½) β (0...π)) |
592 | 591, 582 | sseldd 3945 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β (πβπ‘) β (0...π)) |
593 | 589, 590,
592, 146 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β ((π Dπ (π»βπ‘))β(πβπ‘)):πβΆβ) |
594 | 593 | adantllr 717 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β ((π Dπ (π»βπ‘))β(πβπ‘)):πβΆβ) |
595 | 17 | adantlr 713 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β π₯ β π) |
596 | 594, 595 | ffvelcdmd 7036 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β π
) β (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) β β) |
597 | 588, 596 | fprodcl 15835 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) β β) |
598 | 576, 584 | fprodnncl 15838 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β π
(!β(πβπ‘)) β β) |
599 | | nnne0 12187 |
. . . . . . . . . . . . . 14
β’
(βπ‘ β
π
(!β(πβπ‘)) β β β βπ‘ β π
(!β(πβπ‘)) β 0) |
600 | 598, 599 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β π
(!β(πβπ‘)) β 0) |
601 | 600 | adantlr 713 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β π
(!β(πβπ‘)) β 0) |
602 | 575, 587,
597, 601 | div32d 11954 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!β(π½ β (πβπ))) / βπ‘ β π
(!β(πβπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) = ((!β(π½ β (πβπ))) Β· (βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))))) |
603 | 574, 602 | eqtrd 2776 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) = ((!β(π½ β (πβπ))) Β· (βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))))) |
604 | 544 | fveq2d 6846 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((π Dπ (π»βπ))β(π½ β (π½ β (πβπ)))) = ((π Dπ (π»βπ))β(πβπ))) |
605 | 604 | fveq1d 6844 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯) = (((π Dπ (π»βπ))β(πβπ))βπ₯)) |
606 | 605 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯) = (((π Dπ (π»βπ))β(πβπ))βπ₯)) |
607 | 603, 606 | oveq12d 7375 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯)) = (((!β(π½ β (πβπ))) Β· (βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘)))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯))) |
608 | 597, 587,
601 | divcld 11931 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) β β) |
609 | 505, 23 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π β π) |
610 | 505, 133 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (0...π½) β (0...π)) |
611 | 610, 517 | sseldd 3945 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (πβπ) β (0...π)) |
612 | 505, 609,
611 | 3jca 1128 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π β§ π β π β§ (πβπ) β (0...π))) |
613 | | eleq1 2825 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β (π β (0...π) β (πβπ) β (0...π))) |
614 | 613 | 3anbi3d 1442 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β ((π β§ π β π β§ π β (0...π)) β (π β§ π β π β§ (πβπ) β (0...π)))) |
615 | | fveq2 6842 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β ((π Dπ (π»βπ))βπ) = ((π Dπ (π»βπ))β(πβπ))) |
616 | 615 | feq1d 6653 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (((π Dπ (π»βπ))βπ):πβΆβ β ((π Dπ (π»βπ))β(πβπ)):πβΆβ)) |
617 | 614, 616 | imbi12d 344 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (((π β§ π β π β§ π β (0...π)) β ((π Dπ (π»βπ))βπ):πβΆβ) β ((π β§ π β π β§ (πβπ) β (0...π)) β ((π Dπ (π»βπ))β(πβπ)):πβΆβ))) |
618 | 617, 496 | vtoclg 3525 |
. . . . . . . . . . . . 13
β’ ((πβπ) β (0...π½) β ((π β§ π β π β§ (πβπ) β (0...π)) β ((π Dπ (π»βπ))β(πβπ)):πβΆβ)) |
619 | 517, 612,
618 | sylc 65 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((π Dπ (π»βπ))β(πβπ)):πβΆβ) |
620 | 619 | adantlr 713 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((π Dπ (π»βπ))β(πβπ)):πβΆβ) |
621 | 34 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π₯ β π) |
622 | 620, 621 | ffvelcdmd 7036 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((π Dπ (π»βπ))β(πβπ))βπ₯) β β) |
623 | 575, 608,
622 | mulassd 11178 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!β(π½ β (πβπ))) Β· (βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘)))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)) = ((!β(π½ β (πβπ))) Β· ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)))) |
624 | 607, 623 | eqtrd 2776 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯)) = ((!β(π½ β (πβπ))) Β· ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)))) |
625 | 564, 624 | oveq12d 7375 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((π½C(π½ β (πβπ))) Β· ((((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯))) = ((((!βπ½) / (!β(πβπ))) / (!β(π½ β (πβπ)))) Β· ((!β(π½ β (πβπ))) Β· ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯))))) |
626 | 549 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!βπ½) β β) |
627 | 554 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(πβπ)) β β) |
628 | 559 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(πβπ)) β 0) |
629 | 626, 627,
628 | divcld 11931 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((!βπ½) / (!β(πβπ))) β β) |
630 | 608, 622 | mulcld 11175 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)) β β) |
631 | 560 | adantlr 713 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (!β(π½ β (πβπ))) β 0) |
632 | 629, 575,
630, 631 | dmmcand 43537 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((((!βπ½) / (!β(πβπ))) / (!β(π½ β (πβπ)))) Β· ((!β(π½ β (πβπ))) Β· ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)))) = (((!βπ½) / (!β(πβπ))) Β· ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)))) |
633 | 597, 622,
587, 601 | div23d 11968 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)) / βπ‘ β π
(!β(πβπ‘))) = ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯))) |
634 | 633 | eqcomd 2742 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)) = ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)) / βπ‘ β π
(!β(πβπ‘)))) |
635 | | nfv 1917 |
. . . . . . . . . . . . 13
β’
β²π‘((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) |
636 | | nfcv 2907 |
. . . . . . . . . . . . 13
β’
β²π‘(((π Dπ (π»βπ))β(πβπ))βπ₯) |
637 | 609 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π β π) |
638 | 11 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β Β¬ π β π
) |
639 | | fveq2 6842 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β (πβπ‘) = (πβπ)) |
640 | 179, 639 | fveq12d 6849 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β ((π Dπ (π»βπ‘))β(πβπ‘)) = ((π Dπ (π»βπ))β(πβπ))) |
641 | 640 | fveq1d 6844 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) = (((π Dπ (π»βπ))β(πβπ))βπ₯)) |
642 | 635, 636,
588, 637, 638, 596, 641, 622 | fprodsplitsn 15872 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) = (βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯))) |
643 | 642 | eqcomd 2742 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)) = βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) |
644 | 643 | oveq1d 7372 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)) / βπ‘ β π
(!β(πβπ‘))) = (βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘)))) |
645 | 634, 644 | eqtrd 2776 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯)) = (βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘)))) |
646 | 645 | oveq2d 7373 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) / (!β(πβπ))) Β· ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯))) = (((!βπ½) / (!β(πβπ))) Β· (βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))))) |
647 | 588, 368,
370 | sylancl 586 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π
βͺ {π}) β Fin) |
648 | 505 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β π) |
649 | 347 | sselda 3944 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β (π
βͺ {π})) β π‘ β π) |
650 | 649 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β π‘ β π) |
651 | 511, 610 | fssd 6686 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β π:(π
βͺ {π})βΆ(0...π)) |
652 | 651 | ffvelcdmda 7035 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β (πβπ‘) β (0...π)) |
653 | 648, 650,
652, 146 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β ((π Dπ (π»βπ‘))β(πβπ‘)):πβΆβ) |
654 | 653 | adantllr 717 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β ((π Dπ (π»βπ‘))β(πβπ‘)):πβΆβ) |
655 | 621 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β π₯ β π) |
656 | 654, 655 | ffvelcdmd 7036 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β (((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) β β) |
657 | 647, 656 | fprodcl 15835 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) β β) |
658 | 626, 627,
657, 587, 628, 601 | divmuldivd 11972 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) / (!β(πβπ))) Β· (βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘)))) = (((!βπ½) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) / ((!β(πβπ)) Β· βπ‘ β π
(!β(πβπ‘))))) |
659 | 554, 586 | mulcomd 11176 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((!β(πβπ)) Β· βπ‘ β π
(!β(πβπ‘))) = (βπ‘ β π
(!β(πβπ‘)) Β· (!β(πβπ)))) |
660 | | nfv 1917 |
. . . . . . . . . . . . . 14
β’
β²π‘(π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) |
661 | | nfcv 2907 |
. . . . . . . . . . . . . 14
β’
β²π‘(!β(πβπ)) |
662 | 505, 10 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β Β¬ π β π
) |
663 | 639 | fveq2d 6846 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β (!β(πβπ‘)) = (!β(πβπ))) |
664 | 660, 661,
576, 609, 662, 585, 663, 554 | fprodsplitsn 15872 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β (π
βͺ {π})(!β(πβπ‘)) = (βπ‘ β π
(!β(πβπ‘)) Β· (!β(πβπ)))) |
665 | 664 | eqcomd 2742 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (βπ‘ β π
(!β(πβπ‘)) Β· (!β(πβπ))) = βπ‘ β (π
βͺ {π})(!β(πβπ‘))) |
666 | 659, 665 | eqtrd 2776 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((!β(πβπ)) Β· βπ‘ β π
(!β(πβπ‘))) = βπ‘ β (π
βͺ {π})(!β(πβπ‘))) |
667 | 666 | oveq2d 7373 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) / ((!β(πβπ)) Β· βπ‘ β π
(!β(πβπ‘)))) = (((!βπ½) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) / βπ‘ β (π
βͺ {π})(!β(πβπ‘)))) |
668 | 667 | adantlr 713 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) / ((!β(πβπ)) Β· βπ‘ β π
(!β(πβπ‘)))) = (((!βπ½) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) / βπ‘ β (π
βͺ {π})(!β(πβπ‘)))) |
669 | 505, 371 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (π
βͺ {π}) β Fin) |
670 | 577 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β (0...π½) β
β0) |
671 | 511 | ffvelcdmda 7035 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β (πβπ‘) β (0...π½)) |
672 | 670, 671 | sseldd 3945 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β (πβπ‘) β
β0) |
673 | 672 | faccld 14184 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β (!β(πβπ‘)) β β) |
674 | 673 | nncnd 12169 |
. . . . . . . . . . . 12
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β (!β(πβπ‘)) β β) |
675 | 669, 674 | fprodcl 15835 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β (π
βͺ {π})(!β(πβπ‘)) β β) |
676 | 675 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β (π
βͺ {π})(!β(πβπ‘)) β β) |
677 | 673 | nnne0d 12203 |
. . . . . . . . . . . 12
β’ (((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β§ π‘ β (π
βͺ {π})) β (!β(πβπ‘)) β 0) |
678 | 669, 674,
677 | fprodn0 15862 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β (π
βͺ {π})(!β(πβπ‘)) β 0) |
679 | 678 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β βπ‘ β (π
βͺ {π})(!β(πβπ‘)) β 0) |
680 | 626, 657,
676, 679 | div23d 11968 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) = (((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
681 | | eqidd 2737 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) = (((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
682 | 668, 680,
681 | 3eqtrd 2780 |
. . . . . . . 8
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)) / ((!β(πβπ)) Β· βπ‘ β π
(!β(πβπ‘)))) = (((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
683 | 646, 658,
682 | 3eqtrd 2780 |
. . . . . . 7
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β (((!βπ½) / (!β(πβπ))) Β· ((βπ‘ β π
(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯) / βπ‘ β π
(!β(πβπ‘))) Β· (((π Dπ (π»βπ))β(πβπ))βπ₯))) = (((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
684 | 625, 632,
683 | 3eqtrd 2780 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π β ((πΆβ(π
βͺ {π}))βπ½)) β ((π½C(π½ β (πβπ))) Β· ((((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯))) = (((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
685 | 684 | sumeq2dv 15588 |
. . . . 5
β’ ((π β§ π₯ β π) β Ξ£π β ((πΆβ(π
βͺ {π}))βπ½)((π½C(π½ β (πβπ))) Β· ((((!β(π½ β (πβπ))) / βπ‘ β π
(!β((π βΎ π
)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((π βΎ π
)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (π½ β (πβπ))))βπ₯))) = Ξ£π β ((πΆβ(π
βͺ {π}))βπ½)(((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
686 | 504, 685 | eqtrd 2776 |
. . . 4
β’ ((π β§ π₯ β π) β Ξ£π β βͺ
π β (0...π½)({π} Γ ((πΆβπ
)βπ))((π½C(1st βπ)) Β· ((((!β(1st
βπ)) / βπ‘ β π
(!β((2nd βπ)βπ‘))) Β· βπ‘ β π
(((π Dπ (π»βπ‘))β((2nd βπ)βπ‘))βπ₯)) Β· (((π Dπ (π»βπ))β(π½ β (1st βπ)))βπ₯))) = Ξ£π β ((πΆβ(π
βͺ {π}))βπ½)(((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
687 | 294, 318,
686 | 3eqtrd 2780 |
. . 3
β’ ((π β§ π₯ β π) β Ξ£π β (0...π½)((π½Cπ) Β· ((((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) Β· (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π))βπ₯))) = Ξ£π β ((πΆβ(π
βͺ {π}))βπ½)(((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯))) |
688 | 687 | mpteq2dva 5205 |
. 2
β’ (π β (π₯ β π β¦ Ξ£π β (0...π½)((π½Cπ) Β· ((((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ βπ‘ β π
((π»βπ‘)βπ¦)))βπ))βπ)βπ₯) Β· (((π β (0...π½) β¦ ((π Dπ (π¦ β π β¦ ((π»βπ)βπ¦)))βπ))β(π½ β π))βπ₯)))) = (π₯ β π β¦ Ξ£π β ((πΆβ(π
βͺ {π}))βπ½)(((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |
689 | 39, 209, 688 | 3eqtrd 2780 |
1
β’ (π β ((π Dπ (π₯ β π β¦ βπ‘ β (π
βͺ {π})((π»βπ‘)βπ₯)))βπ½) = (π₯ β π β¦ Ξ£π β ((πΆβ(π
βͺ {π}))βπ½)(((!βπ½) / βπ‘ β (π
βͺ {π})(!β(πβπ‘))) Β· βπ‘ β (π
βͺ {π})(((π Dπ (π»βπ‘))β(πβπ‘))βπ₯)))) |