Proof of Theorem binom4
Step | Hyp | Ref
| Expression |
1 | | df-4 10667 |
. . . 4
   |
2 | 1 | oveq2i 6299 |
. . 3
               |
3 | | addcl 9618 |
. . . 4
 
     |
4 | | 3nn0 10884 |
. . . 4
 |
5 | | expp1 12276 |
. . . 4
   
                     |
6 | 3, 4, 5 | sylancl 667 |
. . 3
 
                     |
7 | 2, 6 | syl5eq 2496 |
. 2
 
                   |
8 | | binom3 12390 |
. . 3
 
                                       |
9 | 8 | oveq1d 6303 |
. 2
 
        
                                      |
10 | | simpl 459 |
. . . . . . 7
 
   |
11 | | expcl 12287 |
. . . . . . 7
 
       |
12 | 10, 4, 11 | sylancl 667 |
. . . . . 6
 
       |
13 | | 3cn 10681 |
. . . . . . 7
 |
14 | 10 | sqcld 12411 |
. . . . . . . 8
 
       |
15 | | simpr 463 |
. . . . . . . 8
 
   |
16 | 14, 15 | mulcld 9660 |
. . . . . . 7
 
         |
17 | | mulcl 9620 |
. . . . . . 7
                   |
18 | 13, 16, 17 | sylancr 668 |
. . . . . 6
 
           |
19 | 12, 18 | addcld 9659 |
. . . . 5
 
                 |
20 | 15 | sqcld 12411 |
. . . . . . . 8
 
       |
21 | 10, 20 | mulcld 9660 |
. . . . . . 7
 
         |
22 | | mulcl 9620 |
. . . . . . 7
  
       
        |
23 | 13, 21, 22 | sylancr 668 |
. . . . . 6
 
  
        |
24 | | expcl 12287 |
. . . . . . 7
 
       |
25 | 15, 4, 24 | sylancl 667 |
. . . . . 6
 
       |
26 | 23, 25 | addcld 9659 |
. . . . 5
 
                 |
27 | 19, 26 | addcld 9659 |
. . . 4
 
                  
              |
28 | 27, 10, 15 | adddid 9664 |
. . 3
 
                                                                                                       |
29 | 19, 26, 10 | adddird 9665 |
. . . . 5
 
                                                                     |
30 | 12, 18, 10 | adddird 9665 |
. . . . . . 7
 
                                     |
31 | 1 | oveq2i 6299 |
. . . . . . . . 9
           |
32 | | expp1 12276 |
. . . . . . . . . 10
 
               |
33 | 10, 4, 32 | sylancl 667 |
. . . . . . . . 9
 
               |
34 | 31, 33 | syl5req 2497 |
. . . . . . . 8
 
             |
35 | 13 | a1i 11 |
. . . . . . . . . 10
 
   |
36 | 35, 16, 10 | mulassd 9663 |
. . . . . . . . 9
 
                       |
37 | 14, 15, 10 | mul32d 9840 |
. . . . . . . . . . 11
 
                   |
38 | | df-3 10666 |
. . . . . . . . . . . . . 14
   |
39 | 38 | oveq2i 6299 |
. . . . . . . . . . . . 13
           |
40 | | 2nn0 10883 |
. . . . . . . . . . . . . 14
 |
41 | | expp1 12276 |
. . . . . . . . . . . . . 14
 
               |
42 | 10, 40, 41 | sylancl 667 |
. . . . . . . . . . . . 13
 
               |
43 | 39, 42 | syl5req 2497 |
. . . . . . . . . . . 12
 
             |
44 | 43 | oveq1d 6303 |
. . . . . . . . . . 11
 
                 |
45 | 37, 44 | eqtrd 2484 |
. . . . . . . . . 10
 
                 |
46 | 45 | oveq2d 6304 |
. . . . . . . . 9
 
                     |
47 | 36, 46 | eqtrd 2484 |
. . . . . . . 8
 
                     |
48 | 34, 47 | oveq12d 6306 |
. . . . . . 7
 
                                   |
49 | 30, 48 | eqtrd 2484 |
. . . . . 6
 
                                 |
50 | 23, 25, 10 | adddird 9665 |
. . . . . . 7
 
                                     |
51 | 35, 21, 10 | mulassd 9663 |
. . . . . . . . 9
 
                       |
