Proof of Theorem dquart
Step | Hyp | Ref
| Expression |
1 | | dquart.x |
. . . . . . . . 9
|
2 | 1 | sqcld 13006 |
. . . . . . . 8
|
3 | | dquart.m |
. . . . . . . . . . 11
|
4 | | 2cn 11091 |
. . . . . . . . . . . . 13
|
5 | | dquart.s |
. . . . . . . . . . . . 13
|
6 | | mulcl 10020 |
. . . . . . . . . . . . 13
|
7 | 4, 5, 6 | sylancr 695 |
. . . . . . . . . . . 12
|
8 | 7 | sqcld 13006 |
. . . . . . . . . . 11
|
9 | 3, 8 | eqeltrd 2701 |
. . . . . . . . . 10
|
10 | | dquart.b |
. . . . . . . . . 10
|
11 | 9, 10 | addcld 10059 |
. . . . . . . . 9
|
12 | 11 | halfcld 11277 |
. . . . . . . 8
|
13 | | binom2 12979 |
. . . . . . . 8
|
14 | 2, 12, 13 | syl2anc 693 |
. . . . . . 7
|
15 | | 2t2e4 11177 |
. . . . . . . . . . . 12
|
16 | 15 | oveq2i 6661 |
. . . . . . . . . . 11
|
17 | | 2nn0 11309 |
. . . . . . . . . . . . 13
|
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
|
19 | 1, 18, 18 | expmuld 13011 |
. . . . . . . . . . 11
|
20 | 16, 19 | syl5reqr 2671 |
. . . . . . . . . 10
|
21 | 4 | a1i 11 |
. . . . . . . . . . . 12
|
22 | 21, 2, 12 | mul12d 10245 |
. . . . . . . . . . 11
|
23 | | 2ne0 11113 |
. . . . . . . . . . . . . . 15
|
24 | 23 | a1i 11 |
. . . . . . . . . . . . . 14
|
25 | 11, 21, 24 | divcan2d 10803 |
. . . . . . . . . . . . 13
|
26 | 25 | oveq2d 6666 |
. . . . . . . . . . . 12
|
27 | 2, 11 | mulcomd 10061 |
. . . . . . . . . . . 12
|
28 | 26, 27 | eqtrd 2656 |
. . . . . . . . . . 11
|
29 | 9, 10, 2 | adddird 10065 |
. . . . . . . . . . 11
|
30 | 22, 28, 29 | 3eqtrd 2660 |
. . . . . . . . . 10
|
31 | 20, 30 | oveq12d 6668 |
. . . . . . . . 9
|
32 | | 4nn0 11311 |
. . . . . . . . . . 11
|
33 | | expcl 12878 |
. . . . . . . . . . 11
|
34 | 1, 32, 33 | sylancl 694 |
. . . . . . . . . 10
|
35 | 9, 2 | mulcld 10060 |
. . . . . . . . . 10
|
36 | 10, 2 | mulcld 10060 |
. . . . . . . . . 10
|
37 | 34, 35, 36 | add12d 10262 |
. . . . . . . . 9
|
38 | 31, 37 | eqtrd 2656 |
. . . . . . . 8
|
39 | 38 | oveq1d 6665 |
. . . . . . 7
|
40 | 34, 36 | addcld 10059 |
. . . . . . . 8
|
41 | 12 | sqcld 13006 |
. . . . . . . 8
|
42 | 35, 40, 41 | addassd 10062 |
. . . . . . 7
|
43 | 14, 39, 42 | 3eqtrd 2660 |
. . . . . 6
|
44 | 9 | halfcld 11277 |
. . . . . . . . . . . 12
|
45 | 44, 1 | mulcld 10060 |
. . . . . . . . . . 11
|
46 | | dquart.c |
. . . . . . . . . . . 12
|
47 | | 4cn 11098 |
. . . . . . . . . . . . 13
|
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
|
49 | | 4ne0 11117 |
. . . . . . . . . . . . 13
|
50 | 49 | a1i 11 |
. . . . . . . . . . . 12
|
51 | 46, 48, 50 | divcld 10801 |
. . . . . . . . . . 11
|
52 | 45, 51 | subcld 10392 |
. . . . . . . . . 10
|
53 | | dquart.m0 |
. . . . . . . . . . . . . 14
|
54 | 3, 53 | eqnetrrd 2862 |
. . . . . . . . . . . . 13
|
55 | | sqne0 12930 |
. . . . . . . . . . . . . 14
|
56 | 7, 55 | syl 17 |
. . . . . . . . . . . . 13
|
57 | 54, 56 | mpbid 222 |
. . . . . . . . . . . 12
|
58 | | mulne0b 10668 |
. . . . . . . . . . . . 13
|
59 | 4, 5, 58 | sylancr 695 |
. . . . . . . . . . . 12
|
60 | 57, 59 | mpbird 247 |
. . . . . . . . . . 11
|
61 | 60 | simprd 479 |
. . . . . . . . . 10
|
62 | 52, 5, 21, 61, 24 | divcan5d 10827 |
. . . . . . . . 9
|
63 | 21, 45, 51 | subdid 10486 |
. . . . . . . . . . 11
|
64 | 21, 44, 1 | mulassd 10063 |
. . . . . . . . . . . . 13
|
65 | 9, 21, 24 | divcan2d 10803 |
. . . . . . . . . . . . . 14
|
66 | 65 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
67 | 64, 66 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
68 | 21, 46, 48, 50 | divassd 10836 |
. . . . . . . . . . . . 13
|
69 | 15 | oveq2i 6661 |
. . . . . . . . . . . . . 14
|
70 | 46, 21, 21, 24, 24 | divcan5d 10827 |
. . . . . . . . . . . . . 14
|
71 | 69, 70 | syl5eqr 2670 |
. . . . . . . . . . . . 13
|
72 | 68, 71 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
73 | 67, 72 | oveq12d 6668 |
. . . . . . . . . . 11
|
74 | 63, 73 | eqtrd 2656 |
. . . . . . . . . 10
|
75 | 74 | oveq1d 6665 |
. . . . . . . . 9
|
76 | 62, 75 | eqtr3d 2658 |
. . . . . . . 8
|
77 | 76 | oveq1d 6665 |
. . . . . . 7
|
78 | 9, 1 | mulcld 10060 |
. . . . . . . . 9
|
79 | 46 | halfcld 11277 |
. . . . . . . . 9
|
80 | 78, 79 | subcld 10392 |
. . . . . . . 8
|
81 | 80, 7, 57 | sqdivd 13021 |
. . . . . . 7
|
82 | 9 | sqcld 13006 |
. . . . . . . . . . 11
|
83 | 82, 2 | mulcld 10060 |
. . . . . . . . . 10
|
84 | 78, 46 | mulcld 10060 |
. . . . . . . . . 10
|
85 | 83, 84 | subcld 10392 |
. . . . . . . . 9
|
86 | 46 | sqcld 13006 |
. . . . . . . . . 10
|
87 | 86, 48, 50 | divcld 10801 |
. . . . . . . . 9
|
88 | 85, 87, 9, 53 | divdird 10839 |
. . . . . . . 8
|
89 | | binom2sub 12981 |
. . . . . . . . . . 11
|
90 | 78, 79, 89 | syl2anc 693 |
. . . . . . . . . 10
|
91 | 9, 1 | sqmuld 13020 |
. . . . . . . . . . . 12
|
92 | 21, 78, 79 | mul12d 10245 |
. . . . . . . . . . . . 13
|
93 | 46, 21, 24 | divcan2d 10803 |
. . . . . . . . . . . . . 14
|
94 | 93 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
95 | 92, 94 | eqtrd 2656 |
. . . . . . . . . . . 12
|
96 | 91, 95 | oveq12d 6668 |
. . . . . . . . . . 11
|
97 | 46, 21, 24 | sqdivd 13021 |
. . . . . . . . . . . 12
|
98 | | sq2 12960 |
. . . . . . . . . . . . 13
|
99 | 98 | oveq2i 6661 |
. . . . . . . . . . . 12
|
100 | 97, 99 | syl6eq 2672 |
. . . . . . . . . . 11
|
101 | 96, 100 | oveq12d 6668 |
. . . . . . . . . 10
|
102 | 90, 101 | eqtr2d 2657 |
. . . . . . . . 9
|
103 | 102, 3 | oveq12d 6668 |
. . . . . . . 8
|
104 | 83, 84, 9, 53 | divsubdird 10840 |
. . . . . . . . . . 11
|
105 | 82, 2, 9, 53 | div23d 10838 |
. . . . . . . . . . . . 13
|
106 | 9 | sqvald 13005 |
. . . . . . . . . . . . . . . 16
|
107 | 106 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
108 | 9, 9, 53 | divcan3d 10806 |
. . . . . . . . . . . . . . 15
|
109 | 107, 108 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
110 | 109 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
111 | 105, 110 | eqtrd 2656 |
. . . . . . . . . . . 12
|
112 | 9, 1, 46 | mul32d 10246 |
. . . . . . . . . . . . . . 15
|
113 | 9, 46, 1 | mulassd 10063 |
. . . . . . . . . . . . . . 15
|
114 | 112, 113 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
115 | 114 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
116 | 46, 1 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
117 | 116, 9, 53 | divcan3d 10806 |
. . . . . . . . . . . . 13
|
118 | 115, 117 | eqtrd 2656 |
. . . . . . . . . . . 12
|
119 | 111, 118 | oveq12d 6668 |
. . . . . . . . . . 11
|
120 | 104, 119 | eqtrd 2656 |
. . . . . . . . . 10
|
121 | 120 | oveq1d 6665 |
. . . . . . . . 9
|
122 | 87, 9, 53 | divcld 10801 |
. . . . . . . . . 10
|
123 | 35, 116, 122 | subsubd 10420 |
. . . . . . . . 9
|
124 | 121, 123 | eqtr4d 2659 |
. . . . . . . 8
|
125 | 88, 103, 124 | 3eqtr3d 2664 |
. . . . . . 7
|
126 | 77, 81, 125 | 3eqtrd 2660 |
. . . . . 6
|
127 | 43, 126 | oveq12d 6668 |
. . . . 5
|
128 | 40, 41 | addcld 10059 |
. . . . . 6
|
129 | 116, 122 | subcld 10392 |
. . . . . 6
|
130 | 35, 128, 129 | pnncand 10431 |
. . . . 5
|
131 | 122 | negcld 10379 |
. . . . . . 7
|
132 | 40, 41, 116, 131 | add4d 10264 |
. . . . . 6
|
133 | 116, 122 | negsubd 10398 |
. . . . . . 7
|
134 | 133 | oveq2d 6666 |
. . . . . 6
|
135 | 41, 122 | negsubd 10398 |
. . . . . . . . 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 24579 |
. . . . . . . . 9
|
141 | 135, 140 | eqtrd 2656 |
. . . . . . . 8
|
142 | 141 | oveq2d 6666 |
. . . . . . 7
|
143 | 40, 116, 138 | addassd 10062 |
. . . . . . 7
|
144 | 142, 143 | eqtrd 2656 |
. . . . . 6
|
145 | 132, 134,
144 | 3eqtr3d 2664 |
. . . . 5
|
146 | 127, 130,
145 | 3eqtrd 2660 |
. . . 4
|
147 | 2, 12 | addcld 10059 |
. . . . 5
|
148 | 52, 5, 61 | divcld 10801 |
. . . . 5
|
149 | | subsq 12972 |
. . . . 5
|
150 | 147, 148,
149 | syl2anc 693 |
. . . 4
|
151 | 146, 150 | eqtr3d 2658 |
. . 3
|
152 | 151 | eqeq1d 2624 |
. 2
|
153 | 147, 148 | addcld 10059 |
. . 3
|
154 | 147, 148 | subcld 10392 |
. . 3
|
155 | 153, 154 | mul0ord 10677 |
. 2
|
156 | 10, 46, 1, 5, 3, 53,
136, 137 | dquartlem1 24578 |
. . 3
|
157 | 5 | negcld 10379 |
. . . . 5
|
158 | | sqneg 12923 |
. . . . . . . 8
|
159 | 7, 158 | syl 17 |
. . . . . . 7
|
160 | 3, 159 | eqtr4d 2659 |
. . . . . 6
|
161 | | mulneg2 10467 |
. . . . . . . 8
|
162 | 4, 5, 161 | sylancr 695 |
. . . . . . 7
|
163 | 162 | oveq1d 6665 |
. . . . . 6
|
164 | 160, 163 | eqtr4d 2659 |
. . . . 5
|
165 | | dquart.j |
. . . . 5
|
166 | | dquart.j2 |
. . . . . 6
|
167 | 5 | sqcld 13006 |
. . . . . . . . 9
|
168 | 167 | negcld 10379 |
. . . . . . . 8
|
169 | 10 | halfcld 11277 |
. . . . . . . 8
|
170 | 168, 169 | subcld 10392 |
. . . . . . 7
|
171 | 51, 5, 61 | divcld 10801 |
. . . . . . 7
|
172 | 170, 171 | negsubd 10398 |
. . . . . 6
|
173 | | sqneg 12923 |
. . . . . . . . . . 11
|
174 | 5, 173 | syl 17 |
. . . . . . . . . 10
|
175 | 174 | eqcomd 2628 |
. . . . . . . . 9
|
176 | 175 | negeqd 10275 |
. . . . . . . 8
|
177 | 176 | oveq1d 6665 |
. . . . . . 7
|
178 | 51, 5, 61 | divneg2d 10815 |
. . . . . . 7
|
179 | 177, 178 | oveq12d 6668 |
. . . . . 6
|
180 | 166, 172,
179 | 3eqtr2d 2662 |
. . . . 5
|
181 | 10, 46, 1, 157, 164, 53, 165, 180 | dquartlem1 24578 |
. . . 4
|
182 | 52, 5, 61 | divneg2d 10815 |
. . . . . . 7
|
183 | 182 | oveq2d 6666 |
. . . . . 6
|
184 | 147, 148 | negsubd 10398 |
. . . . . 6
|
185 | 183, 184 | eqtr3d 2658 |
. . . . 5
|
186 | 185 | eqeq1d 2624 |
. . . 4
|
187 | 5 | negnegd 10383 |
. . . . . . 7
|
188 | 187 | oveq1d 6665 |
. . . . . 6
|
189 | 188 | eqeq2d 2632 |
. . . . 5
|
190 | 187 | oveq1d 6665 |
. . . . . 6
|
191 | 190 | eqeq2d 2632 |
. . . . 5
|
192 | 189, 191 | orbi12d 746 |
. . . 4
|
193 | 181, 186,
192 | 3bitr3d 298 |
. . 3
|
194 | 156, 193 | orbi12d 746 |
. 2
|
195 | 152, 155,
194 | 3bitrd 294 |
1
|