Proof of Theorem quart1lem
Step | Hyp | Ref
| Expression |
1 | | quart1.c |
. . . . . . . . 9
   |
2 | | quart1.a |
. . . . . . . . . . 11
   |
3 | | quart1.b |
. . . . . . . . . . 11
   |
4 | 2, 3 | mulcld 9663 |
. . . . . . . . . 10
     |
5 | 4 | halfcld 10857 |
. . . . . . . . 9
       |
6 | 1, 5 | subcld 9986 |
. . . . . . . 8
         |
7 | | 3nn0 10887 |
. . . . . . . . . 10
 |
8 | | expcl 12290 |
. . . . . . . . . 10
 
       |
9 | 2, 7, 8 | sylancl 668 |
. . . . . . . . 9
       |
10 | | 8cn 10695 |
. . . . . . . . . 10
 |
11 | 10 | a1i 11 |
. . . . . . . . 9
   |
12 | | 8nn 10773 |
. . . . . . . . . . 11
 |
13 | 12 | nnne0i 10644 |
. . . . . . . . . 10
 |
14 | 13 | a1i 11 |
. . . . . . . . 9
   |
15 | 9, 11, 14 | divcld 10383 |
. . . . . . . 8
         |
16 | | 4cn 10687 |
. . . . . . . . . 10
 |
17 | 16 | a1i 11 |
. . . . . . . . 9
   |
18 | | 4ne0 10706 |
. . . . . . . . . 10
 |
19 | 18 | a1i 11 |
. . . . . . . . 9
   |
20 | 2, 17, 19 | divcld 10383 |
. . . . . . . 8
     |
21 | 6, 15, 20 | adddird 9668 |
. . . . . . 7
                                           |
22 | | quart1.q |
. . . . . . . 8
                 |
23 | 22 | oveq1d 6305 |
. . . . . . 7
                         |
24 | 1, 2, 17, 19 | divassd 10418 |
. . . . . . . . . 10
           |
25 | 2 | sqvald 12413 |
. . . . . . . . . . . . . . 15
         |
26 | 25 | oveq1d 6305 |
. . . . . . . . . . . . . 14
             |
27 | 2, 2, 3 | mul32d 9843 |
. . . . . . . . . . . . . 14
           |
28 | 26, 27 | eqtrd 2485 |
. . . . . . . . . . . . 13
             |
29 | 28 | oveq1d 6305 |
. . . . . . . . . . . 12
                 |
30 | | 2cn 10680 |
. . . . . . . . . . . . . 14
 |
31 | | 4t2e8 10763 |
. . . . . . . . . . . . . 14
   |
32 | 16, 30, 31 | mulcomli 9650 |
. . . . . . . . . . . . 13
   |
33 | 32 | oveq2i 6301 |
. . . . . . . . . . . 12
               |
34 | 29, 33 | syl6eqr 2503 |
. . . . . . . . . . 11
                   |
35 | 30 | a1i 11 |
. . . . . . . . . . . 12
   |
36 | | 2ne0 10702 |
. . . . . . . . . . . . 13
 |
37 | 36 | a1i 11 |
. . . . . . . . . . . 12
   |
38 | 4, 35, 2, 17, 37, 19 | divmuldivd 10424 |
. . . . . . . . . . 11
                   |
39 | 34, 38 | eqtr4d 2488 |
. . . . . . . . . 10
                   |
40 | 24, 39 | oveq12d 6308 |
. . . . . . . . 9
                               |
41 | 1, 5, 20 | subdird 10075 |
. . . . . . . . 9
                           |
42 | 40, 41 | eqtr4d 2488 |
. . . . . . . 8
                           |
43 | | df-4 10670 |
. . . . . . . . . . . . . 14
   |
44 | 43 | oveq2i 6301 |
. . . . . . . . . . . . 13
           |
45 | | expp1 12279 |
. . . . . . . . . . . . . 14
 
               |
46 | 2, 7, 45 | sylancl 668 |
. . . . . . . . . . . . 13
               |
47 | 44, 46 | syl5eq 2497 |
. . . . . . . . . . . 12
             |
48 | 47 | oveq1d 6305 |
. . . . . . . . . . 11
                 |
49 | 9, 2, 11, 14 | div23d 10420 |
. . . . . . . . . . 11
                   |
50 | 48, 49 | eqtrd 2485 |
. . . . . . . . . 10
                 |
51 | 50 | oveq1d 6305 |
. . . . . . . . 9
                     |
52 | 15, 2, 17, 19 | divassd 10418 |
. . . . . . . . 9
                       |
