Proof of Theorem binom4
Step | Hyp | Ref
| Expression |
1 | | df-4 8969 |
. . . 4
   |
2 | 1 | oveq2i 5880 |
. . 3
               |
3 | | addcl 7927 |
. . . 4
 
     |
4 | | 3nn0 9183 |
. . . 4
 |
5 | | expp1 10513 |
. . . 4
   
                     |
6 | 3, 4, 5 | sylancl 413 |
. . 3
 
                     |
7 | 2, 6 | eqtrid 2222 |
. 2
 
                   |
8 | | binom3 10623 |
. . 3
 
                                       |
9 | 8 | oveq1d 5884 |
. 2
 
        
                                      |
10 | | simpl 109 |
. . . . . . 7
 
   |
11 | | expcl 10524 |
. . . . . . 7
 
       |
12 | 10, 4, 11 | sylancl 413 |
. . . . . 6
 
       |
13 | | 3cn 8983 |
. . . . . . 7
 |
14 | 10 | sqcld 10637 |
. . . . . . . 8
 
       |
15 | | simpr 110 |
. . . . . . . 8
 
   |
16 | 14, 15 | mulcld 7968 |
. . . . . . 7
 
         |
17 | | mulcl 7929 |
. . . . . . 7
                   |
18 | 13, 16, 17 | sylancr 414 |
. . . . . 6
 
           |
19 | 12, 18 | addcld 7967 |
. . . . 5
 
                 |
20 | 15 | sqcld 10637 |
. . . . . . . 8
 
       |
21 | 10, 20 | mulcld 7968 |
. . . . . . 7
 
         |
22 | | mulcl 7929 |
. . . . . . 7
  
       
        |
23 | 13, 21, 22 | sylancr 414 |
. . . . . 6
 
  
        |
24 | | expcl 10524 |
. . . . . . 7
 
       |
25 | 15, 4, 24 | sylancl 413 |
. . . . . 6
 
       |
26 | 23, 25 | addcld 7967 |
. . . . 5
 
                 |
27 | 19, 26 | addcld 7967 |
. . . 4
 
                  
              |
28 | 27, 10, 15 | adddid 7972 |
. . 3
 
                                                                                                       |
29 | 1 | oveq2i 5880 |
. . . . . . . . 9
           |
30 | | expp1 10513 |
. . . . . . . . . 10
 
               |
31 | 10, 4, 30 | sylancl 413 |
. . . . . . . . 9
 
               |
32 | 29, 31 | eqtr2id 2223 |
. . . . . . . 8
 
             |
33 | 13 | a1i 9 |
. . . . . . . . . 10
 
   |
34 | 33, 16, 10 | mulassd 7971 |
. . . . . . . . 9
 
                       |
35 | 14, 15, 10 | mul32d 8100 |
. . . . . . . . . . 11
 
                   |
36 | | df-3 8968 |
. . . . . . . . . . . . . 14
   |
37 | 36 | oveq2i 5880 |
. . . . . . . . . . . . 13
           |
38 | | 2nn0 9182 |
. . . . . . . . . . . . . 14
 |
39 | | expp1 10513 |
. . . . . . . . . . . . . 14
 
               |
40 | 10, 38, 39 | sylancl 413 |
. . . . . . . . . . . . 13
 
               |
41 | 37, 40 | eqtr2id 2223 |
. . . . . . . . . . . 12
 
             |
42 | 41 | oveq1d 5884 |
. . . . . . . . . . 11
 
                 |
43 | 35, 42 | eqtrd 2210 |
. . . . . . . . . 10
 
                 |
44 | 43 | oveq2d 5885 |
. . . . . . . . 9
 
                     |
45 | 34, 44 | eqtrd 2210 |
. . . . . . . 8
 
                     |
46 | 32, 45 | oveq12d 5887 |
. . . . . . 7
 
                                   |
47 | 12, 10, 18, 46 | joinlmuladdmuld 7975 |
. . . . . 6
 
                                 |
48 | 33, 21, 10 | mulassd 7971 |
. . . . . . . . 9
 
                       |
49 | 10, 20, 10 | mul32d 8100 |
. . . . . . . . . . 11
 
                   |
50 | 10 | sqvald 10636 |
. . . . . . . . . . . 12
 
         |
