Proof of Theorem bdtrilem
Step | Hyp | Ref
| Expression |
1 | | simp1l 1021 |
. . . . . . . . . . . 12
  
 

   |
2 | | simp3 999 |
. . . . . . . . . . . . 13
  
 

   |
3 | 2 | rpred 9683 |
. . . . . . . . . . . 12
  
 

   |
4 | 1, 3 | resubcld 8328 |
. . . . . . . . . . 11
  
 

     |
5 | 4 | resqcld 10665 |
. . . . . . . . . 10
  
 

         |
6 | | 2re 8978 |
. . . . . . . . . . . 12
 |
7 | 6 | a1i 9 |
. . . . . . . . . . 11
  
 

   |
8 | 1 | recnd 7976 |
. . . . . . . . . . . . . 14
  
 

   |
9 | 2 | rpcnd 9685 |
. . . . . . . . . . . . . 14
  
 

   |
10 | 8, 9 | subcld 8258 |
. . . . . . . . . . . . 13
  
 

     |
11 | 10 | abscld 11174 |
. . . . . . . . . . . 12
  
 

    
    |
12 | | simp2l 1023 |
. . . . . . . . . . . . . . 15
  
 

   |
13 | 12 | recnd 7976 |
. . . . . . . . . . . . . 14
  
 

   |
14 | 13, 9 | subcld 8258 |
. . . . . . . . . . . . 13
  
 

     |
15 | 14 | abscld 11174 |
. . . . . . . . . . . 12
  
 

    
    |
16 | 11, 15 | remulcld 7978 |
. . . . . . . . . . 11
  
 

     
           |
17 | 7, 16 | remulcld 7978 |
. . . . . . . . . 10
  
 

      
            |
18 | 5, 17 | readdcld 7977 |
. . . . . . . . 9
  
 

                   
       |
19 | 1, 12 | remulcld 7978 |
. . . . . . . . . . . 12
  
 

     |
20 | 7, 19 | remulcld 7978 |
. . . . . . . . . . 11
  
 

  
    |
21 | 8, 13 | addcld 7967 |
. . . . . . . . . . . . . . 15
  
 

     |
22 | 21, 9 | subcld 8258 |
. . . . . . . . . . . . . 14
  
 

       |
23 | 22 | abscld 11174 |
. . . . . . . . . . . . 13
  
 

           |
24 | 3, 23 | remulcld 7978 |
. . . . . . . . . . . 12
  
 

             |
25 | 7, 24 | remulcld 7978 |
. . . . . . . . . . 11
  
 

  
            |
26 | 20, 25 | readdcld 7977 |
. . . . . . . . . 10
  
 

                     |
27 | 5, 26 | readdcld 7977 |
. . . . . . . . 9
  
 

          
                  |
28 | 12, 3 | resubcld 8328 |
. . . . . . . . . 10
  
 

     |
29 | 28 | resqcld 10665 |
. . . . . . . . 9
  
 

         |
30 | 19, 24 | readdcld 7977 |
. . . . . . . . . . . 12
  
 

                 |
31 | | 0le2 8998 |
. . . . . . . . . . . . 13
 |
32 | 31 | a1i 9 |
. . . . . . . . . . . 12
  
 


  |
33 | 8, 9, 13, 9 | mulsubd 8364 |
. . . . . . . . . . . . . . . . 17
  
 

    
                  |
34 | 19 | recnd 7976 |
. . . . . . . . . . . . . . . . . 18
  
 

     |
35 | 9, 9 | mulcld 7968 |
. . . . . . . . . . . . . . . . . 18
  
 

     |
36 | 8, 9 | mulcld 7968 |
. . . . . . . . . . . . . . . . . . 19
  
 

     |
37 | 13, 9 | mulcld 7968 |
. . . . . . . . . . . . . . . . . . 19
  
 

     |
38 | 36, 37 | addcld 7967 |
. . . . . . . . . . . . . . . . . 18
  
 

         |
39 | 34, 35, 38 | addsubassd 8278 |
. . . . . . . . . . . . . . . . 17
  
 

                               |
40 | 33, 39 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
  
 

    
                  |
41 | 40 | fveq2d 5515 |
. . . . . . . . . . . . . . 15
  
 

                               |
42 | 35, 38 | subcld 8258 |
. . . . . . . . . . . . . . . 16
  
 

             |
43 | 34, 42 | abstrid 11189 |
. . . . . . . . . . . . . . 15
  
 

                  
                        |
44 | 41, 43 | eqbrtrd 4022 |
. . . . . . . . . . . . . 14
  
 

          
                        |
45 | | simp1r 1022 |
. . . . . . . . . . . . . . . . 17
  
 


  |
46 | | simp2r 1024 |
. . . . . . . . . . . . . . . . 17
  
 


  |
