Step | Hyp | Ref
| Expression |
1 | | stoweidlem17.2 |
. . 3
β’ (π β π β β) |
2 | 1 | nnnn0d 12480 |
. 2
β’ (π β π β
β0) |
3 | | nn0uz 12812 |
. . . . 5
β’
β0 = (β€β₯β0) |
4 | 2, 3 | eleqtrdi 2848 |
. . . 4
β’ (π β π β
(β€β₯β0)) |
5 | | eluzfz2 13456 |
. . . 4
β’ (π β
(β€β₯β0) β π β (0...π)) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β π β (0...π)) |
7 | 6 | ancli 550 |
. 2
β’ (π β (π β§ π β (0...π))) |
8 | | eleq1 2826 |
. . . . 5
β’ (π = 0 β (π β (0...π) β 0 β (0...π))) |
9 | 8 | anbi2d 630 |
. . . 4
β’ (π = 0 β ((π β§ π β (0...π)) β (π β§ 0 β (0...π)))) |
10 | | oveq2 7370 |
. . . . . . 7
β’ (π = 0 β (0...π) = (0...0)) |
11 | 10 | sumeq1d 15593 |
. . . . . 6
β’ (π = 0 β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) = Ξ£π β (0...0)(πΈ Β· ((πβπ)βπ‘))) |
12 | 11 | mpteq2dv 5212 |
. . . . 5
β’ (π = 0 β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ Ξ£π β (0...0)(πΈ Β· ((πβπ)βπ‘)))) |
13 | 12 | eleq1d 2823 |
. . . 4
β’ (π = 0 β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄ β (π‘ β π β¦ Ξ£π β (0...0)(πΈ Β· ((πβπ)βπ‘))) β π΄)) |
14 | 9, 13 | imbi12d 345 |
. . 3
β’ (π = 0 β (((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β ((π β§ 0 β (0...π)) β (π‘ β π β¦ Ξ£π β (0...0)(πΈ Β· ((πβπ)βπ‘))) β π΄))) |
15 | | eleq1 2826 |
. . . . 5
β’ (π = π β (π β (0...π) β π β (0...π))) |
16 | 15 | anbi2d 630 |
. . . 4
β’ (π = π β ((π β§ π β (0...π)) β (π β§ π β (0...π)))) |
17 | | oveq2 7370 |
. . . . . . 7
β’ (π = π β (0...π) = (0...π)) |
18 | 17 | sumeq1d 15593 |
. . . . . 6
β’ (π = π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
19 | 18 | mpteq2dv 5212 |
. . . . 5
β’ (π = π β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))) |
20 | 19 | eleq1d 2823 |
. . . 4
β’ (π = π β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄ β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) |
21 | 16, 20 | imbi12d 345 |
. . 3
β’ (π = π β (((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄))) |
22 | | eleq1 2826 |
. . . . 5
β’ (π = (π + 1) β (π β (0...π) β (π + 1) β (0...π))) |
23 | 22 | anbi2d 630 |
. . . 4
β’ (π = (π + 1) β ((π β§ π β (0...π)) β (π β§ (π + 1) β (0...π)))) |
24 | | oveq2 7370 |
. . . . . . 7
β’ (π = (π + 1) β (0...π) = (0...(π + 1))) |
25 | 24 | sumeq1d 15593 |
. . . . . 6
β’ (π = (π + 1) β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) = Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) |
26 | 25 | mpteq2dv 5212 |
. . . . 5
β’ (π = (π + 1) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘)))) |
27 | 26 | eleq1d 2823 |
. . . 4
β’ (π = (π + 1) β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄ β (π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) β π΄)) |
28 | 23, 27 | imbi12d 345 |
. . 3
β’ (π = (π + 1) β (((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β ((π β§ (π + 1) β (0...π)) β (π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) β π΄))) |
29 | | eleq1 2826 |
. . . . 5
β’ (π = π β (π β (0...π) β π β (0...π))) |
30 | 29 | anbi2d 630 |
. . . 4
β’ (π = π β ((π β§ π β (0...π)) β (π β§ π β (0...π)))) |
31 | | oveq2 7370 |
. . . . . . 7
β’ (π = π β (0...π) = (0...π)) |
32 | 31 | sumeq1d 15593 |
. . . . . 6
β’ (π = π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
33 | 32 | mpteq2dv 5212 |
. . . . 5
β’ (π = π β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))) |
34 | 33 | eleq1d 2823 |
. . . 4
β’ (π = π β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄ β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) |
35 | 30, 34 | imbi12d 345 |
. . 3
β’ (π = π β (((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄))) |
36 | | 0z 12517 |
. . . . . . . . 9
β’ 0 β
β€ |
37 | | fzsn 13490 |
. . . . . . . . 9
β’ (0 β
β€ β (0...0) = {0}) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . 8
β’ (0...0) =
{0} |
39 | 38 | sumeq1i 15590 |
. . . . . . 7
β’
Ξ£π β
(0...0)(πΈ Β· ((πβπ)βπ‘)) = Ξ£π β {0} (πΈ Β· ((πβπ)βπ‘)) |
40 | 39 | mpteq2i 5215 |
. . . . . 6
β’ (π‘ β π β¦ Ξ£π β (0...0)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ Ξ£π β {0} (πΈ Β· ((πβπ)βπ‘))) |
41 | | stoweidlem17.1 |
. . . . . . 7
β’
β²π‘π |
42 | | stoweidlem17.7 |
. . . . . . . . . . 11
β’ (π β πΈ β β) |
43 | 42 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β πΈ β β) |
44 | 43 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β πΈ β β) |
45 | | stoweidlem17.3 |
. . . . . . . . . . . . 13
β’ (π β π:(0...π)βΆπ΄) |
46 | | nnz 12527 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β€) |
47 | | nngt0 12191 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β 0 <
π) |
48 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β |
49 | | nnre 12167 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β) |
50 | | ltle 11250 |
. . . . . . . . . . . . . . . . . . 19
β’ ((0
β β β§ π
β β) β (0 < π β 0 β€ π)) |
51 | 48, 49, 50 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (0 <
π β 0 β€ π)) |
52 | 47, 51 | mpd 15 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β 0 β€
π) |
53 | 46, 52 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π β β€ β§ 0 β€
π)) |
54 | 1, 53 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π β β€ β§ 0 β€ π)) |
55 | 36 | eluz1i 12778 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β0) β (π β β€ β§ 0 β€ π)) |
56 | 54, 55 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (π β π β
(β€β₯β0)) |
57 | | eluzfz1 13455 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β 0 β (0...π)) |
59 | 45, 58 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (π β (πβ0) β π΄) |
60 | | feq1 6654 |
. . . . . . . . . . . . . 14
β’ (π = (πβ0) β (π:πβΆβ β (πβ0):πβΆβ)) |
61 | 60 | imbi2d 341 |
. . . . . . . . . . . . 13
β’ (π = (πβ0) β ((π β π:πβΆβ) β (π β (πβ0):πβΆβ))) |
62 | | stoweidlem17.8 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β π:πβΆβ) |
63 | 62 | expcom 415 |
. . . . . . . . . . . . 13
β’ (π β π΄ β (π β π:πβΆβ)) |
64 | 61, 63 | vtoclga 3537 |
. . . . . . . . . . . 12
β’ ((πβ0) β π΄ β (π β (πβ0):πβΆβ)) |
65 | 59, 64 | mpcom 38 |
. . . . . . . . . . 11
β’ (π β (πβ0):πβΆβ) |
66 | 65 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β ((πβ0)βπ‘) β β) |
67 | 66 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((πβ0)βπ‘) β β) |
68 | 44, 67 | mulcld 11182 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πΈ Β· ((πβ0)βπ‘)) β β) |
69 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = 0 β (πβπ) = (πβ0)) |
70 | 69 | fveq1d 6849 |
. . . . . . . . . 10
β’ (π = 0 β ((πβπ)βπ‘) = ((πβ0)βπ‘)) |
71 | 70 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = 0 β (πΈ Β· ((πβπ)βπ‘)) = (πΈ Β· ((πβ0)βπ‘))) |
72 | 71 | sumsn 15638 |
. . . . . . . 8
β’ ((0
β β€ β§ (πΈ
Β· ((πβ0)βπ‘)) β β) β Ξ£π β {0} (πΈ Β· ((πβπ)βπ‘)) = (πΈ Β· ((πβ0)βπ‘))) |
73 | 36, 68, 72 | sylancr 588 |
. . . . . . 7
β’ ((π β§ π‘ β π) β Ξ£π β {0} (πΈ Β· ((πβπ)βπ‘)) = (πΈ Β· ((πβ0)βπ‘))) |
74 | 41, 73 | mpteq2da 5208 |
. . . . . 6
β’ (π β (π‘ β π β¦ Ξ£π β {0} (πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ (πΈ Β· ((πβ0)βπ‘)))) |
75 | 40, 74 | eqtrid 2789 |
. . . . 5
β’ (π β (π‘ β π β¦ Ξ£π β (0...0)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ (πΈ Β· ((πβ0)βπ‘)))) |
76 | | stoweidlem17.5 |
. . . . . 6
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
77 | | stoweidlem17.6 |
. . . . . 6
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
78 | 41, 76, 77, 62, 42, 59 | stoweidlem2 44317 |
. . . . 5
β’ (π β (π‘ β π β¦ (πΈ Β· ((πβ0)βπ‘))) β π΄) |
79 | 75, 78 | eqeltrd 2838 |
. . . 4
β’ (π β (π‘ β π β¦ Ξ£π β (0...0)(πΈ Β· ((πβπ)βπ‘))) β π΄) |
80 | 79 | adantr 482 |
. . 3
β’ ((π β§ 0 β (0...π)) β (π‘ β π β¦ Ξ£π β (0...0)(πΈ Β· ((πβπ)βπ‘))) β π΄) |
81 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
β’ (π = π‘ β πΈ = πΈ) |
82 | 81 | cbvmptv 5223 |
. . . . . . . . . . . . . 14
β’ (π β π β¦ πΈ) = (π‘ β π β¦ πΈ) |
83 | 82 | eqcomi 2746 |
. . . . . . . . . . . . 13
β’ (π‘ β π β¦ πΈ) = (π β π β¦ πΈ) |
84 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β π‘ β π) |
85 | 83, 81, 84, 43 | fvmptd3 6976 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β π) β ((π‘ β π β¦ πΈ)βπ‘) = πΈ) |
86 | 85 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘)) = (πΈ Β· ((πβ(π + 1))βπ‘))) |
87 | 41, 86 | mpteq2da 5208 |
. . . . . . . . . 10
β’ (π β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘))) = (π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))) |
88 | 87 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π + 1) β (0...π)) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘))) = (π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))) |
89 | 45 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ (π + 1) β (0...π)) β (πβ(π + 1)) β π΄) |
90 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β§ (π + 1) β (0...π)) β π) |
91 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = πΈ β π₯ = πΈ) |
92 | 91 | mpteq2dv 5212 |
. . . . . . . . . . . . . . 15
β’ (π₯ = πΈ β (π‘ β π β¦ π₯) = (π‘ β π β¦ πΈ)) |
93 | 92 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π₯ = πΈ β ((π‘ β π β¦ π₯) β π΄ β (π‘ β π β¦ πΈ) β π΄)) |
94 | 93 | imbi2d 341 |
. . . . . . . . . . . . 13
β’ (π₯ = πΈ β ((π β (π‘ β π β¦ π₯) β π΄) β (π β (π‘ β π β¦ πΈ) β π΄))) |
95 | 77 | expcom 415 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (π β (π‘ β π β¦ π₯) β π΄)) |
96 | 94, 95 | vtoclga 3537 |
. . . . . . . . . . . 12
β’ (πΈ β β β (π β (π‘ β π β¦ πΈ) β π΄)) |
97 | 42, 96 | mpcom 38 |
. . . . . . . . . . 11
β’ (π β (π‘ β π β¦ πΈ) β π΄) |
98 | 97 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π + 1) β (0...π)) β (π‘ β π β¦ πΈ) β π΄) |
99 | | fveq1 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβ(π + 1)) β (πβπ‘) = ((πβ(π + 1))βπ‘)) |
100 | 99 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = (πβ(π + 1)) β (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘)) = (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘))) |
101 | 100 | mpteq2dv 5212 |
. . . . . . . . . . . . . 14
β’ (π = (πβ(π + 1)) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) = (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘)))) |
102 | 101 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = (πβ(π + 1)) β ((π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄ β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘))) β π΄)) |
103 | 102 | imbi2d 341 |
. . . . . . . . . . . 12
β’ (π = (πβ(π + 1)) β (((π β§ (π‘ β π β¦ πΈ) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄) β ((π β§ (π‘ β π β¦ πΈ) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘))) β π΄))) |
104 | 82 | eleq1i 2829 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β¦ πΈ) β π΄ β (π‘ β π β¦ πΈ) β π΄) |
105 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π β π β¦ πΈ) β (πβπ‘) = ((π β π β¦ πΈ)βπ‘)) |
106 | 82 | fveq1i 6848 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π β¦ πΈ)βπ‘) = ((π‘ β π β¦ πΈ)βπ‘) |
107 | 105, 106 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π β π β¦ πΈ) β (πβπ‘) = ((π‘ β π β¦ πΈ)βπ‘)) |
108 | 107 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β π β¦ πΈ) β ((πβπ‘) Β· (πβπ‘)) = (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) |
109 | 108 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β π β¦ πΈ) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) = (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘)))) |
110 | 109 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π β π β¦ πΈ) β ((π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄ β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄)) |
111 | 110 | imbi2d 341 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π β π β¦ πΈ) β (((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) β ((π β§ π β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄))) |
112 | 76 | 3com12 1124 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π΄ β§ π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
113 | 112 | 3expib 1123 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β ((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄)) |
114 | 111, 113 | vtoclga 3537 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β¦ πΈ) β π΄ β ((π β§ π β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄)) |
115 | 104, 114 | sylbir 234 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β π β¦ πΈ) β π΄ β ((π β§ π β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄)) |
116 | 115 | 3impib 1117 |
. . . . . . . . . . . . . 14
β’ (((π‘ β π β¦ πΈ) β π΄ β§ π β§ π β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄) |
117 | 116 | 3com13 1125 |
. . . . . . . . . . . . 13
β’ ((π β π΄ β§ π β§ (π‘ β π β¦ πΈ) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄) |
118 | 117 | 3expib 1123 |
. . . . . . . . . . . 12
β’ (π β π΄ β ((π β§ (π‘ β π β¦ πΈ) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· (πβπ‘))) β π΄)) |
119 | 103, 118 | vtoclga 3537 |
. . . . . . . . . . 11
β’ ((πβ(π + 1)) β π΄ β ((π β§ (π‘ β π β¦ πΈ) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘))) β π΄)) |
120 | 119 | 3impib 1117 |
. . . . . . . . . 10
β’ (((πβ(π + 1)) β π΄ β§ π β§ (π‘ β π β¦ πΈ) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘))) β π΄) |
121 | 89, 90, 98, 120 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (π + 1) β (0...π)) β (π‘ β π β¦ (((π‘ β π β¦ πΈ)βπ‘) Β· ((πβ(π + 1))βπ‘))) β π΄) |
122 | 88, 121 | eqeltrrd 2839 |
. . . . . . . 8
β’ ((π β§ (π + 1) β (0...π)) β (π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘))) β π΄) |
123 | 122 | ad2antll 728 |
. . . . . . 7
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β (π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘))) β π΄) |
124 | | simprrl 780 |
. . . . . . 7
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β π) |
125 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π β β0) |
126 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π) |
127 | 1 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π β β) |
128 | 127 | nnnn0d 12480 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π β
β0) |
129 | | nn0re 12429 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
130 | 129 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π β β) |
131 | | peano2nn0 12460 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 1) β
β0) |
132 | 131 | nn0red 12481 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π + 1) β
β) |
133 | 132 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β (π + 1) β β) |
134 | 1 | nnred 12175 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
135 | 134 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π β β) |
136 | | lep1 12003 |
. . . . . . . . . . . . 13
β’ (π β β β π β€ (π + 1)) |
137 | 125, 129,
136 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π β€ (π + 1)) |
138 | | elfzle2 13452 |
. . . . . . . . . . . . 13
β’ ((π + 1) β (0...π) β (π + 1) β€ π) |
139 | 138 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β (π + 1) β€ π) |
140 | 130, 133,
135, 137, 139 | letrd 11319 |
. . . . . . . . . . 11
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π β€ π) |
141 | | elfz2nn0 13539 |
. . . . . . . . . . 11
β’ (π β (0...π) β (π β β0 β§ π β β0
β§ π β€ π)) |
142 | 125, 128,
140, 141 | syl3anbrc 1344 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β π β (0...π)) |
143 | 125, 126,
142 | jca32 517 |
. . . . . . . . 9
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β (π β β0 β§ (π β§ π β (0...π)))) |
144 | 143 | adantl 483 |
. . . . . . . 8
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β (π β β0 β§ (π β§ π β (0...π)))) |
145 | | pm3.31 451 |
. . . . . . . . 9
β’ ((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β ((π β β0 β§ (π β§ π β (0...π))) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) |
146 | 145 | adantr 482 |
. . . . . . . 8
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β ((π β β0 β§ (π β§ π β (0...π))) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) |
147 | 144, 146 | mpd 15 |
. . . . . . 7
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) |
148 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π‘ β ((πβ(π + 1))βπ) = ((πβ(π + 1))βπ‘)) |
149 | 148 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = π‘ β (πΈ Β· ((πβ(π + 1))βπ)) = (πΈ Β· ((πβ(π + 1))βπ‘))) |
150 | 149 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) = (π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘))) |
151 | 150 | eleq1i 2829 |
. . . . . . . . 9
β’ ((π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) β π΄ β (π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘))) β π΄) |
152 | | fveq1 6846 |
. . . . . . . . . . . . . . 15
β’ (π = (π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) β (πβπ‘) = ((π β π β¦ (πΈ Β· ((πβ(π + 1))βπ)))βπ‘)) |
153 | 150 | fveq1i 6848 |
. . . . . . . . . . . . . . 15
β’ ((π β π β¦ (πΈ Β· ((πβ(π + 1))βπ)))βπ‘) = ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘) |
154 | 152, 153 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π = (π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) β (πβπ‘) = ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘)) |
155 | 154 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = (π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) β (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘)) = (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) |
156 | 155 | mpteq2dv 5212 |
. . . . . . . . . . . 12
β’ (π = (π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) = (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘)))) |
157 | 156 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π = (π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) β ((π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄ β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) β π΄)) |
158 | 157 | imbi2d 341 |
. . . . . . . . . 10
β’ (π = (π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) β (((π β§ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄) β ((π β§ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) β π΄))) |
159 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π‘ β ((πβπ)βπ) = ((πβπ)βπ‘)) |
160 | 159 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π = π‘ β (πΈ Β· ((πβπ)βπ)) = (πΈ Β· ((πβπ)βπ‘))) |
161 | 160 | sumeq2sdv 15596 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
162 | 161 | cbvmptv 5223 |
. . . . . . . . . . . . . . 15
β’ (π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) = (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
163 | 162 | eleq1i 2829 |
. . . . . . . . . . . . . 14
β’ ((π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β π΄ β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) |
164 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β (πβπ‘) = ((π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)))βπ‘)) |
165 | 162 | fveq1i 6848 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)))βπ‘) = ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) |
166 | 164, 165 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β (πβπ‘) = ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘)) |
167 | 166 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β ((πβπ‘) + (πβπ‘)) = (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) |
168 | 167 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) = (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘)))) |
169 | 168 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π = (π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β ((π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄ β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄)) |
170 | 169 | imbi2d 341 |
. . . . . . . . . . . . . . 15
β’ (π = (π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β (((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) β ((π β§ π β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄))) |
171 | | stoweidlem17.4 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
172 | 171 | 3com12 1124 |
. . . . . . . . . . . . . . . 16
β’ ((π β π΄ β§ π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
173 | 172 | 3expib 1123 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β ((π β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄)) |
174 | 170, 173 | vtoclga 3537 |
. . . . . . . . . . . . . 14
β’ ((π β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β π΄ β ((π β§ π β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄)) |
175 | 163, 174 | sylbir 234 |
. . . . . . . . . . . . 13
β’ ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄ β ((π β§ π β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄)) |
176 | 175 | 3impib 1117 |
. . . . . . . . . . . 12
β’ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄ β§ π β§ π β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄) |
177 | 176 | 3com13 1125 |
. . . . . . . . . . 11
β’ ((π β π΄ β§ π β§ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄) |
178 | 177 | 3expib 1123 |
. . . . . . . . . 10
β’ (π β π΄ β ((π β§ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πβπ‘))) β π΄)) |
179 | 158, 178 | vtoclga 3537 |
. . . . . . . . 9
β’ ((π β π β¦ (πΈ Β· ((πβ(π + 1))βπ))) β π΄ β ((π β§ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) β π΄)) |
180 | 151, 179 | sylbir 234 |
. . . . . . . 8
β’ ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘))) β π΄ β ((π β§ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) β π΄)) |
181 | 180 | 3impib 1117 |
. . . . . . 7
β’ (((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘))) β π΄ β§ π β§ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) β π΄) |
182 | 123, 124,
147, 181 | syl3anc 1372 |
. . . . . 6
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) β π΄) |
183 | | 3anass 1096 |
. . . . . . . . 9
β’ ((π β β0
β§ π β§ (π + 1) β (0...π)) β (π β β0 β§ (π β§ (π + 1) β (0...π)))) |
184 | 183 | biimpri 227 |
. . . . . . . 8
β’ ((π β β0
β§ (π β§ (π + 1) β (0...π))) β (π β β0 β§ π β§ (π + 1) β (0...π))) |
185 | 184 | adantl 483 |
. . . . . . 7
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β (π β β0 β§ π β§ (π + 1) β (0...π))) |
186 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π‘ π β
β0 |
187 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π‘(π + 1) β (0...π) |
188 | 186, 41, 187 | nf3an 1905 |
. . . . . . . . 9
β’
β²π‘(π β β0
β§ π β§ (π + 1) β (0...π)) |
189 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β π‘ β π) |
190 | | fzfid 13885 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (0...π) β Fin) |
191 | 42 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π β§ (π + 1) β (0...π)) β πΈ β β) |
192 | 191 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β πΈ β β) |
193 | 192 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...π)) β πΈ β β) |
194 | | fzelp1 13500 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β π β (0...(π + 1))) |
195 | 194 | anim2i 618 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...π)) β (((π β β0 β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...(π + 1)))) |
196 | | an32 645 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...(π + 1))) β (((π β β0 β§ π β§ (π + 1) β (0...π)) β§ π β (0...(π + 1))) β§ π‘ β π)) |
197 | 195, 196 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...π)) β (((π β β0 β§ π β§ (π + 1) β (0...π)) β§ π β (0...(π + 1))) β§ π‘ β π)) |
198 | 45 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ π β§ (π + 1) β (0...π)) β π:(0...π)βΆπ΄) |
199 | 198 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π β (0...(π + 1))) β π:(0...π)βΆπ΄) |
200 | | elfzuz3 13445 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π + 1) β (0...π) β π β (β€β₯β(π + 1))) |
201 | | fzss2 13488 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β(π + 1)) β (0...(π + 1)) β (0...π)) |
202 | 200, 201 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π + 1) β (0...π) β (0...(π + 1)) β (0...π)) |
203 | 202 | sselda 3949 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π + 1) β (0...π) β§ π β (0...(π + 1))) β π β (0...π)) |
204 | 203 | 3ad2antl3 1188 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π β (0...(π + 1))) β π β (0...π)) |
205 | 199, 204 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π β (0...(π + 1))) β (πβπ) β π΄) |
206 | | simpl2 1193 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π β (0...(π + 1))) β π) |
207 | | feq1 6654 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβπ) β (π:πβΆβ β (πβπ):πβΆβ)) |
208 | 207 | imbi2d 341 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β ((π β π:πβΆβ) β (π β (πβπ):πβΆβ))) |
209 | 208, 63 | vtoclga 3537 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ) β π΄ β (π β (πβπ):πβΆβ)) |
210 | 205, 206,
209 | sylc 65 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π β (0...(π + 1))) β (πβπ):πβΆβ) |
211 | 210 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . 15
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π β (0...(π + 1))) β§ π‘ β π) β ((πβπ)βπ‘) β β) |
212 | 197, 211 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...π)) β ((πβπ)βπ‘) β β) |
213 | 193, 212 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...π)) β (πΈ Β· ((πβπ)βπ‘)) β β) |
214 | 190, 213 | fsumrecl 15626 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) β β) |
215 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
216 | 215 | fvmpt2 6964 |
. . . . . . . . . . . 12
β’ ((π‘ β π β§ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) β β) β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
217 | 189, 214,
216 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
218 | 217 | oveq1d 7377 |
. . . . . . . . . 10
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πΈ Β· ((πβ(π + 1))βπ‘))) = (Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) + (πΈ Β· ((πβ(π + 1))βπ‘)))) |
219 | | 3simpc 1151 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π β§ (π + 1) β (0...π)) β (π β§ (π + 1) β (0...π))) |
220 | 219 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (π β§ (π + 1) β (0...π))) |
221 | | feq1 6654 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ(π + 1)) β (π:πβΆβ β (πβ(π + 1)):πβΆβ)) |
222 | 221 | imbi2d 341 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ(π + 1)) β ((π β π:πβΆβ) β (π β (πβ(π + 1)):πβΆβ))) |
223 | 222, 63 | vtoclga 3537 |
. . . . . . . . . . . . . . . 16
β’ ((πβ(π + 1)) β π΄ β (π β (πβ(π + 1)):πβΆβ)) |
224 | 89, 90, 223 | sylc 65 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π + 1) β (0...π)) β (πβ(π + 1)):πβΆβ) |
225 | 220, 224 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (πβ(π + 1)):πβΆβ) |
226 | 225, 189 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β ((πβ(π + 1))βπ‘) β β) |
227 | 192, 226 | remulcld 11192 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (πΈ Β· ((πβ(π + 1))βπ‘)) β β) |
228 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘))) = (π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘))) |
229 | 228 | fvmpt2 6964 |
. . . . . . . . . . . 12
β’ ((π‘ β π β§ (πΈ Β· ((πβ(π + 1))βπ‘)) β β) β ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘) = (πΈ Β· ((πβ(π + 1))βπ‘))) |
230 | 189, 227,
229 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘) = (πΈ Β· ((πβ(π + 1))βπ‘))) |
231 | 230 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘)) = (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + (πΈ Β· ((πβ(π + 1))βπ‘)))) |
232 | | elfzuz 13444 |
. . . . . . . . . . . . . 14
β’ ((π + 1) β (0...π) β (π + 1) β
(β€β₯β0)) |
233 | 232 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π β§ (π + 1) β (0...π)) β (π + 1) β
(β€β₯β0)) |
234 | 233 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (π + 1) β
(β€β₯β0)) |
235 | 192 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...(π + 1))) β πΈ β β) |
236 | 211 | an32s 651 |
. . . . . . . . . . . . 13
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...(π + 1))) β ((πβπ)βπ‘) β β) |
237 | | remulcl 11143 |
. . . . . . . . . . . . . 14
β’ ((πΈ β β β§ ((πβπ)βπ‘) β β) β (πΈ Β· ((πβπ)βπ‘)) β β) |
238 | 237 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((πΈ β β β§ ((πβπ)βπ‘) β β) β (πΈ Β· ((πβπ)βπ‘)) β β) |
239 | 235, 236,
238 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β§ π β (0...(π + 1))) β (πΈ Β· ((πβπ)βπ‘)) β β) |
240 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
241 | 240 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β ((πβπ)βπ‘) = ((πβ(π + 1))βπ‘)) |
242 | 241 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (πΈ Β· ((πβπ)βπ‘)) = (πΈ Β· ((πβ(π + 1))βπ‘))) |
243 | 234, 239,
242 | fsumm1 15643 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘)) = (Ξ£π β (0...((π + 1) β 1))(πΈ Β· ((πβπ)βπ‘)) + (πΈ Β· ((πβ(π + 1))βπ‘)))) |
244 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β π β
β) |
245 | 244 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ π β§ (π + 1) β (0...π)) β π β β) |
246 | 245 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β π β β) |
247 | | 1cnd 11157 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β 1 β β) |
248 | 246, 247 | pncand 11520 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β ((π + 1) β 1) = π) |
249 | 248 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (0...((π + 1) β 1)) = (0...π)) |
250 | 249 | sumeq1d 15593 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β Ξ£π β (0...((π + 1) β 1))(πΈ Β· ((πβπ)βπ‘)) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
251 | 250 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β (Ξ£π β (0...((π + 1) β 1))(πΈ Β· ((πβπ)βπ‘)) + (πΈ Β· ((πβ(π + 1))βπ‘))) = (Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) + (πΈ Β· ((πβ(π + 1))βπ‘)))) |
252 | 243, 251 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘)) = (Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) + (πΈ Β· ((πβ(π + 1))βπ‘)))) |
253 | 218, 231,
252 | 3eqtr4rd 2788 |
. . . . . . . . 9
β’ (((π β β0
β§ π β§ (π + 1) β (0...π)) β§ π‘ β π) β Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘)) = (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) |
254 | 188, 253 | mpteq2da 5208 |
. . . . . . . 8
β’ ((π β β0
β§ π β§ (π + 1) β (0...π)) β (π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘)))) |
255 | 254 | eleq1d 2823 |
. . . . . . 7
β’ ((π β β0
β§ π β§ (π + 1) β (0...π)) β ((π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) β π΄ β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) β π΄)) |
256 | 185, 255 | syl 17 |
. . . . . 6
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β ((π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) β π΄ β (π‘ β π β¦ (((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) + ((π‘ β π β¦ (πΈ Β· ((πβ(π + 1))βπ‘)))βπ‘))) β π΄)) |
257 | 182, 256 | mpbird 257 |
. . . . 5
β’ (((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β§ (π β β0 β§ (π β§ (π + 1) β (0...π)))) β (π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) β π΄) |
258 | 257 | exp32 422 |
. . . 4
β’ ((π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) β (π β β0 β ((π β§ (π + 1) β (0...π)) β (π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) β π΄))) |
259 | 258 | pm2.86i 110 |
. . 3
β’ (π β β0
β (((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) β ((π β§ (π + 1) β (0...π)) β (π‘ β π β¦ Ξ£π β (0...(π + 1))(πΈ Β· ((πβπ)βπ‘))) β π΄))) |
260 | 14, 21, 28, 35, 80, 259 | nn0ind 12605 |
. 2
β’ (π β β0
β ((π β§ π β (0...π)) β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄)) |
261 | 2, 7, 260 | sylc 65 |
1
β’ (π β (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) β π΄) |