51 | 50 | oveq1d 5884 |
. . . . . . . . . . 11
 
                     |
52 | 49, 51 | eqtr4d 2213 |
. . . . . . . . . 10
 
                     |
53 | 52 | oveq2d 5885 |
. . . . . . . . 9
 
                         |
54 | 48, 53 | eqtrd 2210 |
. . . . . . . 8
 
                         |
55 | 25, 10 | mulcomd 7969 |
. . . . . . . 8
 
               |
56 | 54, 55 | oveq12d 5887 |
. . . . . . 7
 
                                         |
57 | 23, 10, 25, 56 | joinlmuladdmuld 7975 |
. . . . . 6
 
                                       |
58 | 47, 57 | oveq12d 5887 |
. . . . 5
 
                                                                         |
59 | 19, 10, 26, 58 | joinlmuladdmuld 7975 |
. . . 4
 
                                                                       |
60 | 19, 26, 15 | adddird 7973 |
. . . . 5
 
                                                                     |
61 | 33, 16, 15 | mulassd 7971 |
. . . . . . . . 9
 
                       |
62 | 14, 15, 15 | mulassd 7971 |
. . . . . . . . . . 11
 
                   |
63 | 15 | sqvald 10636 |
. . . . . . . . . . . 12
 
         |
64 | 63 | oveq2d 5885 |
. . . . . . . . . . 11
 
                     |
65 | 62, 64 | eqtr4d 2213 |
. . . . . . . . . 10
 
                     |
66 | 65 | oveq2d 5885 |
. . . . . . . . 9
 
                         |
67 | 61, 66 | eqtrd 2210 |
. . . . . . . 8
 
                         |
68 | 67 | oveq2d 5885 |
. . . . . . 7
 
                                         |
69 | 12, 15, 18, 68 | joinlmuladdmuld 7975 |
. . . . . 6
 
                                       |
70 | 33, 21, 15 | mulassd 7971 |
. . . . . . . . 9
 
                       |
71 | 10, 20, 15 | mulassd 7971 |
. . . . . . . . . . 11
 
                   |
72 | 36 | oveq2i 5880 |
. . . . . . . . . . . . 13
           |
73 | | expp1 10513 |
. . . . . . . . . . . . . 14
 
               |
74 | 15, 38, 73 | sylancl 413 |
. . . . . . . . . . . . 13
 
               |
75 | 72, 74 | eqtr2id 2223 |
. . . . . . . . . . . 12
 
             |
76 | 75 | oveq2d 5885 |
. . . . . . . . . . 11
 
                 |
77 | 71, 76 | eqtrd 2210 |
. . . . . . . . . 10
 
                 |
78 | 77 | oveq2d 5885 |
. . . . . . . . 9
 
                     |
79 | 70, 78 | eqtrd 2210 |
. . . . . . . 8
 
                     |
80 | 1 | oveq2i 5880 |
. . . . . . . . 9
           |
81 | | expp1 10513 |
. . . . . . . . . 10
 
               |
82 | 15, 4, 81 | sylancl 413 |
. . . . . . . . 9
 
               |
83 | 80, 82 | eqtr2id 2223 |
. . . . . . . 8
 
             |
84 | 79, 83 | oveq12d 5887 |
. . . . . . 7
 
                                   |
85 | 23, 15, 25, 84 | joinlmuladdmuld 7975 |
. . . . . 6
 
                                 |
86 | 69, 85 | oveq12d 5887 |
. . . . 5
 
                                                          
              |
87 | 12, 15 | mulcld 7968 |
. . . . . 6
 
         |
88 | 14, 20 | mulcld 7968 |
. . . . . . 7
 
             |
89 | | mulcl 7929 |
. . . . . . 7
                           |
90 | 13, 88, 89 | sylancr 414 |
. . . . . 6
 
               |
91 | 10, 25 | mulcld 7968 |
. . . . . . . 8
 
         |
92 | | mulcl 7929 |
. . . . . . . 8
  
       
        |
93 | 13, 91, 92 | sylancr 414 |
. . . . . . 7
 
  
        |
94 | | 4nn0 9184 |
. . . . . . . 8
 |
95 | | expcl 10524 |
. . . . . . . 8
 
       |