53 | 51, 52 | eqtrd 2485 |
. . . . . . . 8
                     |
54 | 42, 53 | oveq12d 6308 |
. . . . . . 7
                                                 |
55 | 21, 23, 54 | 3eqtr4d 2495 |
. . . . . 6
                               |
56 | 1, 2 | mulcld 9663 |
. . . . . . . 8
     |
57 | 56, 17, 19 | divcld 10383 |
. . . . . . 7
       |
58 | 2 | sqcld 12414 |
. . . . . . . . 9
       |
59 | 58, 3 | mulcld 9663 |
. . . . . . . 8
         |
60 | 59, 11, 14 | divcld 10383 |
. . . . . . 7
           |
61 | | 4nn0 10888 |
. . . . . . . . . 10
 |
62 | | expcl 12290 |
. . . . . . . . . 10
 
       |
63 | 2, 61, 62 | sylancl 668 |
. . . . . . . . 9
       |
64 | 63, 11, 14 | divcld 10383 |
. . . . . . . 8
         |
65 | 64, 17, 19 | divcld 10383 |
. . . . . . 7
           |
66 | 57, 60, 65 | subadd23d 10008 |
. . . . . 6
                                                   |
67 | 65, 60 | subcld 9986 |
. . . . . . 7
                     |
68 | 57, 67 | addcomd 9835 |
. . . . . 6
                                                   |
69 | 55, 66, 68 | 3eqtrd 2489 |
. . . . 5
                               |
70 | | quart1.r |
. . . . . 6
                ;    ;;            |
71 | | quart1.d |
. . . . . . 7
   |
72 | | 1nn0 10885 |
. . . . . . . . . . . 12
 |
73 | | 6nn 10771 |
. . . . . . . . . . . 12
 |
74 | 72, 73 | decnncl 11064 |
. . . . . . . . . . 11
;  |
75 | 74 | nncni 10619 |
. . . . . . . . . 10
;  |
76 | 75 | a1i 11 |
. . . . . . . . 9
 ;   |
77 | 74 | nnne0i 10644 |
. . . . . . . . . 10
;  |
78 | 77 | a1i 11 |
. . . . . . . . 9
 ;   |
79 | 59, 76, 78 | divcld 10383 |
. . . . . . . 8
        ;    |
80 | | 3cn 10684 |
. . . . . . . . . 10
 |
81 | | 2nn0 10886 |
. . . . . . . . . . . . 13
 |
82 | | 5nn0 10889 |
. . . . . . . . . . . . 13
 |
83 | 81, 82 | deccl 11065 |
. . . . . . . . . . . 12
;  |
84 | 83, 73 | decnncl 11064 |
. . . . . . . . . . 11
;;   |
85 | 84 | nncni 10619 |
. . . . . . . . . 10
;;   |
86 | 84 | nnne0i 10644 |
. . . . . . . . . 10
;;   |
87 | 80, 85, 86 | divcli 10349 |
. . . . . . . . 9
 ;;    |
88 | | mulcl 9623 |
. . . . . . . . 9
   ;;          ;;          |
89 | 87, 63, 88 | sylancr 669 |
. . . . . . . 8
   ;;          |
90 | 79, 89 | subcld 9986 |
. . . . . . 7
         ;    ;;           |
91 | 71, 90, 57 | addsubd 10007 |
. . . . . 6
           ;    ;;                              ;    ;;            |
92 | 70, 91 | eqtr4d 2488 |
. . . . 5
          
;    ;;                 |
93 | 69, 92 | oveq12d 6308 |
. . . 4
   
                                      ;    ;;                  |
94 | 71, 90 | addcld 9662 |
. . . . 5
          ;    ;;            |
95 | 67, 57, 94 | ppncand 10026 |
. . . 4
                                    ;    ;;                                            ;    ;;             |
96 | 67, 71, 90 | add12d 9856 |
. . . . 5
                            
;    ;;                                       ;    ;;             |
97 | 60, 89 | addcld 9662 |
. . . . . . . 8
            ;;           |
98 | 65, 79 | addcld 9662 |
. . . . . . . 8
                
;     |
99 | 97, 98 | negsubdi2d 10002 |
. . . . . . 7
              ;;                         ;                     ;              ;;            |
100 | 65, 79 | addcomd 9835 |
. . . . . . . . . 10
                
;           ;             |
101 | 100 | oveq2d 6306 |
. . . . . . . . 9
             ;;                         ;                ;;                 ;              |
