Step | Hyp | Ref
| Expression |
1 | | ssidd 4004 |
. . 3
β’ (π β β β
β) |
2 | | coeeu.4 |
. . . 4
β’ (π β π β
β0) |
3 | | coeeu.5 |
. . . 4
β’ (π β π β
β0) |
4 | 2, 3 | nn0addcld 12540 |
. . 3
β’ (π β (π + π) β
β0) |
5 | | subcl 11463 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β (π₯ β π¦) β β) |
6 | 5 | adantl 480 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ β π¦) β β) |
7 | | coeeu.2 |
. . . . . . 7
β’ (π β π΄ β (β βm
β0)) |
8 | | cnex 11193 |
. . . . . . . 8
β’ β
β V |
9 | | nn0ex 12482 |
. . . . . . . 8
β’
β0 β V |
10 | 8, 9 | elmap 8867 |
. . . . . . 7
β’ (π΄ β (β
βm β0) β π΄:β0βΆβ) |
11 | 7, 10 | sylib 217 |
. . . . . 6
β’ (π β π΄:β0βΆβ) |
12 | | coeeu.3 |
. . . . . . 7
β’ (π β π΅ β (β βm
β0)) |
13 | 8, 9 | elmap 8867 |
. . . . . . 7
β’ (π΅ β (β
βm β0) β π΅:β0βΆβ) |
14 | 12, 13 | sylib 217 |
. . . . . 6
β’ (π β π΅:β0βΆβ) |
15 | 9 | a1i 11 |
. . . . . 6
β’ (π β β0 β
V) |
16 | | inidm 4217 |
. . . . . 6
β’
(β0 β© β0) =
β0 |
17 | 6, 11, 14, 15, 15, 16 | off 7690 |
. . . . 5
β’ (π β (π΄ βf β π΅):β0βΆβ) |
18 | 8, 9 | elmap 8867 |
. . . . 5
β’ ((π΄ βf β
π΅) β (β
βm β0) β (π΄ βf β π΅):β0βΆβ) |
19 | 17, 18 | sylibr 233 |
. . . 4
β’ (π β (π΄ βf β π΅) β (β
βm β0)) |
20 | | 0cn 11210 |
. . . . . . 7
β’ 0 β
β |
21 | | snssi 4810 |
. . . . . . 7
β’ (0 β
β β {0} β β) |
22 | 20, 21 | ax-mp 5 |
. . . . . 6
β’ {0}
β β |
23 | | ssequn2 4182 |
. . . . . 6
β’ ({0}
β β β (β βͺ {0}) = β) |
24 | 22, 23 | mpbi 229 |
. . . . 5
β’ (β
βͺ {0}) = β |
25 | 24 | oveq1i 7421 |
. . . 4
β’ ((β
βͺ {0}) βm β0) = (β
βm β0) |
26 | 19, 25 | eleqtrrdi 2842 |
. . 3
β’ (π β (π΄ βf β π΅) β ((β βͺ {0})
βm β0)) |
27 | 4 | nn0red 12537 |
. . . . . . . 8
β’ (π β (π + π) β β) |
28 | | nn0re 12485 |
. . . . . . . 8
β’ (π β β0
β π β
β) |
29 | | ltnle 11297 |
. . . . . . . 8
β’ (((π + π) β β β§ π β β) β ((π + π) < π β Β¬ π β€ (π + π))) |
30 | 27, 28, 29 | syl2an 594 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π + π) < π β Β¬ π β€ (π + π))) |
31 | 11 | ffnd 6717 |
. . . . . . . . . . 11
β’ (π β π΄ Fn β0) |
32 | 14 | ffnd 6717 |
. . . . . . . . . . 11
β’ (π β π΅ Fn β0) |
33 | | eqidd 2731 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (π΄βπ) = (π΄βπ)) |
34 | | eqidd 2731 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (π΅βπ) = (π΅βπ)) |
35 | 31, 32, 15, 15, 16, 33, 34 | ofval 7683 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((π΄ βf β
π΅)βπ) = ((π΄βπ) β (π΅βπ))) |
36 | 35 | adantrr 713 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§ (π + π) < π)) β ((π΄ βf β π΅)βπ) = ((π΄βπ) β (π΅βπ))) |
37 | 2 | nn0red 12537 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
38 | 37 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ (π + π) < π)) β π β β) |
39 | 27 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ (π + π) < π)) β (π + π) β β) |
40 | 28 | adantl 480 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β π β
β) |
41 | 40 | adantrr 713 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ (π + π) < π)) β π β β) |
42 | 2 | nn0cnd 12538 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
43 | 3 | nn0cnd 12538 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
44 | 42, 43 | addcomd 11420 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π + π) = (π + π)) |
45 | | nn0uz 12868 |
. . . . . . . . . . . . . . . . . . . 20
β’
β0 = (β€β₯β0) |
46 | 3, 45 | eleqtrdi 2841 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β
(β€β₯β0)) |
47 | 2 | nn0zd 12588 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β€) |
48 | | eluzadd 12855 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β
(β€β₯β0) β§ π β β€) β (π + π) β (β€β₯β(0 +
π))) |
49 | 46, 47, 48 | syl2anc 582 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π + π) β (β€β₯β(0 +
π))) |
50 | 44, 49 | eqeltrd 2831 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + π) β (β€β₯β(0 +
π))) |
51 | 42 | addlidd 11419 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0 + π) = π) |
52 | 51 | fveq2d 6894 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β(0 + π)) = (β€β₯βπ)) |
53 | 50, 52 | eleqtrd 2833 |
. . . . . . . . . . . . . . . 16
β’ (π β (π + π) β (β€β₯βπ)) |
54 | | eluzle 12839 |
. . . . . . . . . . . . . . . 16
β’ ((π + π) β (β€β₯βπ) β π β€ (π + π)) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β€ (π + π)) |
56 | 55 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ (π + π) < π)) β π β€ (π + π)) |
57 | | simprr 769 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ (π + π) < π)) β (π + π) < π) |
58 | 38, 39, 41, 56, 57 | lelttrd 11376 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ (π + π) < π)) β π < π) |
59 | 38, 41 | ltnled 11365 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ (π + π) < π)) β (π < π β Β¬ π β€ π)) |
60 | 58, 59 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β0 β§ (π + π) < π)) β Β¬ π β€ π) |
61 | | coeeu.6 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄ β
(β€β₯β(π + 1))) = {0}) |
62 | | plyco0 25941 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π΄ β
(β€β₯β(π + 1))) = {0} β βπ β β0
((π΄βπ) β 0 β π β€ π))) |
63 | 2, 11, 62 | syl2anc 582 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π΄ β
(β€β₯β(π + 1))) = {0} β βπ β β0
((π΄βπ) β 0 β π β€ π))) |
64 | 61, 63 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β β0 ((π΄βπ) β 0 β π β€ π)) |
65 | 64 | r19.21bi 3246 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β ((π΄βπ) β 0 β π β€ π)) |
66 | 65 | adantrr 713 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ (π + π) < π)) β ((π΄βπ) β 0 β π β€ π)) |
67 | 66 | necon1bd 2956 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β0 β§ (π + π) < π)) β (Β¬ π β€ π β (π΄βπ) = 0)) |
68 | 60, 67 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ (π β β0 β§ (π + π) < π)) β (π΄βπ) = 0) |
69 | 3 | nn0red 12537 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
70 | 69 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ (π + π) < π)) β π β β) |
71 | 2, 45 | eleqtrdi 2841 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β
(β€β₯β0)) |
72 | 3 | nn0zd 12588 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β€) |
73 | | eluzadd 12855 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β
(β€β₯β0) β§ π β β€) β (π + π) β (β€β₯β(0 +
π))) |
74 | 71, 72, 73 | syl2anc 582 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + π) β (β€β₯β(0 +
π))) |
75 | 43 | addlidd 11419 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0 + π) = π) |
76 | 75 | fveq2d 6894 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β(0 + π)) = (β€β₯βπ)) |
77 | 74, 76 | eleqtrd 2833 |
. . . . . . . . . . . . . . . 16
β’ (π β (π + π) β (β€β₯βπ)) |
78 | | eluzle 12839 |
. . . . . . . . . . . . . . . 16
β’ ((π + π) β (β€β₯βπ) β π β€ (π + π)) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β€ (π + π)) |
80 | 79 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β0 β§ (π + π) < π)) β π β€ (π + π)) |
81 | 70, 39, 41, 80, 57 | lelttrd 11376 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ (π + π) < π)) β π < π) |
82 | 70, 41 | ltnled 11365 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ (π + π) < π)) β (π < π β Β¬ π β€ π)) |
83 | 81, 82 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β0 β§ (π + π) < π)) β Β¬ π β€ π) |
84 | | coeeu.7 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΅ β
(β€β₯β(π + 1))) = {0}) |
85 | | plyco0 25941 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β0
β§ π΅:β0βΆβ) β
((π΅ β
(β€β₯β(π + 1))) = {0} β βπ β β0
((π΅βπ) β 0 β π β€ π))) |
86 | 3, 14, 85 | syl2anc 582 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π΅ β
(β€β₯β(π + 1))) = {0} β βπ β β0
((π΅βπ) β 0 β π β€ π))) |
87 | 84, 86 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β β0 ((π΅βπ) β 0 β π β€ π)) |
88 | 87 | r19.21bi 3246 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β ((π΅βπ) β 0 β π β€ π)) |
89 | 88 | adantrr 713 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β0 β§ (π + π) < π)) β ((π΅βπ) β 0 β π β€ π)) |
90 | 89 | necon1bd 2956 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β0 β§ (π + π) < π)) β (Β¬ π β€ π β (π΅βπ) = 0)) |
91 | 83, 90 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ (π β β0 β§ (π + π) < π)) β (π΅βπ) = 0) |
92 | 68, 91 | oveq12d 7429 |
. . . . . . . . . 10
β’ ((π β§ (π β β0 β§ (π + π) < π)) β ((π΄βπ) β (π΅βπ)) = (0 β 0)) |
93 | | 0m0e0 12336 |
. . . . . . . . . 10
β’ (0
β 0) = 0 |
94 | 92, 93 | eqtrdi 2786 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§ (π + π) < π)) β ((π΄βπ) β (π΅βπ)) = 0) |
95 | 36, 94 | eqtrd 2770 |
. . . . . . . 8
β’ ((π β§ (π β β0 β§ (π + π) < π)) β ((π΄ βf β π΅)βπ) = 0) |
96 | 95 | expr 455 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π + π) < π β ((π΄ βf β π΅)βπ) = 0)) |
97 | 30, 96 | sylbird 259 |
. . . . . 6
β’ ((π β§ π β β0) β (Β¬
π β€ (π + π) β ((π΄ βf β π΅)βπ) = 0)) |
98 | 97 | necon1ad 2955 |
. . . . 5
β’ ((π β§ π β β0) β (((π΄ βf β
π΅)βπ) β 0 β π β€ (π + π))) |
99 | 98 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β β0 (((π΄ βf β
π΅)βπ) β 0 β π β€ (π + π))) |
100 | | plyco0 25941 |
. . . . 5
β’ (((π + π) β β0 β§ (π΄ βf β
π΅):β0βΆβ) β
(((π΄ βf
β π΅) β
(β€β₯β((π + π) + 1))) = {0} β βπ β β0
(((π΄ βf
β π΅)βπ) β 0 β π β€ (π + π)))) |
101 | 4, 17, 100 | syl2anc 582 |
. . . 4
β’ (π β (((π΄ βf β π΅) β
(β€β₯β((π + π) + 1))) = {0} β βπ β β0
(((π΄ βf
β π΅)βπ) β 0 β π β€ (π + π)))) |
102 | 99, 101 | mpbird 256 |
. . 3
β’ (π β ((π΄ βf β π΅) β
(β€β₯β((π + π) + 1))) = {0}) |
103 | | df-0p 25419 |
. . . . 5
β’
0π = (β Γ {0}) |
104 | | fconstmpt 5737 |
. . . . 5
β’ (β
Γ {0}) = (π§ β
β β¦ 0) |
105 | 103, 104 | eqtri 2758 |
. . . 4
β’
0π = (π§ β β β¦ 0) |
106 | | elfznn0 13598 |
. . . . . . . 8
β’ (π β (0...(π + π)) β π β β0) |
107 | 35 | adantlr 711 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β β0) β ((π΄ βf β
π΅)βπ) = ((π΄βπ) β (π΅βπ))) |
108 | 107 | oveq1d 7426 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π β β0) β (((π΄ βf β
π΅)βπ) Β· (π§βπ)) = (((π΄βπ) β (π΅βπ)) Β· (π§βπ))) |
109 | 11 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β) β π΄:β0βΆβ) |
110 | 109 | ffvelcdmda 7085 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β β0) β (π΄βπ) β β) |
111 | 14 | adantr 479 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β) β π΅:β0βΆβ) |
112 | 111 | ffvelcdmda 7085 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β β0) β (π΅βπ) β β) |
113 | | expcl 14049 |
. . . . . . . . . . 11
β’ ((π§ β β β§ π β β0)
β (π§βπ) β
β) |
114 | 113 | adantll 710 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β β0) β (π§βπ) β β) |
115 | 110, 112,
114 | subdird 11675 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π β β0) β (((π΄βπ) β (π΅βπ)) Β· (π§βπ)) = (((π΄βπ) Β· (π§βπ)) β ((π΅βπ) Β· (π§βπ)))) |
116 | 108, 115 | eqtrd 2770 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π β β0) β (((π΄ βf β
π΅)βπ) Β· (π§βπ)) = (((π΄βπ) Β· (π§βπ)) β ((π΅βπ) Β· (π§βπ)))) |
117 | 106, 116 | sylan2 591 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π β (0...(π + π))) β (((π΄ βf β π΅)βπ) Β· (π§βπ)) = (((π΄βπ) Β· (π§βπ)) β ((π΅βπ) Β· (π§βπ)))) |
118 | 117 | sumeq2dv 15653 |
. . . . . 6
β’ ((π β§ π§ β β) β Ξ£π β (0...(π + π))(((π΄ βf β π΅)βπ) Β· (π§βπ)) = Ξ£π β (0...(π + π))(((π΄βπ) Β· (π§βπ)) β ((π΅βπ) Β· (π§βπ)))) |
119 | | fzfid 13942 |
. . . . . . 7
β’ ((π β§ π§ β β) β (0...(π + π)) β Fin) |
120 | 110, 114 | mulcld 11238 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π β β0) β ((π΄βπ) Β· (π§βπ)) β β) |
121 | 106, 120 | sylan2 591 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π β (0...(π + π))) β ((π΄βπ) Β· (π§βπ)) β β) |
122 | 112, 114 | mulcld 11238 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π β β0) β ((π΅βπ) Β· (π§βπ)) β β) |
123 | 106, 122 | sylan2 591 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π β (0...(π + π))) β ((π΅βπ) Β· (π§βπ)) β β) |
124 | 119, 121,
123 | fsumsub 15738 |
. . . . . 6
β’ ((π β§ π§ β β) β Ξ£π β (0...(π + π))(((π΄βπ) Β· (π§βπ)) β ((π΅βπ) Β· (π§βπ))) = (Ξ£π β (0...(π + π))((π΄βπ) Β· (π§βπ)) β Ξ£π β (0...(π + π))((π΅βπ) Β· (π§βπ)))) |
125 | 119, 121 | fsumcl 15683 |
. . . . . . 7
β’ ((π β§ π§ β β) β Ξ£π β (0...(π + π))((π΄βπ) Β· (π§βπ)) β β) |
126 | | coeeu.8 |
. . . . . . . . . . 11
β’ (π β πΉ = (π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))) |
127 | | coeeu.9 |
. . . . . . . . . . 11
β’ (π β πΉ = (π§ β β β¦ Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)))) |
128 | 126, 127 | eqtr3d 2772 |
. . . . . . . . . 10
β’ (π β (π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)))) |
129 | 128 | fveq1d 6892 |
. . . . . . . . 9
β’ (π β ((π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ§) = ((π§ β β β¦ Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)))βπ§)) |
130 | 129 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π§ β β) β ((π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ§) = ((π§ β β β¦ Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)))βπ§)) |
131 | | simpr 483 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β π§ β β) |
132 | | sumex 15638 |
. . . . . . . . . 10
β’
Ξ£π β
(0...π)((π΄βπ) Β· (π§βπ)) β V |
133 | | eqid 2730 |
. . . . . . . . . . 11
β’ (π§ β β β¦
Ξ£π β (0...π)((π΄βπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ))) |
134 | 133 | fvmpt2 7008 |
. . . . . . . . . 10
β’ ((π§ β β β§
Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)) β V) β ((π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ§) = Ξ£π β (0...π)((π΄βπ) Β· (π§βπ))) |
135 | 131, 132,
134 | sylancl 584 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β ((π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ§) = Ξ£π β (0...π)((π΄βπ) Β· (π§βπ))) |
136 | | fzss2 13545 |
. . . . . . . . . . . 12
β’ ((π + π) β (β€β₯βπ) β (0...π) β (0...(π + π))) |
137 | 53, 136 | syl 17 |
. . . . . . . . . . 11
β’ (π β (0...π) β (0...(π + π))) |
138 | 137 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β (0...π) β (0...(π + π))) |
139 | 138 | sselda 3981 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β (0...π)) β π β (0...(π + π))) |
140 | 139, 121 | syldan 589 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β (0...π)) β ((π΄βπ) Β· (π§βπ)) β β) |
141 | | eldifn 4126 |
. . . . . . . . . . . . . 14
β’ (π β ((0...(π + π)) β (0...π)) β Β¬ π β (0...π)) |
142 | 141 | adantl 480 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β Β¬ π β (0...π)) |
143 | | eldifi 4125 |
. . . . . . . . . . . . . . 15
β’ (π β ((0...(π + π)) β (0...π)) β π β (0...(π + π))) |
144 | 143, 106 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((0...(π + π)) β (0...π)) β π β β0) |
145 | | simpr 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β0) β π β
β0) |
146 | 145, 45 | eleqtrdi 2841 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β0) β π β
(β€β₯β0)) |
147 | 47 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β0) β π β
β€) |
148 | | elfz5 13497 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β
(β€β₯β0) β§ π β β€) β (π β (0...π) β π β€ π)) |
149 | 146, 147,
148 | syl2anc 582 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β (π β (0...π) β π β€ π)) |
150 | 65, 149 | sylibrd 258 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β ((π΄βπ) β 0 β π β (0...π))) |
151 | 150 | adantlr 711 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β) β§ π β β0) β ((π΄βπ) β 0 β π β (0...π))) |
152 | 151 | necon1bd 2956 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π β β0) β (Β¬
π β (0...π) β (π΄βπ) = 0)) |
153 | 144, 152 | sylan2 591 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β (Β¬ π β (0...π) β (π΄βπ) = 0)) |
154 | 142, 153 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β (π΄βπ) = 0) |
155 | 154 | oveq1d 7426 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β ((π΄βπ) Β· (π§βπ)) = (0 Β· (π§βπ))) |
156 | 131, 144,
113 | syl2an 594 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β (π§βπ) β β) |
157 | 156 | mul02d 11416 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β (0 Β· (π§βπ)) = 0) |
158 | 155, 157 | eqtrd 2770 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β ((π΄βπ) Β· (π§βπ)) = 0) |
159 | 138, 140,
158, 119 | fsumss 15675 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)) = Ξ£π β (0...(π + π))((π΄βπ) Β· (π§βπ))) |
160 | 135, 159 | eqtrd 2770 |
. . . . . . . 8
β’ ((π β§ π§ β β) β ((π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ§) = Ξ£π β (0...(π + π))((π΄βπ) Β· (π§βπ))) |
161 | | sumex 15638 |
. . . . . . . . . 10
β’
Ξ£π β
(0...π)((π΅βπ) Β· (π§βπ)) β V |
162 | | eqid 2730 |
. . . . . . . . . . 11
β’ (π§ β β β¦
Ξ£π β (0...π)((π΅βπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((π΅βπ) Β· (π§βπ))) |
163 | 162 | fvmpt2 7008 |
. . . . . . . . . 10
β’ ((π§ β β β§
Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)) β V) β ((π§ β β β¦ Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)))βπ§) = Ξ£π β (0...π)((π΅βπ) Β· (π§βπ))) |
164 | 131, 161,
163 | sylancl 584 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β ((π§ β β β¦ Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)))βπ§) = Ξ£π β (0...π)((π΅βπ) Β· (π§βπ))) |
165 | | fzss2 13545 |
. . . . . . . . . . . 12
β’ ((π + π) β (β€β₯βπ) β (0...π) β (0...(π + π))) |
166 | 77, 165 | syl 17 |
. . . . . . . . . . 11
β’ (π β (0...π) β (0...(π + π))) |
167 | 166 | adantr 479 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β (0...π) β (0...(π + π))) |
168 | 167 | sselda 3981 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β (0...π)) β π β (0...(π + π))) |
169 | 168, 123 | syldan 589 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β (0...π)) β ((π΅βπ) Β· (π§βπ)) β β) |
170 | | eldifn 4126 |
. . . . . . . . . . . . . 14
β’ (π β ((0...(π + π)) β (0...π)) β Β¬ π β (0...π)) |
171 | 170 | adantl 480 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β Β¬ π β (0...π)) |
172 | | eldifi 4125 |
. . . . . . . . . . . . . . 15
β’ (π β ((0...(π + π)) β (0...π)) β π β (0...(π + π))) |
173 | 172, 106 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β ((0...(π + π)) β (0...π)) β π β β0) |
174 | 72 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β0) β π β
β€) |
175 | | elfz5 13497 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β
(β€β₯β0) β§ π β β€) β (π β (0...π) β π β€ π)) |
176 | 146, 174,
175 | syl2anc 582 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β (π β (0...π) β π β€ π)) |
177 | 88, 176 | sylibrd 258 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β ((π΅βπ) β 0 β π β (0...π))) |
178 | 177 | adantlr 711 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β β) β§ π β β0) β ((π΅βπ) β 0 β π β (0...π))) |
179 | 178 | necon1bd 2956 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β β) β§ π β β0) β (Β¬
π β (0...π) β (π΅βπ) = 0)) |
180 | 173, 179 | sylan2 591 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β (Β¬ π β (0...π) β (π΅βπ) = 0)) |
181 | 171, 180 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β (π΅βπ) = 0) |
182 | 181 | oveq1d 7426 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β ((π΅βπ) Β· (π§βπ)) = (0 Β· (π§βπ))) |
183 | 131, 173,
113 | syl2an 594 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β (π§βπ) β β) |
184 | 183 | mul02d 11416 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β (0 Β· (π§βπ)) = 0) |
185 | 182, 184 | eqtrd 2770 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π β ((0...(π + π)) β (0...π))) β ((π΅βπ) Β· (π§βπ)) = 0) |
186 | 167, 169,
185, 119 | fsumss 15675 |
. . . . . . . . 9
β’ ((π β§ π§ β β) β Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)) = Ξ£π β (0...(π + π))((π΅βπ) Β· (π§βπ))) |
187 | 164, 186 | eqtrd 2770 |
. . . . . . . 8
β’ ((π β§ π§ β β) β ((π§ β β β¦ Ξ£π β (0...π)((π΅βπ) Β· (π§βπ)))βπ§) = Ξ£π β (0...(π + π))((π΅βπ) Β· (π§βπ))) |
188 | 130, 160,
187 | 3eqtr3d 2778 |
. . . . . . 7
β’ ((π β§ π§ β β) β Ξ£π β (0...(π + π))((π΄βπ) Β· (π§βπ)) = Ξ£π β (0...(π + π))((π΅βπ) Β· (π§βπ))) |
189 | 125, 188 | subeq0bd 11644 |
. . . . . 6
β’ ((π β§ π§ β β) β (Ξ£π β (0...(π + π))((π΄βπ) Β· (π§βπ)) β Ξ£π β (0...(π + π))((π΅βπ) Β· (π§βπ))) = 0) |
190 | 118, 124,
189 | 3eqtrrd 2775 |
. . . . 5
β’ ((π β§ π§ β β) β 0 = Ξ£π β (0...(π + π))(((π΄ βf β π΅)βπ) Β· (π§βπ))) |
191 | 190 | mpteq2dva 5247 |
. . . 4
β’ (π β (π§ β β β¦ 0) = (π§ β β β¦
Ξ£π β (0...(π + π))(((π΄ βf β π΅)βπ) Β· (π§βπ)))) |
192 | 105, 191 | eqtrid 2782 |
. . 3
β’ (π β 0π =
(π§ β β β¦
Ξ£π β (0...(π + π))(((π΄ βf β π΅)βπ) Β· (π§βπ)))) |
193 | 1, 4, 26, 102, 192 | plyeq0 25960 |
. 2
β’ (π β (π΄ βf β π΅) = (β0 Γ
{0})) |
194 | | ofsubeq0 12213 |
. . 3
β’
((β0 β V β§ π΄:β0βΆβ β§
π΅:β0βΆβ) β
((π΄ βf
β π΅) =
(β0 Γ {0}) β π΄ = π΅)) |
195 | 9, 11, 14, 194 | mp3an2i 1464 |
. 2
β’ (π β ((π΄ βf β π΅) = (β0 Γ
{0}) β π΄ = π΅)) |
196 | 193, 195 | mpbid 231 |
1
β’ (π β π΄ = π΅) |