Step | Hyp | Ref
| Expression |
1 | | stoweidlem32.2 |
. . 3
β’ π = (π‘ β π β¦ (π Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
2 | | stoweidlem32.1 |
. . . 4
β’
β²π‘π |
3 | | stoweidlem32.3 |
. . . . . . . . . 10
β’ πΉ = (π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) |
4 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π‘ = π β ((πΊβπ)βπ‘) = ((πΊβπ)βπ )) |
5 | 4 | sumeq2sdv 15594 |
. . . . . . . . . . 11
β’ (π‘ = π β Ξ£π β (1...π)((πΊβπ)βπ‘) = Ξ£π β (1...π)((πΊβπ)βπ )) |
6 | 5 | cbvmptv 5219 |
. . . . . . . . . 10
β’ (π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) = (π β π β¦ Ξ£π β (1...π)((πΊβπ)βπ )) |
7 | 3, 6 | eqtri 2761 |
. . . . . . . . 9
β’ πΉ = (π β π β¦ Ξ£π β (1...π)((πΊβπ)βπ )) |
8 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π‘ β ((πΊβπ)βπ ) = ((πΊβπ)βπ‘)) |
9 | 8 | sumeq2sdv 15594 |
. . . . . . . . 9
β’ (π = π‘ β Ξ£π β (1...π)((πΊβπ)βπ ) = Ξ£π β (1...π)((πΊβπ)βπ‘)) |
10 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β π‘ β π) |
11 | | fzfid 13884 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (1...π) β Fin) |
12 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β π) |
13 | | stoweidlem32.7 |
. . . . . . . . . . . . . 14
β’ (π β πΊ:(1...π)βΆπ΄) |
14 | 13 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πΊβπ) β π΄) |
15 | | eleq1 2822 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πΊβπ) β (π β π΄ β (πΊβπ) β π΄)) |
16 | 15 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = (πΊβπ) β ((π β§ π β π΄) β (π β§ (πΊβπ) β π΄))) |
17 | | feq1 6650 |
. . . . . . . . . . . . . . . 16
β’ (π = (πΊβπ) β (π:πβΆβ β (πΊβπ):πβΆβ)) |
18 | 16, 17 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = (πΊβπ) β (((π β§ π β π΄) β π:πβΆβ) β ((π β§ (πΊβπ) β π΄) β (πΊβπ):πβΆβ))) |
19 | | stoweidlem32.11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π:πβΆβ) |
20 | 18, 19 | vtoclg 3524 |
. . . . . . . . . . . . . 14
β’ ((πΊβπ) β π΄ β ((π β§ (πΊβπ) β π΄) β (πΊβπ):πβΆβ)) |
21 | 14, 20 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β ((π β§ (πΊβπ) β π΄) β (πΊβπ):πβΆβ)) |
22 | 12, 14, 21 | mp2and 698 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (πΊβπ):πβΆβ) |
23 | 22 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π) β§ π β (1...π)) β (πΊβπ):πβΆβ) |
24 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π) β§ π β (1...π)) β π‘ β π) |
25 | 23, 24 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((πΊβπ)βπ‘) β β) |
26 | 11, 25 | fsumrecl 15624 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β Ξ£π β (1...π)((πΊβπ)βπ‘) β β) |
27 | 7, 9, 10, 26 | fvmptd3 6972 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πΉβπ‘) = Ξ£π β (1...π)((πΊβπ)βπ‘)) |
28 | 27, 26 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
29 | 28 | recnd 11188 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
30 | | stoweidlem32.4 |
. . . . . . . . . 10
β’ π» = (π‘ β π β¦ π) |
31 | | eqidd 2734 |
. . . . . . . . . . 11
β’ (π = π‘ β π = π) |
32 | 31 | cbvmptv 5219 |
. . . . . . . . . 10
β’ (π β π β¦ π) = (π‘ β π β¦ π) |
33 | 30, 32 | eqtr4i 2764 |
. . . . . . . . 9
β’ π» = (π β π β¦ π) |
34 | | stoweidlem32.6 |
. . . . . . . . . 10
β’ (π β π β β) |
35 | 34 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β π β β) |
36 | 33, 31, 10, 35 | fvmptd3 6972 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π»βπ‘) = π) |
37 | 36, 35 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (π»βπ‘) β β) |
38 | 37 | recnd 11188 |
. . . . . 6
β’ ((π β§ π‘ β π) β (π»βπ‘) β β) |
39 | 29, 38 | mulcomd 11181 |
. . . . 5
β’ ((π β§ π‘ β π) β ((πΉβπ‘) Β· (π»βπ‘)) = ((π»βπ‘) Β· (πΉβπ‘))) |
40 | 36, 27 | oveq12d 7376 |
. . . . 5
β’ ((π β§ π‘ β π) β ((π»βπ‘) Β· (πΉβπ‘)) = (π Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
41 | 39, 40 | eqtr2d 2774 |
. . . 4
β’ ((π β§ π‘ β π) β (π Β· Ξ£π β (1...π)((πΊβπ)βπ‘)) = ((πΉβπ‘) Β· (π»βπ‘))) |
42 | 2, 41 | mpteq2da 5204 |
. . 3
β’ (π β (π‘ β π β¦ (π Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) = (π‘ β π β¦ ((πΉβπ‘) Β· (π»βπ‘)))) |
43 | 1, 42 | eqtrid 2785 |
. 2
β’ (π β π = (π‘ β π β¦ ((πΉβπ‘) Β· (π»βπ‘)))) |
44 | | stoweidlem32.5 |
. . . 4
β’ (π β π β β) |
45 | | stoweidlem32.8 |
. . . 4
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
46 | 2, 3, 44, 13, 45, 19 | stoweidlem20 44347 |
. . 3
β’ (π β πΉ β π΄) |
47 | | stoweidlem32.10 |
. . . . . 6
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
48 | 47 | stoweidlem4 44331 |
. . . . 5
β’ ((π β§ π β β) β (π‘ β π β¦ π) β π΄) |
49 | 34, 48 | mpdan 686 |
. . . 4
β’ (π β (π‘ β π β¦ π) β π΄) |
50 | 30, 49 | eqeltrid 2838 |
. . 3
β’ (π β π» β π΄) |
51 | | nfmpt1 5214 |
. . . . . 6
β’
β²π‘(π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) |
52 | 3, 51 | nfcxfr 2902 |
. . . . 5
β’
β²π‘πΉ |
53 | 52 | nfeq2 2921 |
. . . 4
β’
β²π‘ π = πΉ |
54 | | nfmpt1 5214 |
. . . . . 6
β’
β²π‘(π‘ β π β¦ π) |
55 | 30, 54 | nfcxfr 2902 |
. . . . 5
β’
β²π‘π» |
56 | 55 | nfeq2 2921 |
. . . 4
β’
β²π‘ π = π» |
57 | | stoweidlem32.9 |
. . . 4
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
58 | 53, 56, 57 | stoweidlem6 44333 |
. . 3
β’ ((π β§ πΉ β π΄ β§ π» β π΄) β (π‘ β π β¦ ((πΉβπ‘) Β· (π»βπ‘))) β π΄) |
59 | 46, 50, 58 | mpd3an23 1464 |
. 2
β’ (π β (π‘ β π β¦ ((πΉβπ‘) Β· (π»βπ‘))) β π΄) |
60 | 43, 59 | eqeltrd 2834 |
1
β’ (π β π β π΄) |