96 | 15, 94, 95 | sylancl 413 |
. . . . . . 7
 
       |
97 | 93, 96 | addcld 7967 |
. . . . . 6
 
                 |
98 | 87, 90, 97 | addassd 7970 |
. . . . 5
 
                        
                                                  |
99 | 60, 86, 98 | 3eqtrd 2214 |
. . . 4
 
                                                                       |
100 | 59, 99 | oveq12d 5887 |
. . 3
 
                                                                                                                                               |
101 | | expcl 10524 |
. . . . . . 7
 
       |
102 | 10, 94, 101 | sylancl 413 |
. . . . . 6
 
       |
103 | | mulcl 7929 |
. . . . . . 7
                   |
104 | 13, 87, 103 | sylancr 414 |
. . . . . 6
 
           |
105 | 102, 104 | addcld 7967 |
. . . . 5
 
                 |
106 | 90, 91 | addcld 7967 |
. . . . 5
 
                       |
107 | 90, 97 | addcld 7967 |
. . . . 5
 
                               |
108 | 105, 106,
87, 107 | add4d 8116 |
. . . 4
 
                                                                                                                                                       |
109 | 102, 104,
87 | addassd 7970 |
. . . . . 6
 
                                               |
110 | 1 | oveq1i 5879 |
. . . . . . . . 9
                   |
111 | | ax-1cn 7895 |
. . . . . . . . . . 11
 |
112 | 111 | a1i 9 |
. . . . . . . . . 10
 
   |
113 | 33, 112, 87 | adddird 7973 |
. . . . . . . . 9
 
                               |
114 | 110, 113 | eqtrid 2222 |
. . . . . . . 8
 
                             |
115 | 87 | mulid2d 7966 |
. . . . . . . . 9
 
                 |
116 | 115 | oveq2d 5885 |
. . . . . . . 8
 
                                     |
117 | 114, 116 | eqtrd 2210 |
. . . . . . 7
 
                           |
118 | 117 | oveq2d 5885 |
. . . . . 6
 
                                       |
119 | 109, 118 | eqtr4d 2213 |
. . . . 5
 
                                       |
120 | 90, 91, 90, 97 | add4d 8116 |
. . . . . 6
 
                                                                                                       |
121 | | 3p3e6 9050 |
. . . . . . . . 9
   |
122 | 121 | oveq1i 5879 |
. . . . . . . 8
                           |
123 | 33, 33, 88 | adddird 7973 |
. . . . . . . 8
 
                                           |
124 | 122, 123 | eqtr3id 2224 |
. . . . . . 7
 
                                         |
125 | | 3p1e4 9043 |
. . . . . . . . . . . . 13
   |
126 | 13, 111, 125 | addcomli 8092 |
. . . . . . . . . . . 12
   |
127 | 126 | oveq1i 5879 |
. . . . . . . . . . 11
                   |
128 | 112, 33, 91 | adddird 7973 |
. . . . . . . . . . 11
 
    
                          |
129 | 127, 128 | eqtr3id 2224 |
. . . . . . . . . 10
 
  
                          |
130 | 91 | mulid2d 7966 |
. . . . . . . . . . 11
 
  
              |
131 | 130 | oveq1d 5884 |
. . . . . . . . . 10
 
                                     |
132 | 129, 131 | eqtrd 2210 |
. . . . . . . . 9
 
  
                        |
133 | 132 | oveq1d 5884 |
. . . . . . . 8
 
                                       |
134 | 91, 93, 96 | addassd 7970 |
. . . . . . . 8
 
          
                                    |
135 | 133, 134 | eqtrd 2210 |
. . . . . . 7
 
                                       |
136 | 124, 135 | oveq12d 5887 |
. . . . . 6
 
                                                                                 |
137 | 120, 136 | eqtr4d 2213 |
. . . . 5
 
                                                                                 |
138 | 119, 137 | oveq12d 5887 |
. . . 4
 
                                                                                                                         |
139 | 108, 138 | eqtrd 2210 |
. . 3
 
                                                                                                                         |
140 | 28, 100, 139 | 3eqtrd 2214 |
. 2
 
                                                                                 |
141 | 7, 9, 140 | 3eqtrd 2214 |
1
 
                                                     |