Proof of Theorem dquart
Step | Hyp | Ref
| Expression |
1 | | dquart.x |
. . . . . . . . 9
   |
2 | 1 | sqcld 12452 |
. . . . . . . 8
       |
3 | | dquart.m |
. . . . . . . . . . 11
         |
4 | | 2cn 10702 |
. . . . . . . . . . . . 13
 |
5 | | dquart.s |
. . . . . . . . . . . . 13
   |
6 | | mulcl 9641 |
. . . . . . . . . . . . 13
 
     |
7 | 4, 5, 6 | sylancr 676 |
. . . . . . . . . . . 12
     |
8 | 7 | sqcld 12452 |
. . . . . . . . . . 11
         |
9 | 3, 8 | eqeltrd 2549 |
. . . . . . . . . 10
   |
10 | | dquart.b |
. . . . . . . . . 10
   |
11 | 9, 10 | addcld 9680 |
. . . . . . . . 9
     |
12 | 11 | halfcld 10880 |
. . . . . . . 8
       |
13 | | binom2 12427 |
. . . . . . . 8
                                                           |
14 | 2, 12, 13 | syl2anc 673 |
. . . . . . 7
                                                 |
15 | | 2t2e4 10782 |
. . . . . . . . . . . 12
   |
16 | 15 | oveq2i 6319 |
. . . . . . . . . . 11
           |
17 | | 2nn0 10910 |
. . . . . . . . . . . . 13
 |
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
   |
19 | 1, 18, 18 | expmuld 12457 |
. . . . . . . . . . 11
                 |
20 | 16, 19 | syl5reqr 2520 |
. . . . . . . . . 10
               |
21 | 4 | a1i 11 |
. . . . . . . . . . . 12
   |
22 | 21, 2, 12 | mul12d 9860 |
. . . . . . . . . . 11
                           |
23 | | 2ne0 10724 |
. . . . . . . . . . . . . . 15
 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . 14
   |
25 | 11, 21, 24 | divcan2d 10407 |
. . . . . . . . . . . . 13
           |
26 | 25 | oveq2d 6324 |
. . . . . . . . . . . 12
                       |
27 | 2, 11 | mulcomd 9682 |
. . . . . . . . . . . 12
      
            |
28 | 26, 27 | eqtrd 2505 |
. . . . . . . . . . 11
                       |
29 | 9, 10, 2 | adddird 9686 |
. . . . . . . . . . 11
                         |
30 | 22, 28, 29 | 3eqtrd 2509 |
. . . . . . . . . 10
                             |
31 | 20, 30 | oveq12d 6326 |
. . . . . . . . 9
                                             |
32 | | 4nn0 10912 |
. . . . . . . . . . 11
 |
33 | | expcl 12328 |
. . . . . . . . . . 11
 
       |
34 | 1, 32, 33 | sylancl 675 |
. . . . . . . . . 10
       |
35 | 9, 2 | mulcld 9681 |
. . . . . . . . . 10
         |
36 | 10, 2 | mulcld 9681 |
. . . . . . . . . 10
         |
37 | 34, 35, 36 | add12d 9876 |
. . . . . . . . 9
                                           |
38 | 31, 37 | eqtrd 2505 |
. . . . . . . 8
                                             |
39 | 38 | oveq1d 6323 |
. . . . . . 7
                                                                 |
40 | 34, 36 | addcld 9680 |
. . . . . . . 8
               |
41 | 12 | sqcld 12452 |
. . . . . . . 8
           |
42 | 35, 40, 41 | addassd 9683 |
. . . . . . 7
                                                               |
43 | 14, 39, 42 | 3eqtrd 2509 |
. . . . . 6
                                               |
44 | 9 | halfcld 10880 |
. . . . . . . . . . . 12
     |
45 | 44, 1 | mulcld 9681 |
. . . . . . . . . . 11
       |
46 | | dquart.c |
. . . . . . . . . . . 12
   |
47 | | 4cn 10709 |
. . . . . . . . . . . . 13
 |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
   |
49 | | 4ne0 10728 |
. . . . . . . . . . . . 13
 |
50 | 49 | a1i 11 |
. . . . . . . . . . . 12
   |
51 | 46, 48, 50 | divcld 10405 |
. . . . . . . . . . 11
     |