102 | 60, 89, 79, 65 | addsub4d 10033 |
. . . . . . . . 9
             ;;                 ;                             ;      ;;                    |
103 | 80 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
104 | 85 | a1i 11 |
. . . . . . . . . . . . . . . 16
 ;;    |
105 | 86 | a1i 11 |
. . . . . . . . . . . . . . . 16
 ;;    |
106 | 103, 63, 104, 105 | divassd 10418 |
. . . . . . . . . . . . . . 15
        ;;         ;;      |
107 | 103, 63, 104, 105 | div23d 10420 |
. . . . . . . . . . . . . . 15
        ;;     ;;          |
108 | | 1p2e3 10734 |
. . . . . . . . . . . . . . . . . 18
   |
109 | 108 | oveq1i 6300 |
. . . . . . . . . . . . . . . . 17
        ;;          ;;     |
110 | | 1cnd 9659 |
. . . . . . . . . . . . . . . . . 18
   |
111 | 63, 104, 105 | divcld 10383 |
. . . . . . . . . . . . . . . . . 18
      ;;     |
112 | 110, 35, 111 | adddird 9668 |
. . . . . . . . . . . . . . . . 17
         ;;           ;;          ;;       |
113 | 109, 112 | syl5eqr 2499 |
. . . . . . . . . . . . . . . 16
       ;;           ;;          ;;       |
114 | 111 | mulid2d 9661 |
. . . . . . . . . . . . . . . . 17
       ;;         ;;     |
115 | 114 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
        ;;          ;;           ;;         ;;       |
116 | 113, 115 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
       ;;          ;;         ;;       |
117 | 106, 107,
116 | 3eqtr3d 2493 |
. . . . . . . . . . . . . 14
   ;;              ;;         ;;       |
118 | 43 | oveq1i 6300 |
. . . . . . . . . . . . . . . 16
                           |
119 | 65, 17, 19 | divcld 10383 |
. . . . . . . . . . . . . . . . 17
             |
120 | 103, 110,
119 | adddird 9668 |
. . . . . . . . . . . . . . . 16
                                           |
121 | 118, 120 | syl5eq 2497 |
. . . . . . . . . . . . . . 15
                                         |
122 | 65, 17, 19 | divcan2d 10385 |
. . . . . . . . . . . . . . 15
                       |
123 | 119 | mulid2d 9661 |
. . . . . . . . . . . . . . . . 17
                         |
124 | 64, 17, 17, 19, 19 | divdiv1d 10414 |
. . . . . . . . . . . . . . . . . 18
                       |
125 | | 4t4e16 11124 |
. . . . . . . . . . . . . . . . . . 19
  ;  |
126 | 125 | oveq2i 6301 |
. . . . . . . . . . . . . . . . . 18
                 ;   |
127 | 124, 126 | syl6eq 2501 |
. . . . . . . . . . . . . . . . 17
                  ;    |
128 | 63, 11, 76, 14, 78 | divdiv1d 10414 |
. . . . . . . . . . . . . . . . . 18
        ;        ;     |
129 | 10, 75 | mulcli 9648 |
. . . . . . . . . . . . . . . . . . . . 21
 ;   |
130 | 129 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
  ;    |
131 | 10, 75, 13, 77 | mulne0i 10255 |
. . . . . . . . . . . . . . . . . . . . 21
 ;   |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
  ;    |
133 | 63, 130, 132 | divcld 10383 |
. . . . . . . . . . . . . . . . . . 19
       ;     |
134 | 133, 35, 37 | divcan2d 10385 |
. . . . . . . . . . . . . . . . . 18
         ;           ;     |
135 | 63, 130, 35, 132, 37 | divdiv1d 10414 |
. . . . . . . . . . . . . . . . . . . 20
        ;           ;      |
136 | 10, 75, 30 | mul32i 9829 |
. . . . . . . . . . . . . . . . . . . . . 22
  ;      ;   |
137 | | 2exp4 15057 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    ;  |
138 | | 8t2e16 11139 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  ;  |
139 | 137, 138 | eqtr4i 2476 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
140 | 139, 137 | oveq12i 6302 |
. . . . . . . . . . . . . . . . . . . . . 22
             ;   |
141 | | 4p4e8 10746 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
142 | 141 | oveq2i 6301 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
143 | | expadd 12314 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                   |
144 | 30, 61, 61, 143 | mp3an 1364 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
145 | | 2exp8 15060 |
. . . . . . . . . . . . . . . . . . . . . . 23
    ;;   |