47 | 1, 12, 45, 46 | mulge0d 8568 |
. . . . . . . . . . . . . . . 16
  
 


    |
48 | 19, 47 | absidd 11160 |
. . . . . . . . . . . . . . 15
  
 

    
      |
49 | 9, 21 | subcld 8258 |
. . . . . . . . . . . . . . . . 17
  
 

  
    |
50 | 49, 9 | absmuld 11187 |
. . . . . . . . . . . . . . . 16
  
 

      
                    |
51 | 9, 21, 9 | subdird 8362 |
. . . . . . . . . . . . . . . . . 18
  
 

   
             |
52 | 8, 13, 9 | adddird 7973 |
. . . . . . . . . . . . . . . . . . 19
  
 

             |
53 | 52 | oveq2d 5885 |
. . . . . . . . . . . . . . . . . 18
  
 

                     |
54 | 51, 53 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
  
 

   
               |
55 | 54 | fveq2d 5515 |
. . . . . . . . . . . . . . . 16
  
 

      
                    |
56 | 9, 21 | abssubd 11186 |
. . . . . . . . . . . . . . . . 17
  
 

    
              |
57 | 2 | rpge0d 9687 |
. . . . . . . . . . . . . . . . . 18
  
 


  |
58 | 3, 57 | absidd 11160 |
. . . . . . . . . . . . . . . . 17
  
 

       |
59 | 56, 58 | oveq12d 5887 |
. . . . . . . . . . . . . . . 16
  
 

     
                     |
60 | 50, 55, 59 | 3eqtr3d 2218 |
. . . . . . . . . . . . . . 15
  
 

                           |
61 | 48, 60 | oveq12d 5887 |
. . . . . . . . . . . . . 14
  
 

     
                                 |
62 | 44, 61 | breqtrd 4026 |
. . . . . . . . . . . . 13
  
 

          
 
              |
63 | 10, 14 | absmuld 11187 |
. . . . . . . . . . . . 13
  
 

                     
     |
64 | 23 | recnd 7976 |
. . . . . . . . . . . . . . 15
  
 

           |
65 | 64, 9 | mulcomd 7969 |
. . . . . . . . . . . . . 14
  
 

                       |
66 | 65 | oveq2d 5885 |
. . . . . . . . . . . . 13
  
 

                               |
67 | 62, 63, 66 | 3brtr3d 4031 |
. . . . . . . . . . . 12
  
 

     
                         |
68 | 16, 30, 7, 32, 67 | lemul2ad 8886 |
. . . . . . . . . . 11
  
 

      
                            |
69 | 7 | recnd 7976 |
. . . . . . . . . . . 12
  
 

   |
70 | 9, 64 | mulcld 7968 |
. . . . . . . . . . . 12
  
 

             |
71 | 69, 34, 70 | adddid 7972 |
. . . . . . . . . . 11
  
 

                       
             |
72 | 68, 71 | breqtrd 4026 |
. . . . . . . . . 10
  
 

      
                
             |
73 | 17, 26, 5, 72 | leadd2dd 8507 |
. . . . . . . . 9
  
 

                   
                                 |
74 | 18, 27, 29, 73 | leadd1dd 8506 |
. . . . . . . 8
  
 

              
                                
                     |
75 | 5 | recnd 7976 |
. . . . . . . . 9
  
 

         |
76 | 26 | recnd 7976 |
. . . . . . . . 9
  
 

                     |
77 | 29 | recnd 7976 |
. . . . . . . . 9
  
 

         |
78 | 75, 76, 77 | add32d 8115 |
. . . . . . . 8
  
 

                                                                       |
79 | 74, 78 | breqtrd 4026 |
. . . . . . 7
  
 

              
                                                      |
80 | 75, 77 | addcld 7967 |
. . . . . . . 8
  
 

                 |
81 | 69, 34 | mulcld 7968 |
. . . . . . . 8
  
 

  
    |
82 | 69, 70 | mulcld 7968 |
. . . . . . . 8
  
 

  
            |
83 | 80, 81, 82 | addassd 7970 |
. . . . . . 7
  
 

                  
                                                    |
84 | 79, 83 | breqtrrd 4028 |
. . . . . 6
  
 

              
                                        
             |
85 | 8 | sqcld 10637 |
. . . . . . . . . . . . . 14
  
 

       |
86 | 69, 36 | mulcld 7968 |
. . . . . . . . . . . . . 14
  
 

  
    |
87 | 85, 86 | subcld 8258 |
. . . . . . . . . . . . 13
  
 

             |
88 | 9 | sqcld 10637 |
. . . . . . . . . . . . 13
  
 

       |
89 | 87, 88 | addcld 7967 |
. . . . . . . . . . . 12
  
 

        
          |