52 | 45, 51 | subcld 10005 |
. . . . . . . . . 10
           |
53 | | dquart.m0 |
. . . . . . . . . . . . . 14
   |
54 | 3, 53 | eqnetrrd 2711 |
. . . . . . . . . . . . 13
         |
55 | | sqne0 12379 |
. . . . . . . . . . . . . 14
               |
56 | 7, 55 | syl 17 |
. . . . . . . . . . . . 13
             |
57 | 54, 56 | mpbid 215 |
. . . . . . . . . . . 12
     |
58 | | mulne0b 10275 |
. . . . . . . . . . . . 13
 
   
     |
59 | 4, 5, 58 | sylancr 676 |
. . . . . . . . . . . 12
   
     |
60 | 57, 59 | mpbird 240 |
. . . . . . . . . . 11
 
   |
61 | 60 | simprd 470 |
. . . . . . . . . 10
   |
62 | 52, 5, 21, 61, 24 | divcan5d 10431 |
. . . . . . . . 9
                           |
63 | 21, 45, 51 | subdid 10095 |
. . . . . . . . . . 11
                         |
64 | 21, 44, 1 | mulassd 9684 |
. . . . . . . . . . . . 13
               |
65 | 9, 21, 24 | divcan2d 10407 |
. . . . . . . . . . . . . 14
       |
66 | 65 | oveq1d 6323 |
. . . . . . . . . . . . 13
           |
67 | 64, 66 | eqtr3d 2507 |
. . . . . . . . . . . 12
           |
68 | 21, 46, 48, 50 | divassd 10440 |
. . . . . . . . . . . . 13
           |
69 | 15 | oveq2i 6319 |
. . . . . . . . . . . . . 14
           |
70 | 46, 21, 21, 24, 24 | divcan5d 10431 |
. . . . . . . . . . . . . 14
           |
71 | 69, 70 | syl5eqr 2519 |
. . . . . . . . . . . . 13
         |
72 | 68, 71 | eqtr3d 2507 |
. . . . . . . . . . . 12
         |
73 | 67, 72 | oveq12d 6326 |
. . . . . . . . . . 11
                     |
74 | 63, 73 | eqtrd 2505 |
. . . . . . . . . 10
                   |
75 | 74 | oveq1d 6323 |
. . . . . . . . 9
                           |
76 | 62, 75 | eqtr3d 2507 |
. . . . . . . 8
       
               |
77 | 76 | oveq1d 6323 |
. . . . . . 7
                               |
78 | 9, 1 | mulcld 9681 |
. . . . . . . . 9
     |
79 | 46 | halfcld 10880 |
. . . . . . . . 9
     |
80 | 78, 79 | subcld 10005 |
. . . . . . . 8
         |
81 | 80, 7, 57 | sqdivd 12467 |
. . . . . . 7
                                   |
82 | 9 | sqcld 12452 |
. . . . . . . . . . 11
       |
83 | 82, 2 | mulcld 9681 |
. . . . . . . . . 10
             |
84 | 78, 46 | mulcld 9681 |
. . . . . . . . . 10
       |
85 | 83, 84 | subcld 10005 |
. . . . . . . . 9
                   |
86 | 46 | sqcld 12452 |
. . . . . . . . . 10
       |
87 | 86, 48, 50 | divcld 10405 |
. . . . . . . . 9
         |
88 | 85, 87, 9, 53 | divdird 10443 |
. . . . . . . 8
                                                         |
89 | | binom2sub 12429 |
. . . . . . . . . . 11
    
                                      |
90 | 78, 79, 89 | syl2anc 673 |
. . . . . . . . . 10
     
                               |
91 | 9, 1 | sqmuld 12466 |
. . . . . . . . . . . 12
                   |
92 | 21, 78, 79 | mul12d 9860 |
. . . . . . . . . . . . 13
                   |
93 | 46, 21, 24 | divcan2d 10407 |
. . . . . . . . . . . . . 14
       |
94 | 93 | oveq2d 6324 |
. . . . . . . . . . . . 13
               |
95 | 92, 94 | eqtrd 2505 |
. . . . . . . . . . . 12
               |
96 | 91, 95 | oveq12d 6326 |
. . . . . . . . . . 11
                                   |
97 | 46, 21, 24 | sqdivd 12467 |
. . . . . . . . . . . 12
                   |