146 | 142, 144,
145 | 3eqtr3i 2481 |
. . . . . . . . . . . . . . . . . . . . . 22
          ;;   |
147 | 136, 140,
146 | 3eqtr2i 2479 |
. . . . . . . . . . . . . . . . . . . . 21
  ;   ;;   |
148 | 147 | oveq2i 6301 |
. . . . . . . . . . . . . . . . . . . 20
       ;         ;;    |
149 | 135, 148 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . 19
        ;         ;;     |
150 | 149 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
         ;           ;;      |
151 | 128, 134,
150 | 3eqtr2d 2491 |
. . . . . . . . . . . . . . . . 17
        ;        ;;      |
152 | 123, 127,
151 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . 16
                   ;;      |
153 | 152 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
                                              ;;       |
154 | 121, 122,
153 | 3eqtr3d 2493 |
. . . . . . . . . . . . . 14
                            ;;       |
155 | 117, 154 | oveq12d 6308 |
. . . . . . . . . . . . 13
    ;;                        ;;         ;;                        ;;        |
156 | | mulcl 9623 |
. . . . . . . . . . . . . . 15
                           |
157 | 80, 119, 156 | sylancr 669 |
. . . . . . . . . . . . . 14
               |
158 | | mulcl 9623 |
. . . . . . . . . . . . . . 15
       ;;          ;;      |
159 | 30, 111, 158 | sylancr 669 |
. . . . . . . . . . . . . 14
       ;;      |
160 | 111, 157,
159 | pnpcan2d 10024 |
. . . . . . . . . . . . 13
        ;;         ;;                        ;;            ;;                  |
161 | 155, 160 | eqtrd 2485 |
. . . . . . . . . . . 12
    ;;                       ;;                  |
162 | 161 | oveq2d 6306 |
. . . . . . . . . . 11
         ;     ;;                          ;        ;;                   |
163 | 79, 111, 157 | addsub12d 10009 |
. . . . . . . . . . 11
         ;        ;;                       ;;           ;                  |
164 | 162, 163 | eqtrd 2485 |
. . . . . . . . . 10
         ;     ;;                        ;;           ;                  |
165 | 59, 11, 35, 14, 37 | divdiv1d 10414 |
. . . . . . . . . . . . . . . 16
                       |
166 | 138 | oveq2i 6301 |
. . . . . . . . . . . . . . . 16
                 ;   |
167 | 165, 166 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
                  ;    |
168 | 167 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                     ;     |
169 | 60, 35, 37 | divcan2d 10385 |
. . . . . . . . . . . . . 14
                       |
170 | 79 | 2timesd 10855 |
. . . . . . . . . . . . . 14
        
;           ;         ;     |
171 | 168, 169,
170 | 3eqtr3d 2493 |
. . . . . . . . . . . . 13
                
;         ;     |
172 | 171 | oveq1d 6305 |
. . . . . . . . . . . 12
                
;           
;         ;          ;     |
173 | 79, 79 | pncand 9987 |
. . . . . . . . . . . 12
          ;         ;          ;         
;    |
174 | 172, 173 | eqtrd 2485 |
. . . . . . . . . . 11
                
;          ;    |
175 | 174 | oveq1d 6305 |
. . . . . . . . . 10
                  ;      ;;                          ;     ;;                    |
176 | | quart1.p |
. . . . . . . . . . . . 13
             |
177 | 176 | oveq1d 6305 |
. . . . . . . . . . . 12
                             |
178 | 80, 10, 13 | divcli 10349 |
. . . . . . . . . . . . . 14
   |
179 | | mulcl 9623 |
. . . . . . . . . . . . . 14
                   |
180 | 178, 58, 179 | sylancr 669 |
. . . . . . . . . . . . 13
           |
181 | 20 | sqcld 12414 |
. . . . . . . . . . . . 13
         |
182 | 3, 180, 181 | subdird 10075 |
. . . . . . . . . . . 12
                                               |
183 | 2, 17, 19 | sqdivd 12429 |
. . . . . . . . . . . . . . . 16
                   |
184 | 16 | sqvali 12354 |
. . . . . . . . . . . . . . . . . 18
       |
185 | 184, 125 | eqtri 2473 |
. . . . . . . . . . . . . . . . 17
    ;  |
186 | 185 | oveq2i 6301 |
. . . . . . . . . . . . . . . 16
               ;   |
187 | 183, 186 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
            ;    |
188 | 187 | oveq2d 6306 |
. . . . . . . . . . . . . 14
               ;     |
189 | 3, 58, 76, 78 | divassd 10418 |
. . . . . . . . . . . . . 14
        ;        ;     |