52 | 10, 20, 10 | mul32d 9840 |
. . . . . . . . . . 11
 
                   |
53 | 10 | sqvald 12410 |
. . . . . . . . . . . 12
 
         |
54 | 53 | oveq1d 6303 |
. . . . . . . . . . 11
 
                     |
55 | 52, 54 | eqtr4d 2487 |
. . . . . . . . . 10
 
                     |
56 | 55 | oveq2d 6304 |
. . . . . . . . 9
 
                         |
57 | 51, 56 | eqtrd 2484 |
. . . . . . . 8
 
                         |
58 | 25, 10 | mulcomd 9661 |
. . . . . . . 8
 
               |
59 | 57, 58 | oveq12d 6306 |
. . . . . . 7
 
                                         |
60 | 50, 59 | eqtrd 2484 |
. . . . . 6
 
                                       |
61 | 49, 60 | oveq12d 6306 |
. . . . 5
 
                                                                         |
62 | 29, 61 | eqtrd 2484 |
. . . 4
 
                                                                       |
63 | 19, 26, 15 | adddird 9665 |
. . . . 5
 
                                                                     |
64 | 12, 18, 15 | adddird 9665 |
. . . . . . 7
 
                                     |
65 | 35, 16, 15 | mulassd 9663 |
. . . . . . . . 9
 
                       |
66 | 14, 15, 15 | mulassd 9663 |
. . . . . . . . . . 11
 
                   |
67 | 15 | sqvald 12410 |
. . . . . . . . . . . 12
 
         |
68 | 67 | oveq2d 6304 |
. . . . . . . . . . 11
 
                     |
69 | 66, 68 | eqtr4d 2487 |
. . . . . . . . . 10
 
                     |
70 | 69 | oveq2d 6304 |
. . . . . . . . 9
 
                         |
71 | 65, 70 | eqtrd 2484 |
. . . . . . . 8
 
                         |
72 | 71 | oveq2d 6304 |
. . . . . . 7
 
                                         |
73 | 64, 72 | eqtrd 2484 |
. . . . . 6
 
                                       |
74 | 23, 25, 15 | adddird 9665 |
. . . . . . 7
 
                                     |
75 | 35, 21, 15 | mulassd 9663 |
. . . . . . . . 9
 
                       |
76 | 10, 20, 15 | mulassd 9663 |
. . . . . . . . . . 11
 
                   |
77 | 38 | oveq2i 6299 |
. . . . . . . . . . . . 13
           |
78 | | expp1 12276 |
. . . . . . . . . . . . . 14
 
               |
79 | 15, 40, 78 | sylancl 667 |
. . . . . . . . . . . . 13
 
               |
80 | 77, 79 | syl5req 2497 |
. . . . . . . . . . . 12
 
             |
81 | 80 | oveq2d 6304 |
. . . . . . . . . . 11
 
                 |
82 | 76, 81 | eqtrd 2484 |
. . . . . . . . . 10
 
                 |
83 | 82 | oveq2d 6304 |
. . . . . . . . 9
 
                     |
84 | 75, 83 | eqtrd 2484 |
. . . . . . . 8
 
                     |
85 | 1 | oveq2i 6299 |
. . . . . . . . 9
           |
86 | | expp1 12276 |
. . . . . . . . . 10
 
               |
87 | 15, 4, 86 | sylancl 667 |
. . . . . . . . 9
 
               |
88 | 85, 87 | syl5req 2497 |
. . . . . . . 8
 
             |
89 | 84, 88 | oveq12d 6306 |
. . . . . . 7
 
                                   |
90 | 74, 89 | eqtrd 2484 |
. . . . . 6
 
                                 |
91 | 73, 90 | oveq12d 6306 |
. . . . 5
 
                                                          
              |
92 | 12, 15 | mulcld 9660 |
. . . . . 6
 
         |
93 | 14, 20 | mulcld 9660 |
. . . . . . 7
 
             |
94 | | mulcl 9620 |
. . . . . . 7
                           |
95 | 13, 93, 94 | sylancr 668 |
. . . . . 6
 
               |
96 | 10, 25 | mulcld 9660 |
. . . . . . . 8
 
         |
97 | | mulcl 9620 |
. . . . . . . 8
  
       
        |
98 | 13, 96, 97 | sylancr 668 |
. . . . . . 7
 
  
        |
