Proof of Theorem fsumcube
Step | Hyp | Ref
| Expression |
1 | | 3nn0 11310 |
. . 3
|
2 | | fsumkthpow 14787 |
. . 3
BernPoly BernPoly |
3 | 1, 2 | mpan 706 |
. 2
BernPoly
BernPoly |
4 | | df-4 11081 |
. . . . . 6
|
5 | 4 | oveq1i 6660 |
. . . . 5
BernPoly
BernPoly |
6 | 4 | oveq1i 6660 |
. . . . 5
BernPoly BernPoly |
7 | 5, 6 | oveq12i 6662 |
. . . 4
BernPoly
BernPoly BernPoly
BernPoly |
8 | 7, 4 | oveq12i 6662 |
. . 3
BernPoly BernPoly BernPoly BernPoly |
9 | | nn0cn 11302 |
. . . . . . . 8
|
10 | | peano2cn 10208 |
. . . . . . . 8
|
11 | 9, 10 | syl 17 |
. . . . . . 7
|
12 | | bpoly4 14790 |
. . . . . . 7
BernPoly ; |
13 | 11, 12 | syl 17 |
. . . . . 6
BernPoly
; |
14 | | 4nn 11187 |
. . . . . . . . . . . . . 14
|
15 | | 0exp 12895 |
. . . . . . . . . . . . . 14
|
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . 13
|
17 | | 3nn 11186 |
. . . . . . . . . . . . . . . 16
|
18 | | 0exp 12895 |
. . . . . . . . . . . . . . . 16
|
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
20 | 19 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
21 | | 2t0e0 11183 |
. . . . . . . . . . . . . 14
|
22 | 20, 21 | eqtri 2644 |
. . . . . . . . . . . . 13
|
23 | 16, 22 | oveq12i 6662 |
. . . . . . . . . . . 12
|
24 | | 0m0e0 11130 |
. . . . . . . . . . . 12
|
25 | 23, 24 | eqtri 2644 |
. . . . . . . . . . 11
|
26 | | sq0 12955 |
. . . . . . . . . . 11
|
27 | 25, 26 | oveq12i 6662 |
. . . . . . . . . 10
|
28 | | 00id 10211 |
. . . . . . . . . 10
|
29 | 27, 28 | eqtri 2644 |
. . . . . . . . 9
|
30 | 29 | oveq1i 6660 |
. . . . . . . 8
; ; |
31 | | 0cn 10032 |
. . . . . . . . 9
|
32 | | bpoly4 14790 |
. . . . . . . . 9
BernPoly ; |
33 | 31, 32 | ax-mp 5 |
. . . . . . . 8
BernPoly ; |
34 | | df-neg 10269 |
. . . . . . . 8
;
; |
35 | 30, 33, 34 | 3eqtr4i 2654 |
. . . . . . 7
BernPoly ; |
36 | 35 | a1i 11 |
. . . . . 6
BernPoly ; |
37 | 13, 36 | oveq12d 6668 |
. . . . 5
BernPoly
BernPoly ;
; |
38 | | 4nn0 11311 |
. . . . . . . . . . . 12
|
39 | | expcl 12878 |
. . . . . . . . . . . 12
|
40 | 38, 39 | mpan2 707 |
. . . . . . . . . . 11
|
41 | | 2cn 11091 |
. . . . . . . . . . . 12
|
42 | | expcl 12878 |
. . . . . . . . . . . . 13
|
43 | 1, 42 | mpan2 707 |
. . . . . . . . . . . 12
|
44 | | mulcl 10020 |
. . . . . . . . . . . 12
|
45 | 41, 43, 44 | sylancr 695 |
. . . . . . . . . . 11
|
46 | 40, 45 | subcld 10392 |
. . . . . . . . . 10
|
47 | | sqcl 12925 |
. . . . . . . . . 10
|
48 | 46, 47 | addcld 10059 |
. . . . . . . . 9
|
49 | 10, 48 | syl 17 |
. . . . . . . 8
|
50 | 9, 49 | syl 17 |
. . . . . . 7
|
51 | | 0nn0 11307 |
. . . . . . . . . 10
|
52 | 1, 51 | deccl 11512 |
. . . . . . . . 9
; |
53 | 52 | nn0cni 11304 |
. . . . . . . 8
; |
54 | 52 | nn0rei 11303 |
. . . . . . . . 9
; |
55 | | 10pos 11515 |
. . . . . . . . . 10
; |
56 | 17, 51, 51, 55 | declti 11546 |
. . . . . . . . 9
; |
57 | 54, 56 | gt0ne0ii 10564 |
. . . . . . . 8
; |
58 | 53, 57 | reccli 10755 |
. . . . . . 7
; |
59 | | subcl 10280 |
. . . . . . 7
; ; |
60 | 50, 58, 59 | sylancl 694 |
. . . . . 6
; |
61 | | subneg 10330 |
. . . . . 6
;
;
; ;
; ; |
62 | 60, 58, 61 | sylancl 694 |
. . . . 5
; ;
; ; |
63 | | npcan 10290 |
. . . . . . . 8
;
; ; |
64 | 49, 58, 63 | sylancl 694 |
. . . . . . 7
; ; |
65 | 9, 64 | syl 17 |
. . . . . 6
; ; |
66 | | 2p2e4 11144 |
. . . . . . . . . . 11
|
67 | 66 | eqcomi 2631 |
. . . . . . . . . 10
|
68 | 67 | oveq2i 6661 |
. . . . . . . . 9
|
69 | | df-3 11080 |
. . . . . . . . . . 11
|
70 | 69 | oveq2i 6661 |
. . . . . . . . . 10
|
71 | 70 | oveq2i 6661 |
. . . . . . . . 9
|
72 | 68, 71 | oveq12i 6662 |
. . . . . . . 8
|
73 | 72 | oveq1i 6660 |
. . . . . . 7
|
74 | | 2nn0 11309 |
. . . . . . . . . . . . 13
|
75 | | expadd 12902 |
. . . . . . . . . . . . 13
|
76 | 74, 74, 75 | mp3an23 1416 |
. . . . . . . . . . . 12
|
77 | | 1nn0 11308 |
. . . . . . . . . . . . . 14
|
78 | | expadd 12902 |
. . . . . . . . . . . . . 14
|
79 | 74, 77, 78 | mp3an23 1416 |
. . . . . . . . . . . . 13
|
80 | 79 | oveq2d 6666 |
. . . . . . . . . . . 12
|
81 | 76, 80 | oveq12d 6668 |
. . . . . . . . . . 11
|
82 | 10, 81 | syl 17 |
. . . . . . . . . 10
|
83 | 10 | sqcld 13006 |
. . . . . . . . . . . 12
|
84 | 83 | mulid1d 10057 |
. . . . . . . . . . 11
|
85 | 84 | eqcomd 2628 |
. . . . . . . . . 10
|
86 | 82, 85 | oveq12d 6668 |
. . . . . . . . 9
|
87 | 10 | exp1d 13003 |
. . . . . . . . . . . . . . . 16
|
88 | 87 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
89 | 88 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
90 | 89 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
91 | 87, 10 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
|
92 | | mul12 10202 |
. . . . . . . . . . . . . . 15
|
93 | 41, 83, 91, 92 | mp3an2i 1429 |
. . . . . . . . . . . . . 14
|
94 | 93 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
95 | | mulcl 10020 |
. . . . . . . . . . . . . . 15
|
96 | 41, 10, 95 | sylancr 695 |
. . . . . . . . . . . . . 14
|
97 | 83, 83, 96 | subdid 10486 |
. . . . . . . . . . . . 13
|
98 | 90, 94, 97 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
|
99 | 98 | oveq1d 6665 |
. . . . . . . . . . 11
|
100 | 83, 96 | subcld 10392 |
. . . . . . . . . . . 12
|
101 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
102 | | adddi 10025 |
. . . . . . . . . . . . 13
|
103 | 101, 102 | mp3an3 1413 |
. . . . . . . . . . . 12
|
104 | 83, 100, 103 | syl2anc 693 |
. . . . . . . . . . 11
|
105 | 99, 104 | eqtr4d 2659 |
. . . . . . . . . 10
|
106 | | adddi 10025 |
. . . . . . . . . . . . . . . . 17
|
107 | 41, 101, 106 | mp3an13 1415 |
. . . . . . . . . . . . . . . 16
|
108 | | 2t1e2 11176 |
. . . . . . . . . . . . . . . . 17
|
109 | 108 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
|
110 | 107, 109 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
111 | 110 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
112 | | mulcl 10020 |
. . . . . . . . . . . . . . . . 17
|
113 | 41, 112 | mpan 706 |
. . . . . . . . . . . . . . . 16
|
114 | | addsubass 10291 |
. . . . . . . . . . . . . . . . 17
|
115 | 41, 101, 114 | mp3an23 1416 |
. . . . . . . . . . . . . . . 16
|
116 | 113, 115 | syl 17 |
. . . . . . . . . . . . . . 15
|
117 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . 16
|
118 | 117 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
|
119 | 116, 118 | syl6eq 2672 |
. . . . . . . . . . . . . 14
|
120 | 111, 119 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
121 | 120 | oveq2d 6666 |
. . . . . . . . . . . 12
|
122 | | subsub 10311 |
. . . . . . . . . . . . . 14
|
123 | 101, 122 | mp3an3 1413 |
. . . . . . . . . . . . 13
|
124 | 83, 96, 123 | syl2anc 693 |
. . . . . . . . . . . 12
|
125 | | sqcl 12925 |
. . . . . . . . . . . . 13
|
126 | | peano2cn 10208 |
. . . . . . . . . . . . . 14
|
127 | 113, 126 | syl 17 |
. . . . . . . . . . . . 13
|
128 | | binom21 12980 |
. . . . . . . . . . . . . 14
|
129 | | addass 10023 |
. . . . . . . . . . . . . . . 16
|
130 | 101, 129 | mp3an3 1413 |
. . . . . . . . . . . . . . 15
|
131 | 125, 113,
130 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
132 | 128, 131 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
133 | 125, 127,
132 | mvrraddd 10445 |
. . . . . . . . . . . 12
|
134 | 121, 124,
133 | 3eqtr3d 2664 |
. . . . . . . . . . 11
|
135 | 134 | oveq2d 6666 |
. . . . . . . . . 10
|
136 | 83, 125 | mulcomd 10061 |
. . . . . . . . . 10
|
137 | 105, 135,
136 | 3eqtrd 2660 |
. . . . . . . . 9
|
138 | 86, 137 | eqtrd 2656 |
. . . . . . . 8
|
139 | 9, 138 | syl 17 |
. . . . . . 7
|
140 | 73, 139 | syl5eq 2668 |
. . . . . 6
|
141 | 65, 140 | eqtrd 2656 |
. . . . 5
; ; |
142 | 37, 62, 141 | 3eqtrd 2660 |
. . . 4
BernPoly
BernPoly |
143 | 142 | oveq1d 6665 |
. . 3
BernPoly BernPoly |
144 | 8, 143 | syl5eqr 2670 |
. 2
BernPoly BernPoly |
145 | 3, 144 | eqtrd 2656 |
1
|