90 | 89, 81 | addcld 7967 |
. . . . . . . . . . 11
  
 

                         |
91 | 13 | sqcld 10637 |
. . . . . . . . . . . 12
  
 

       |
92 | 69, 37 | mulcld 7968 |
. . . . . . . . . . . 12
  
 

  
    |
93 | 91, 92 | subcld 8258 |
. . . . . . . . . . 11
  
 

             |
94 | 90, 93 | addcld 7967 |
. . . . . . . . . 10
  
 

                    
                |
95 | 93, 88 | addcld 7967 |
. . . . . . . . . . . 12
  
 

        
          |
96 | 89, 95, 81 | add32d 8115 |
. . . . . . . . . . 11
  
 

                          
                       
                                |
97 | 90, 93, 88 | addassd 7970 |
. . . . . . . . . . 11
  
 

                                                  
                                |
98 | 96, 97 | eqtr4d 2213 |
. . . . . . . . . 10
  
 

                          
                                                        |
99 | 94, 88, 98 | comraddd 8104 |
. . . . . . . . 9
  
 

                          
                                                        |
100 | 81, 93 | addcld 7967 |
. . . . . . . . . . . . 13
  
 

                   |
101 | 87, 100 | addcld 7967 |
. . . . . . . . . . . 12
  
 

        
     
                |
102 | 89, 81, 93 | addassd 7970 |
. . . . . . . . . . . . . 14
  
 

                    
                                                  |
103 | 87, 88 | addcomd 8098 |
. . . . . . . . . . . . . . 15
  
 

        
                   
      |
104 | 103 | oveq1d 5884 |
. . . . . . . . . . . . . 14
  
 

                    
                                                  |
105 | 102, 104 | eqtrd 2210 |
. . . . . . . . . . . . 13
  
 

                    
                                                  |
106 | 88, 87, 100 | addassd 7970 |
. . . . . . . . . . . . 13
  
 

                    
                                                  |
107 | 105, 106 | eqtrd 2210 |
. . . . . . . . . . . 12
  
 

                    
                                                  |
108 | 88, 101, 107 | comraddd 8104 |
. . . . . . . . . . 11
  
 

                    
                                     
            |
109 | 85, 86, 93 | subadd23d 8280 |
. . . . . . . . . . . . . . 15
  
 

        
                               
      |
110 | 91, 92, 86 | subsub4d 8289 |
. . . . . . . . . . . . . . . . 17
  
 

        
                   
      |
111 | 92, 86 | addcomd 8098 |
. . . . . . . . . . . . . . . . . 18
  
 

                       |
112 | 111 | oveq2d 5885 |
. . . . . . . . . . . . . . . . 17
  
 

        
                   
      |
113 | 110, 112 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
  
 

        
                   
      |
114 | 113 | oveq2d 5885 |
. . . . . . . . . . . . . . 15
  
 

                                               |
115 | 109, 114 | eqtrd 2210 |
. . . . . . . . . . . . . 14
  
 

        
                                      |
116 | 115 | oveq2d 5885 |
. . . . . . . . . . . . 13
  
 

                                              
            |
117 | 87, 81, 93 | add12d 8114 |
. . . . . . . . . . . . 13
  
 

        
     
                                            |
118 | 86, 92 | addcld 7967 |
. . . . . . . . . . . . . . . 16
  
 

             |
119 | 91, 118 | subcld 8258 |
. . . . . . . . . . . . . . 15
  
 

        
          |
120 | 85, 119 | addcld 7967 |
. . . . . . . . . . . . . 14
  
 

                         |
121 | 85, 81 | addcld 7967 |
. . . . . . . . . . . . . . . 16
  
 

             |
122 | 121, 91, 118 | addsubassd 8278 |
. . . . . . . . . . . . . . 15
  
 

                    
                                      |
123 | 85, 81, 119 | add32d 8115 |
. . . . . . . . . . . . . . 15
  
 

        
                                     
            |
124 | 122, 123 | eqtrd 2210 |
. . . . . . . . . . . . . 14
  
 

                    
                         
            |
125 | 120, 81, 124 | comraddd 8104 |
. . . . . . . . . . . . 13
  
 

                    
                         
            |
126 | 116, 117,
125 | 3eqtr4d 2220 |
. . . . . . . . . . . 12
  
 

        
     
                                     
      |
127 | 126 | oveq1d 5884 |
. . . . . . . . . . 11
  
 

                                            
                          |
128 | 108, 127 | eqtrd 2210 |
. . . . . . . . . 10
  
 

                    
                       
                          |
129 | 128 | oveq2d 5885 |
. . . . . . . . 9
  
 

                                                                      
            |
130 | 99, 129 | eqtrd 2210 |
. . . . . . . 8
  
 

                          
                                           
            |