98 | | sq2 12409 |
. . . . . . . . . . . . 13
     |
99 | 98 | oveq2i 6319 |
. . . . . . . . . . . 12
                 |
100 | 97, 99 | syl6eq 2521 |
. . . . . . . . . . 11
               |
101 | 96, 100 | oveq12d 6326 |
. . . . . . . . . 10
                                                   |
102 | 90, 101 | eqtr2d 2506 |
. . . . . . . . 9
                                     |
103 | 102, 3 | oveq12d 6326 |
. . . . . . . 8
                                               |
104 | 83, 84, 9, 53 | divsubdird 10444 |
. . . . . . . . . . 11
                                         |
105 | 82, 2, 9, 53 | div23d 10442 |
. . . . . . . . . . . . 13
                           |
106 | 9 | sqvald 12451 |
. . . . . . . . . . . . . . . 16
         |
107 | 106 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
             |
108 | 9, 9, 53 | divcan3d 10410 |
. . . . . . . . . . . . . . 15
       |
109 | 107, 108 | eqtrd 2505 |
. . . . . . . . . . . . . 14
         |
110 | 109 | oveq1d 6323 |
. . . . . . . . . . . . 13
                     |
111 | 105, 110 | eqtrd 2505 |
. . . . . . . . . . . 12
                     |
112 | 9, 1, 46 | mul32d 9861 |
. . . . . . . . . . . . . . 15
           |
113 | 9, 46, 1 | mulassd 9684 |
. . . . . . . . . . . . . . 15
           |
114 | 112, 113 | eqtrd 2505 |
. . . . . . . . . . . . . 14
           |
115 | 114 | oveq1d 6323 |
. . . . . . . . . . . . 13
               |
116 | 46, 1 | mulcld 9681 |
. . . . . . . . . . . . . 14
     |
117 | 116, 9, 53 | divcan3d 10410 |
. . . . . . . . . . . . 13
   
       |
118 | 115, 117 | eqtrd 2505 |
. . . . . . . . . . . 12
           |
119 | 111, 118 | oveq12d 6326 |
. . . . . . . . . . 11
                                 |
120 | 104, 119 | eqtrd 2505 |
. . . . . . . . . 10
                               |
121 | 120 | oveq1d 6323 |
. . . . . . . . 9
                                                   |
122 | 87, 9, 53 | divcld 10405 |
. . . . . . . . . 10
           |
123 | 35, 116, 122 | subsubd 10033 |
. . . . . . . . 9
                                           |
124 | 121, 123 | eqtr4d 2508 |
. . . . . . . 8
                                                   |
125 | 88, 103, 124 | 3eqtr3d 2513 |
. . . . . . 7
                                         |
126 | 77, 81, 125 | 3eqtrd 2509 |
. . . . . 6
                                     |
127 | 43, 126 | oveq12d 6326 |
. . . . 5
                       
                                                             |
128 | 40, 41 | addcld 9680 |
. . . . . 6
                         |
129 | 116, 122 | subcld 10005 |
. . . . . 6
               |
130 | 35, 128, 129 | pnncand 10044 |
. . . . 5
                                                                                           |
131 | 122 | negcld 9992 |
. . . . . . 7
            |
132 | 40, 41, 116, 131 | add4d 9878 |
. . . . . 6
                                                                             |
133 | 116, 122 | negsubd 10011 |
. . . . . . 7
                            |
134 | 133 | oveq2d 6324 |
. . . . . 6
                                                                            |
135 | 41, 122 | negsubd 10011 |
. . . . . . . . 9
                                        |
136 | | dquart.i |
. . . . . . . . . 10
   |
137 | | dquart.i2 |
. . . . . . . . . 10
                      |
138 | | dquart.d |
. . . . . . . . . 10
   |
139 | | dquart.3 |
. . . . . . . . . 10
                                    |
140 | 10, 46, 1, 5, 3, 53,
136, 137, 138, 139 | dquartlem2 23857 |
. . . . . . . . 9
                     |
141 | 135, 140 | eqtrd 2505 |
. . . . . . . 8
                      |
142 | 141 | oveq2d 6324 |
. . . . . . 7
                                                          |
143 | 40, 116, 138 | addassd 9683 |
. . . . . . 7
                                       |