190 | 3, 58 | mulcomd 9664 |
. . . . . . . . . . . . . . 15
               |
191 | 190 | oveq1d 6305 |
. . . . . . . . . . . . . 14
        ;         ;    |
192 | 188, 189,
191 | 3eqtr2d 2491 |
. . . . . . . . . . . . 13
                ;    |
193 | 178 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
     |
194 | 193, 58, 58 | mulassd 9666 |
. . . . . . . . . . . . . . . . 17
                               |
195 | 103, 63, 11, 14 | div23d 10420 |
. . . . . . . . . . . . . . . . . 18
                   |
196 | | 2p2e4 10727 |
. . . . . . . . . . . . . . . . . . . . 21
   |
197 | 196 | oveq2i 6301 |
. . . . . . . . . . . . . . . . . . . 20
           |
198 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   |
199 | 2, 198, 198 | expaddd 12418 |
. . . . . . . . . . . . . . . . . . . 20
                   |
200 | 197, 199 | syl5eqr 2499 |
. . . . . . . . . . . . . . . . . . 19
                 |
201 | 200 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . 18
                         |
202 | 195, 201 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
                         |
203 | 103, 63, 11, 14 | divassd 10418 |
. . . . . . . . . . . . . . . . 17
                   |
204 | 194, 202,
203 | 3eqtr2d 2491 |
. . . . . . . . . . . . . . . 16
                         |
205 | 204 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                                     |
206 | 185, 76 | syl5eqel 2533 |
. . . . . . . . . . . . . . . 16
       |
207 | 185, 77 | eqnetri 2694 |
. . . . . . . . . . . . . . . . 17
     |
208 | 207 | a1i 11 |
. . . . . . . . . . . . . . . 16
       |
209 | 180, 58, 206, 208 | divassd 10418 |
. . . . . . . . . . . . . . 15
                                           |
210 | 103, 64, 206, 208 | divassd 10418 |
. . . . . . . . . . . . . . 15
                               |
211 | 205, 209,
210 | 3eqtr3d 2493 |
. . . . . . . . . . . . . 14
                                     |
212 | 183 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                                       |
213 | 185 | oveq2i 6301 |
. . . . . . . . . . . . . . . 16
                   ;   |
214 | 127, 213 | syl6eqr 2503 |
. . . . . . . . . . . . . . 15
                         |
215 | 214 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                             |
216 | 211, 212,
215 | 3eqtr4d 2495 |
. . . . . . . . . . . . 13
                               |
217 | 192, 216 | oveq12d 6308 |
. . . . . . . . . . . 12
                                   ;                 |
218 | 177, 182,
217 | 3eqtrd 2489 |
. . . . . . . . . . 11
                
;                 |
219 | 218 | oveq2d 6306 |
. . . . . . . . . 10
       ;;                  ;;           ;                  |
220 | 164, 175,
219 | 3eqtr4d 2495 |
. . . . . . . . 9
                  ;      ;;                        ;;              |
221 | 101, 102,
220 | 3eqtrd 2489 |
. . . . . . . 8
             ;;                         ;          ;;              |
222 | 221 | negeqd 9869 |
. . . . . . 7
              ;;                         ;           ;;              |
223 | 65, 79, 60, 89 | addsub4d 10033 |
. . . . . . 7
                  ;              ;;                                     ;    ;;            |
224 | 99, 222, 223 | 3eqtr3rd 2494 |
. . . . . 6
                            ;    ;;                 ;;              |
225 | 224 | oveq2d 6306 |
. . . . 5
                            
;    ;;                   ;;               |
226 | 3, 180 | subcld 9986 |
. . . . . . . . 9
             |
227 | 176, 226 | eqeltrd 2529 |
. . . . . . . 8
   |
228 | 227, 181 | mulcld 9663 |
. . . . . . 7
           |
229 | 111, 228 | addcld 9662 |
. . . . . 6
       ;;              |
230 | 71, 229 | negsubd 9992 |
. . . . 5
         ;;                    ;;               |
231 | 96, 225, 230 | 3eqtrd 2489 |
. . . 4
                            
;    ;;                  ;;               |
232 | 93, 95, 231 | 3eqtrd 2489 |
. . 3
   
          ;;               |
233 | 232 | oveq2d 6306 |
. 2
        ;;                          ;;                   ;;                |
234 | 229, 71 | pncan3d 9989 |
. 2
        ;;                   ;;                |
235 | 233, 234 | eqtr2d 2486 |
1
        ;;                     |