131 | | binom2sub 10619 |
. . . . . . . . . . 11
 
                         |
132 | 8, 9, 131 | syl2anc 411 |
. . . . . . . . . 10
  
 

                         |
133 | | binom2sub 10619 |
. . . . . . . . . . 11
 
                         |
134 | 13, 9, 133 | syl2anc 411 |
. . . . . . . . . 10
  
 

                         |
135 | 132, 134 | oveq12d 5887 |
. . . . . . . . 9
  
 

                                                   |
136 | 135 | oveq1d 5884 |
. . . . . . . 8
  
 

                              
                                |
137 | | binom2sub 10619 |
. . . . . . . . . . 11
   
                               |
138 | 21, 9, 137 | syl2anc 411 |
. . . . . . . . . 10
  
 

                               |
139 | | binom2 10617 |
. . . . . . . . . . . . 13
 
                         |
140 | 8, 13, 139 | syl2anc 411 |
. . . . . . . . . . . 12
  
 

                         |
141 | 52 | oveq2d 5885 |
. . . . . . . . . . . . 13
  
 

                 |
142 | 69, 36, 37 | adddid 7972 |
. . . . . . . . . . . . 13
  
 

                     |
143 | 141, 142 | eqtrd 2210 |
. . . . . . . . . . . 12
  
 

                   |
144 | 140, 143 | oveq12d 5887 |
. . . . . . . . . . 11
  
 

                                      
      |
145 | 144 | oveq1d 5884 |
. . . . . . . . . 10
  
 

                              
                          |
146 | 138, 145 | eqtrd 2210 |
. . . . . . . . 9
  
 

                  
                          |
147 | 146 | oveq2d 5885 |
. . . . . . . 8
  
 

                                            
            |
148 | 130, 136,
147 | 3eqtr4d 2220 |
. . . . . . 7
  
 

                                     |
149 | 148 | oveq1d 5884 |
. . . . . 6
  
 

                  
                                
             |
150 | 84, 149 | breqtrd 4026 |
. . . . 5
  
 

              
                                  
             |
151 | 22 | sqcld 10637 |
. . . . . 6
  
 

           |
152 | 88, 151, 82 | add32d 8115 |
. . . . 5
  
 

                                                           |
153 | 150, 152 | breqtrd 4026 |
. . . 4
  
 

              
                                                |
154 | | absresq 11071 |
. . . . . . 7
       
             |
155 | 4, 154 | syl 14 |
. . . . . 6
  
 

     
             |
156 | 155 | oveq1d 5884 |
. . . . 5
  
 

                                                       |
157 | | absresq 11071 |
. . . . . 6
       
             |
158 | 28, 157 | syl 14 |
. . . . 5
  
 

     
             |
159 | 156, 158 | oveq12d 5887 |
. . . 4
  
 

                  
                                   
                    |
160 | 1, 12 | readdcld 7977 |
. . . . . . 7
  
 

     |
161 | 160, 3 | resubcld 8328 |
. . . . . 6
  
 

       |
162 | | absresq 11071 |
. . . . . 6
                           |
163 | 161, 162 | syl 14 |
. . . . 5
  
 

                       |
164 | 163 | oveq2d 5885 |
. . . 4
  
 

        
                                                      |
165 | 153, 159,
164 | 3brtr4d 4032 |
. . 3
  
 

                  
                                                        |
166 | 11 | recnd 7976 |
. . . 4
  
 

    
    |
167 | 15 | recnd 7976 |
. . . 4
  
 

    
    |
168 | | binom2 10617 |
. . . 4
     
                                 
          
                        |
169 | 166, 167,
168 | syl2anc 411 |
. . 3
  
 

                         
          
                        |
170 | | binom2 10617 |
. . . 4
                                                           |
171 | 9, 64, 170 | syl2anc 411 |
. . 3
  
 

                                                 |
172 | 165, 169,
171 | 3brtr4d 4032 |
. 2
  
 

                                   |
173 | 11, 15 | readdcld 7977 |
. . 3
  
 

     
           |
174 | 3, 23 | readdcld 7977 |
. . 3
  
 

             |
175 | 10 | absge0d 11177 |
. . . 4
  
 


        |
176 | 14 | absge0d 11177 |
. . . 4
  
 


        |
177 | 11, 15, 175, 176 | addge0d 8469 |
. . 3
  
 


          
     |
178 | 22 | absge0d 11177 |
. . . 4
  
 


          |
179 | 3, 23, 57, 178 | addge0d 8469 |
. . 3
  
 


            |
180 | 173, 174,
177, 179 | le2sqd 10671 |
. 2
  
 

               
         
     
                             |
181 | 172, 180 | mpbird 167 |
1
  
 

     
                     |