144 | 142, 143 | eqtrd 2505 |
. . . . . 6
                                                          |
145 | 132, 134,
144 | 3eqtr3d 2513 |
. . . . 5
                                                         |
146 | 127, 130,
145 | 3eqtrd 2509 |
. . . 4
                       
                           |
147 | 2, 12 | addcld 9680 |
. . . . 5
             |
148 | 52, 5, 61 | divcld 10405 |
. . . . 5
       
     |
149 | | subsq 12420 |
. . . . 5
                  
                                                                          
       |
150 | 147, 148,
149 | syl2anc 673 |
. . . 4
                       
                                               
       |
151 | 146, 150 | eqtr3d 2507 |
. . 3
                                                                   |
152 | 151 | eqeq1d 2473 |
. 2
                                                            
        |
153 | 147, 148 | addcld 9680 |
. . 3
                         |
154 | 147, 148 | subcld 10005 |
. . 3
                         |
155 | 153, 154 | mul0ord 10284 |
. 2
                                                                                                 |
156 | 10, 46, 1, 5, 3, 53,
136, 137 | dquartlem1 23856 |
. . 3
                   
               |
157 | 5 | negcld 9992 |
. . . . 5
    |
158 | | sqneg 12373 |
. . . . . . . 8
                  |
159 | 7, 158 | syl 17 |
. . . . . . 7
                |
160 | 3, 159 | eqtr4d 2508 |
. . . . . 6
          |
161 | | mulneg2 10077 |
. . . . . . . 8
 
         |
162 | 4, 5, 161 | sylancr 676 |
. . . . . . 7
         |
163 | 162 | oveq1d 6323 |
. . . . . 6
                 |
164 | 160, 163 | eqtr4d 2508 |
. . . . 5
          |
165 | | dquart.j |
. . . . 5
   |
166 | | dquart.j2 |
. . . . . 6
                      |
167 | 5 | sqcld 12452 |
. . . . . . . . 9
       |
168 | 167 | negcld 9992 |
. . . . . . . 8
        |
169 | 10 | halfcld 10880 |
. . . . . . . 8
     |
170 | 168, 169 | subcld 10005 |
. . . . . . 7
       
    |
171 | 51, 5, 61 | divcld 10405 |
. . . . . . 7
       |
172 | 170, 171 | negsubd 10011 |
. . . . . 6
        
               
         |
173 | | sqneg 12373 |
. . . . . . . . . . 11
            |
174 | 5, 173 | syl 17 |
. . . . . . . . . 10
            |
175 | 174 | eqcomd 2477 |
. . . . . . . . 9
            |
176 | 175 | negeqd 9889 |
. . . . . . . 8
              |
177 | 176 | oveq1d 6323 |
. . . . . . 7
       
         
    |
178 | 51, 5, 61 | divneg2d 10419 |
. . . . . . 7
             |
179 | 177, 178 | oveq12d 6326 |
. . . . . 6
        
                
          |
180 | 166, 172,
179 | 3eqtr2d 2511 |
. . . . 5
             
          |
181 | 10, 46, 1, 157, 164, 53, 165, 180 | dquartlem1 23856 |
. . . 4
                   
                  |
182 | 52, 5, 61 | divneg2d 10419 |
. . . . . . 7
                         |
183 | 182 | oveq2d 6324 |
. . . . . 6
                   
                             |
184 | 147, 148 | negsubd 10011 |
. . . . . 6
                   
                            |
185 | 183, 184 | eqtr3d 2507 |
. . . . 5
                                         
      |
186 | 185 | eqeq1d 2473 |
. . . 4
                   
                              |
187 | 5 | negnegd 9996 |
. . . . . . 7
     |
188 | 187 | oveq1d 6323 |
. . . . . 6
         |
189 | 188 | eqeq2d 2481 |
. . . . 5
     

    |
190 | 187 | oveq1d 6323 |
. . . . . 6
         |
191 | 190 | eqeq2d 2481 |
. . . . 5
     

    |
192 | 189, 191 | orbi12d 724 |
. . . 4
           
         |
193 | 181, 186,
192 | 3bitr3d 291 |
. . 3
                   
             |
194 | 156, 193 | orbi12d 724 |
. 2
                                               
 
                 |
195 | 152, 155,
194 | 3bitrd 287 |
1
                                       |