99 | | 4nn0 10885 |
. . . . . . . 8
 |
100 | | expcl 12287 |
. . . . . . . 8
 
       |
101 | 15, 99, 100 | sylancl 667 |
. . . . . . 7
 
       |
102 | 98, 101 | addcld 9659 |
. . . . . 6
 
                 |
103 | 92, 95, 102 | addassd 9662 |
. . . . 5
 
                        
                                                  |
104 | 63, 91, 103 | 3eqtrd 2488 |
. . . 4
 
                                                                       |
105 | 62, 104 | oveq12d 6306 |
. . 3
 
                                                                                                                                               |
106 | | expcl 12287 |
. . . . . . 7
 
       |
107 | 10, 99, 106 | sylancl 667 |
. . . . . 6
 
       |
108 | | mulcl 9620 |
. . . . . . 7
                   |
109 | 13, 92, 108 | sylancr 668 |
. . . . . 6
 
           |
110 | 107, 109 | addcld 9659 |
. . . . 5
 
                 |
111 | 95, 96 | addcld 9659 |
. . . . 5
 
                       |
112 | 95, 102 | addcld 9659 |
. . . . 5
 
                               |
113 | 110, 111,
92, 112 | add4d 9855 |
. . . 4
 
                                                                                                                                                       |
114 | 107, 109,
92 | addassd 9662 |
. . . . . 6
 
                                               |
115 | 1 | oveq1i 6298 |
. . . . . . . . 9
                   |
116 | | ax-1cn 9594 |
. . . . . . . . . . 11
 |
117 | 116 | a1i 11 |
. . . . . . . . . 10
 
   |
118 | 35, 117, 92 | adddird 9665 |
. . . . . . . . 9
 
                               |
119 | 115, 118 | syl5eq 2496 |
. . . . . . . 8
 
                             |
120 | 92 | mulid2d 9658 |
. . . . . . . . 9
 
                 |
121 | 120 | oveq2d 6304 |
. . . . . . . 8
 
                                     |
122 | 119, 121 | eqtrd 2484 |
. . . . . . 7
 
                           |
123 | 122 | oveq2d 6304 |
. . . . . 6
 
                                       |
124 | 114, 123 | eqtr4d 2487 |
. . . . 5
 
                                       |
125 | 95, 96, 95, 102 | add4d 9855 |
. . . . . 6
 
                                                                                                       |
126 | | 3p3e6 10740 |
. . . . . . . . 9
   |
127 | 126 | oveq1i 6298 |
. . . . . . . 8
                           |
128 | 35, 35, 93 | adddird 9665 |
. . . . . . . 8
 
                                           |
129 | 127, 128 | syl5eqr 2498 |
. . . . . . 7
 
                                         |
130 | | 3p1e4 10732 |
. . . . . . . . . . . . 13
   |
131 | 13, 116, 130 | addcomli 9822 |
. . . . . . . . . . . 12
   |
132 | 131 | oveq1i 6298 |
. . . . . . . . . . 11
                   |
133 | 117, 35, 96 | adddird 9665 |
. . . . . . . . . . 11
 
    
                          |
134 | 132, 133 | syl5eqr 2498 |
. . . . . . . . . 10
 
  
                          |
135 | 96 | mulid2d 9658 |
. . . . . . . . . . 11
 
  
              |
136 | 135 | oveq1d 6303 |
. . . . . . . . . 10
 
                                     |
137 | 134, 136 | eqtrd 2484 |
. . . . . . . . 9
 
  
                        |
138 | 137 | oveq1d 6303 |
. . . . . . . 8
 
                                       |
139 | 96, 98, 101 | addassd 9662 |
. . . . . . . 8
 
          
                                    |
140 | 138, 139 | eqtrd 2484 |
. . . . . . 7
 
                                       |
141 | 129, 140 | oveq12d 6306 |
. . . . . 6
 
                                                                                 |
142 | 125, 141 | eqtr4d 2487 |
. . . . 5
 
                                                                                 |
143 | 124, 142 | oveq12d 6306 |
. . . 4
 
                                                                                                                         |
144 | 113, 143 | eqtrd 2484 |
. . 3
 
                                                                                                                         |
145 | 28, 105, 144 | 3eqtrd 2488 |
. 2
 
                                                                                 |
146 | 7, 9, 145 | 3eqtrd 2488 |
1
 
                                                     |