Proof of Theorem bposlem8
Step | Hyp | Ref
| Expression |
1 | | 6nn0 10919 |
. . . . 5
 |
2 | | 4nn 10798 |
. . . . 5
 |
3 | 1, 2 | decnncl 11093 |
. . . 4
;  |
4 | | fveq2 5888 |
. . . . . . . . . . . . . 14
 ;       ;    |
5 | | 8cn 10723 |
. . . . . . . . . . . . . . . . . 18
 |
6 | 5 | sqvali 12386 |
. . . . . . . . . . . . . . . . 17
       |
7 | | 8t8e64 11174 |
. . . . . . . . . . . . . . . . 17
  ;  |
8 | 6, 7 | eqtri 2484 |
. . . . . . . . . . . . . . . 16
    ;  |
9 | 8 | fveq2i 5891 |
. . . . . . . . . . . . . . 15
          ;   |
10 | | 0re 9669 |
. . . . . . . . . . . . . . . . 17
 |
11 | | 8re 10722 |
. . . . . . . . . . . . . . . . 17
 |
12 | | 8pos 10738 |
. . . . . . . . . . . . . . . . 17
 |
13 | 10, 11, 12 | ltleii 9783 |
. . . . . . . . . . . . . . . 16
 |
14 | 11 | sqrtsqi 13486 |
. . . . . . . . . . . . . . . 16
           |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . . . . 15
         |
16 | 9, 15 | eqtr3i 2486 |
. . . . . . . . . . . . . 14
  ;   |
17 | 4, 16 | syl6eq 2512 |
. . . . . . . . . . . . 13
 ;       |
18 | 17 | fveq2d 5892 |
. . . . . . . . . . . 12
 ;               |
19 | | 8nn 10802 |
. . . . . . . . . . . . 13
 |
20 | | nnrp 11340 |
. . . . . . . . . . . . 13
   |
21 | | fveq2 5888 |
. . . . . . . . . . . . . . . . 17
           |
22 | | cu2 12405 |
. . . . . . . . . . . . . . . . . . 19
     |
23 | 22 | fveq2i 5891 |
. . . . . . . . . . . . . . . . . 18
             |
24 | | 2rp 11336 |
. . . . . . . . . . . . . . . . . . 19
 |
25 | | 3z 10999 |
. . . . . . . . . . . . . . . . . . 19
 |
26 | | relogexp 23594 |
. . . . . . . . . . . . . . . . . . 19
                   |
27 | 24, 25, 26 | mp2an 683 |
. . . . . . . . . . . . . . . . . 18
               |
28 | 23, 27 | eqtr3i 2486 |
. . . . . . . . . . . . . . . . 17
           |
29 | 21, 28 | syl6eq 2512 |
. . . . . . . . . . . . . . . 16
             |
30 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
31 | 29, 30 | oveq12d 6333 |
. . . . . . . . . . . . . . 15
                 |
32 | | 3cn 10712 |
. . . . . . . . . . . . . . . 16
 |
33 | | 2nn 10796 |
. . . . . . . . . . . . . . . . . 18
 |
34 | | nnrp 11340 |
. . . . . . . . . . . . . . . . . 18
   |
35 | | relogcl 23574 |
. . . . . . . . . . . . . . . . . 18

      |
36 | 33, 34, 35 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
     |
37 | 36 | recni 9681 |
. . . . . . . . . . . . . . . 16
     |
38 | 19 | nnne0i 10672 |
. . . . . . . . . . . . . . . 16
 |
39 | 32, 37, 5, 38 | div23i 10393 |
. . . . . . . . . . . . . . 15
                 |
40 | 31, 39 | syl6eq 2512 |
. . . . . . . . . . . . . 14
                 |
41 | | bposlem7.2 |
. . . . . . . . . . . . . 14
         |
42 | | ovex 6343 |
. . . . . . . . . . . . . 14
         |
43 | 40, 41, 42 | fvmpt 5971 |
. . . . . . . . . . . . 13

              |
44 | 19, 20, 43 | mp2b 10 |
. . . . . . . . . . . 12
             |
45 | 18, 44 | syl6eq 2512 |
. . . . . . . . . . 11
 ;                   |
46 | 45 | oveq2d 6331 |
. . . . . . . . . 10
 ;                               |
47 | | sqrt2re 14351 |
. . . . . . . . . . . . 13
     |
48 | 47 | recni 9681 |
. . . . . . . . . . . 12
     |
49 | 32, 5, 38 | divcli 10377 |
. . . . . . . . . . . 12
   |
50 | 48, 49, 37 | mulassi 9678 |
. . . . . . . . . . 11
                             |
51 | | 4cn 10715 |
. . . . . . . . . . . . . . . 16
 |
52 | 48, 51, 48 | mul12i 9854 |
. . . . . . . . . . . . . . 15
                         |
53 | | 2re 10707 |
. . . . . . . . . . . . . . . . 17
 |
54 | | 0le2 10728 |
. . . . . . . . . . . . . . . . 17
 |
55 | | remsqsqrt 13369 |
. . . . . . . . . . . . . . . . 17
               |
56 | 53, 54, 55 | mp2an 683 |
. . . . . . . . . . . . . . . 16
           |
57 | 56 | oveq2i 6326 |
. . . . . . . . . . . . . . 15
               |
58 | | 4t2e8 10792 |
. . . . . . . . . . . . . . 15
   |
59 | 52, 57, 58 | 3eqtri 2488 |
. . . . . . . . . . . . . 14
             |
60 | 59 | oveq2i 6326 |
. . . . . . . . . . . . 13
                             |
61 | 51, 48 | mulcli 9674 |
. . . . . . . . . . . . . . 15
       |
62 | | nnrp 11340 |
. . . . . . . . . . . . . . . . . 18
   |
63 | 2, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 |
64 | | rpsqrtcl 13377 |
. . . . . . . . . . . . . . . . . 18

      |
65 | 33, 34, 64 | mp2b 10 |
. . . . . . . . . . . . . . . . 17
     |
66 | | rpmulcl 11353 |
. . . . . . . . . . . . . . . . 17
      
        |
67 | 63, 65, 66 | mp2an 683 |
. . . . . . . . . . . . . . . 16
       |
68 | | rpne0 11346 |
. . . . . . . . . . . . . . . 16
      
        |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . . . . . 15
       |
70 | | rpne0 11346 |
. . . . . . . . . . . . . . . 16
    
      |
71 | 24, 64, 70 | mp2b 10 |
. . . . . . . . . . . . . . 15
     |
72 | | divcan5 10337 |
. . . . . . . . . . . . . . . 16
                                                         |
73 | 32, 72 | mp3an1 1360 |
. . . . . . . . . . . . . . 15
                                                         |
74 | 61, 69, 48, 71, 73 | mp4an 684 |
. . . . . . . . . . . . . 14
                             |
75 | | 4ne0 10734 |
. . . . . . . . . . . . . . 15
 |
76 | | divdiv1 10346 |
. . . . . . . . . . . . . . . 16
                                 |
77 | 32, 76 | mp3an1 1360 |
. . . . . . . . . . . . . . 15
                                 |
78 | 51, 75, 48, 71, 77 | mp4an 684 |
. . . . . . . . . . . . . 14
                 |
79 | 74, 78 | eqtr4i 2487 |
. . . . . . . . . . . . 13
                             |
80 | 48, 32, 5, 38 | divassi 10391 |
. . . . . . . . . . . . 13
                 |
81 | 60, 79, 80 | 3eqtr3ri 2493 |
. . . . . . . . . . . 12
                 |
82 | 81 | oveq1i 6325 |
. . . . . . . . . . 11
                             |
83 | 50, 82 | eqtr3i 2486 |
. . . . . . . . . 10
                             |
84 | 46, 83 | syl6eq 2512 |
. . . . . . . . 9
 ;                               |
85 | | oveq1 6322 |
. . . . . . . . . . . . . 14
 ;   ;    |
86 | | df-6 10700 |
. . . . . . . . . . . . . . . . . 18
   |
87 | 86 | oveq2i 6326 |
. . . . . . . . . . . . . . . . 17
           |
88 | | 2exp6 15107 |
. . . . . . . . . . . . . . . . 17
    ;  |
89 | | 2cn 10708 |
. . . . . . . . . . . . . . . . . 18
 |
90 | | 5nn0 10918 |
. . . . . . . . . . . . . . . . . 18
 |
91 | | expp1 12311 |
. . . . . . . . . . . . . . . . . 18
 
               |
92 | 89, 90, 91 | mp2an 683 |
. . . . . . . . . . . . . . . . 17
             |
93 | 87, 88, 92 | 3eqtr3i 2492 |
. . . . . . . . . . . . . . . 16
;        |
94 | 93 | oveq1i 6325 |
. . . . . . . . . . . . . . 15
;           |
95 | | nnexpcl 12317 |
. . . . . . . . . . . . . . . . . 18
 
       |
96 | 33, 90, 95 | mp2an 683 |
. . . . . . . . . . . . . . . . 17
     |
97 | 96 | nncni 10647 |
. . . . . . . . . . . . . . . 16
     |
98 | | 2ne0 10730 |
. . . . . . . . . . . . . . . 16
 |
99 | 97, 89, 98 | divcan4i 10382 |
. . . . . . . . . . . . . . 15
             |
100 | 94, 99 | eqtri 2484 |
. . . . . . . . . . . . . 14
;       |
101 | 85, 100 | syl6eq 2512 |
. . . . . . . . . . . . 13
 ;         |
102 | 101 | fveq2d 5892 |
. . . . . . . . . . . 12
 ;                 |
103 | | nnrp 11340 |
. . . . . . . . . . . . 13
           |
104 | | fveq2 5888 |
. . . . . . . . . . . . . . . . 17
                   |
105 | | 5nn 10799 |
. . . . . . . . . . . . . . . . . . 19
 |
106 | 105 | nnzi 10990 |
. . . . . . . . . . . . . . . . . 18
 |
107 | | relogexp 23594 |
. . . . . . . . . . . . . . . . . 18
                   |
108 | 24, 106, 107 | mp2an 683 |
. . . . . . . . . . . . . . . . 17
               |
109 | 104, 108 | syl6eq 2512 |
. . . . . . . . . . . . . . . 16
                 |
110 | | id 22 |
. . . . . . . . . . . . . . . 16
           |
111 | 109, 110 | oveq12d 6333 |
. . . . . . . . . . . . . . 15
                         |
112 | | 5cn 10717 |
. . . . . . . . . . . . . . . 16
 |
113 | 96 | nnne0i 10672 |
. . . . . . . . . . . . . . . 16
     |
114 | 112, 37, 97, 113 | div23i 10393 |
. . . . . . . . . . . . . . 15
                         |
115 | 111, 114 | syl6eq 2512 |
. . . . . . . . . . . . . 14
                         |
116 | | ovex 6343 |
. . . . . . . . . . . . . 14
             |
117 | 115, 41, 116 | fvmpt 5971 |
. . . . . . . . . . . . 13
    
                      |
118 | 96, 103, 117 | mp2b 10 |
. . . . . . . . . . . 12
                     |
119 | 102, 118 | syl6eq 2512 |
. . . . . . . . . . 11
 ;                     |
120 | 119 | oveq2d 6331 |
. . . . . . . . . 10
 ;                             |
121 | | 9cn 10725 |
. . . . . . . . . . . 12
 |
122 | 121, 51, 75 | divcli 10377 |
. . . . . . . . . . 11
   |
123 | 112, 97, 113 | divcli 10377 |
. . . . . . . . . . 11
       |
124 | 122, 123,
37 | mulassi 9678 |
. . . . . . . . . 10
                                 |
125 | 120, 124 | syl6eqr 2514 |
. . . . . . . . 9
 ;                             |
126 | 84, 125 | oveq12d 6333 |
. . . . . . . 8
 ;                                                             |
127 | 32, 51, 75 | divcli 10377 |
. . . . . . . . . 10
   |
128 | 127, 48, 71 | divcli 10377 |
. . . . . . . . 9
         |
129 | 122, 123 | mulcli 9674 |
. . . . . . . . 9
           |
130 | 128, 129,
37 | adddiri 9680 |
. . . . . . . 8
                                                           |
131 | 126, 130 | syl6eqr 2514 |
. . . . . . 7
 ;                                                       |
132 | | oveq2 6323 |
. . . . . . . . . . 11
 ;    ;    |
133 | 132 | fveq2d 5892 |
. . . . . . . . . 10
 ;           ;     |
134 | 3 | nnrei 10646 |
. . . . . . . . . . . 12
;  |
135 | 3 | nngt0i 10671 |
. . . . . . . . . . . . 13
;  |
136 | 10, 134, 135 | ltleii 9783 |
. . . . . . . . . . . 12
;  |
137 | 53, 134, 54, 136 | sqrtmulii 13498 |
. . . . . . . . . . 11
    ;          ;    |
138 | 16 | oveq2i 6326 |
. . . . . . . . . . 11
       ;          |
139 | 137, 138 | eqtri 2484 |
. . . . . . . . . 10
    ;          |
140 | 133, 139 | syl6eq 2512 |
. . . . . . . . 9
 ;               |
141 | 140 | oveq2d 6331 |
. . . . . . . 8
 ;                           |
142 | 48, 5 | mulcli 9674 |
. . . . . . . . . 10
       |
143 | | rpmulcl 11353 |
. . . . . . . . . . . 12
               |
144 | 65, 20, 143 | sylancr 674 |
. . . . . . . . . . 11
         |
145 | | rpne0 11346 |
. . . . . . . . . . 11
      
        |
146 | 19, 144, 145 | mp2b 10 |
. . . . . . . . . 10
       |
147 | | divrec2 10315 |
. . . . . . . . . 10
                                               |
148 | 37, 142, 146, 147 | mp3an 1373 |
. . . . . . . . 9
                           |
149 | 48, 5 | mulcomi 9675 |
. . . . . . . . . . . 12
             |
150 | 149 | oveq2i 6326 |
. . . . . . . . . . 11
                 |
151 | | recdiv2 10348 |
. . . . . . . . . . . 12
                                 |
152 | 5, 38, 48, 71, 151 | mp4an 684 |
. . . . . . . . . . 11
                 |
153 | 150, 152 | eqtr4i 2487 |
. . . . . . . . . 10
                 |
154 | 153 | oveq1i 6325 |
. . . . . . . . 9
                             |
155 | 148, 154 | eqtri 2484 |
. . . . . . . 8
                           |
156 | 141, 155 | syl6eq 2512 |
. . . . . . 7
 ;                             |
157 | 131, 156 | oveq12d 6333 |
. . . . . 6
 ;                       
                                                             |
158 | 128, 129 | addcli 9673 |
. . . . . . 7
                     |
159 | 5, 38 | reccli 10365 |
. . . . . . . 8
   |
160 | 159, 48, 71 | divcli 10377 |
. . . . . . 7
         |
161 | 158, 160,
37 | adddiri 9680 |
. . . . . 6
                                                                               |
162 | 157, 161 | syl6eqr 2514 |
. . . . 5
 ;                       
                                                       |
163 | | bposlem7.1 |
. . . . 5
                                           |
164 | | ovex 6343 |
. . . . 5
                                     |
165 | 162, 163,
164 | fvmpt 5971 |
. . . 4
;   ;                                        |
166 | 3, 165 | ax-mp 5 |
. . 3
  ;                                       |
167 | | 3re 10711 |
. . . . . . . 8
 |
168 | | 4re 10714 |
. . . . . . . 8
 |
169 | 167, 168,
75 | redivcli 10402 |
. . . . . . 7
   |
170 | 169, 47, 71 | redivcli 10402 |
. . . . . 6
         |
171 | | 9re 10724 |
. . . . . . . 8
 |
172 | 171, 168,
75 | redivcli 10402 |
. . . . . . 7
   |
173 | | 5re 10716 |
. . . . . . . 8
 |
174 | 96 | nnrei 10646 |
. . . . . . . 8
     |
175 | 173, 174,
113 | redivcli 10402 |
. . . . . . 7
       |
176 | 172, 175 | remulcli 9683 |
. . . . . 6
           |
177 | 170, 176 | readdcli 9682 |
. . . . 5
                     |
178 | 11, 38 | rereccli 10400 |
. . . . . 6
   |
179 | 178, 47, 71 | redivcli 10402 |
. . . . 5
         |
180 | 177, 179 | readdcli 9682 |
. . . 4
                               |
181 | 180, 36 | remulcli 9683 |
. . 3
                                     |
182 | 166, 181 | eqeltri 2536 |
. 2
  ;   |
183 | 128, 129,
160 | add32i 9878 |
. . . . . 6
                                                             |
184 | | 6cn 10719 |
. . . . . . . . . . 11
 |
185 | | ax-1cn 9623 |
. . . . . . . . . . 11
 |
186 | 184, 185,
5, 38 | divdiri 10392 |
. . . . . . . . . 10
           |
187 | | df-7 10701 |
. . . . . . . . . . 11
   |
188 | 187 | oveq1i 6325 |
. . . . . . . . . 10
       |
189 | | divcan5 10337 |
. . . . . . . . . . . . . 14
                 |
190 | 32, 189 | mp3an1 1360 |
. . . . . . . . . . . . 13
                 |
191 | 51, 75, 89, 98, 190 | mp4an 684 |
. . . . . . . . . . . 12
         |
192 | | 3t2e6 10790 |
. . . . . . . . . . . . . 14
   |
193 | 32, 89, 192 | mulcomli 9676 |
. . . . . . . . . . . . 13
   |
194 | 51, 89, 58 | mulcomli 9676 |
. . . . . . . . . . . . 13
   |
195 | 193, 194 | oveq12i 6327 |
. . . . . . . . . . . 12
         |
196 | 191, 195 | eqtr3i 2486 |
. . . . . . . . . . 11
     |
197 | 196 | oveq1i 6325 |
. . . . . . . . . 10
             |
198 | 186, 188,
197 | 3eqtr4ri 2495 |
. . . . . . . . 9
         |
199 | 198 | oveq1i 6325 |
. . . . . . . 8
                     |
200 | 127, 159,
48, 71 | divdiri 10392 |
. . . . . . . 8
                               |
201 | | 7cn 10721 |
. . . . . . . . 9
 |
202 | 201, 5, 48, 38, 71 | divdiv32i 10390 |
. . . . . . . 8
                 |
203 | 199, 200,
202 | 3eqtr3i 2492 |
. . . . . . 7
                           |
204 | 203 | oveq1i 6325 |
. . . . . 6
                                                   |
205 | 183, 204 | eqtri 2484 |
. . . . 5
                                                   |
206 | | 4nn0 10917 |
. . . . . . . . . . . 12
 |
207 | | 9nn0 10922 |
. . . . . . . . . . . 12
 |
208 | | 0nn0 10913 |
. . . . . . . . . . . 12
 |
209 | | 9lt10 10841 |
. . . . . . . . . . . 12
 |
210 | | 4lt5 10811 |
. . . . . . . . . . . 12
 |
211 | 206, 90, 207, 208, 209, 210 | decltc 11102 |
. . . . . . . . . . 11
; ;  |
212 | | 7t7e49 11167 |
. . . . . . . . . . 11
  ;  |
213 | 56 | oveq1i 6325 |
. . . . . . . . . . . 12
                   |
214 | 48, 48, 112, 112 | mul4i 9856 |
. . . . . . . . . . . 12
                             |
215 | | 5t2e10 10793 |
. . . . . . . . . . . . . . 15
   |
216 | 112, 89, 215 | mulcomli 9676 |
. . . . . . . . . . . . . 14
   |
217 | 216 | oveq1i 6325 |
. . . . . . . . . . . . 13
       |
218 | 89, 112, 112 | mulassi 9678 |
. . . . . . . . . . . . 13
         |
219 | 90 | dec0u 11095 |
. . . . . . . . . . . . 13
  ;  |
220 | 217, 218,
219 | 3eqtr3i 2492 |
. . . . . . . . . . . 12
    ;  |
221 | 213, 214,
220 | 3eqtr3i 2492 |
. . . . . . . . . . 11
              ;  |
222 | 211, 212,
221 | 3brtr4i 4445 |
. . . . . . . . . 10
                 |
223 | | 7re 10720 |
. . . . . . . . . . . 12
 |
224 | | 7pos 10737 |
. . . . . . . . . . . 12
 |
225 | 10, 223, 224 | ltleii 9783 |
. . . . . . . . . . 11
 |
226 | | nnrp 11340 |
. . . . . . . . . . . . . 14
   |
227 | 105, 226 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
228 | | rpmulcl 11353 |
. . . . . . . . . . . . 13
               |
229 | 65, 227, 228 | mp2an 683 |
. . . . . . . . . . . 12
       |
230 | | rpge0 11343 |
. . . . . . . . . . . 12
      
        |
231 | 229, 230 | ax-mp 5 |
. . . . . . . . . . 11
       |
232 | | rpre 11337 |
. . . . . . . . . . . . 13
      
        |
233 | 229, 232 | ax-mp 5 |
. . . . . . . . . . . 12
       |
234 | 223, 233 | lt2msqi 10547 |
. . . . . . . . . . 11
 
                                 |
235 | 225, 231,
234 | mp2an 683 |
. . . . . . . . . 10
      
                  |
236 | 222, 235 | mpbir 214 |
. . . . . . . . 9
       |
237 | | rpgt0 11342 |
. . . . . . . . . . 11
    
      |
238 | 24, 64, 237 | mp2b 10 |
. . . . . . . . . 10
     |
239 | | ltdivmul 10508 |
. . . . . . . . . . 11
 
                           |
240 | 223, 173,
239 | mp3an12 1363 |
. . . . . . . . . 10
                 
         |
241 | 47, 238, 240 | mp2an 683 |
. . . . . . . . 9
      
        |
242 | 236, 241 | mpbir 214 |
. . . . . . . 8
       |
243 | 223, 47, 71 | redivcli 10402 |
. . . . . . . . 9
       |
244 | 243, 173,
11, 12 | ltdiv1ii 10564 |
. . . . . . . 8
      
            |
245 | 242, 244 | mpbi 213 |
. . . . . . 7
           |
246 | | divsubdir 10331 |
. . . . . . . . . . 11
 
               |
247 | 5, 32, 246 | mp3an12 1363 |
. . . . . . . . . 10
               |
248 | 5, 38, 247 | mp2an 683 |
. . . . . . . . 9
           |
249 | | 5p3e8 10777 |
. . . . . . . . . . . 12
   |
250 | 249 | oveq1i 6325 |
. . . . . . . . . . 11
       |
251 | 112, 32 | pncan3oi 9917 |
. . . . . . . . . . 11
     |
252 | 250, 251 | eqtr3i 2486 |
. . . . . . . . . 10
   |
253 | 252 | oveq1i 6325 |
. . . . . . . . 9
       |
254 | 5, 38 | dividi 10368 |
. . . . . . . . . 10
   |
255 | 254 | oveq1i 6325 |
. . . . . . . . 9
           |
256 | 248, 253,
255 | 3eqtr3ri 2493 |
. . . . . . . 8
       |
257 | | 5lt8 10828 |
. . . . . . . . . . . . 13
 |
258 | 11, 173 | remulcli 9683 |
. . . . . . . . . . . . . 14
   |
259 | 173, 11, 258 | ltadd2i 9791 |
. . . . . . . . . . . . 13

          |
260 | 257, 259 | mpbi 213 |
. . . . . . . . . . . 12
         |
261 | | df-9 10703 |
. . . . . . . . . . . . . 14
   |
262 | 261 | oveq1i 6325 |
. . . . . . . . . . . . 13
       |
263 | 5, 185, 112 | adddiri 9680 |
. . . . . . . . . . . . 13
           |
264 | 112 | mulid2i 9672 |
. . . . . . . . . . . . . 14
   |
265 | 264 | oveq2i 6326 |
. . . . . . . . . . . . 13
           |
266 | 262, 263,
265 | 3eqtri 2488 |
. . . . . . . . . . . 12
       |
267 | 86 | oveq2i 6326 |
. . . . . . . . . . . . 13
       |
268 | 5, 112, 185 | adddii 9679 |
. . . . . . . . . . . . 13
           |
269 | 5 | mulid1i 9671 |
. . . . . . . . . . . . . 14
   |
270 | 269 | oveq2i 6326 |
. . . . . . . . . . . . 13
           |
271 | 267, 268,
270 | 3eqtri 2488 |
. . . . . . . . . . . 12
       |
272 | 260, 266,
271 | 3brtr4i 4445 |
. . . . . . . . . . 11
     |
273 | 171, 173 | remulcli 9683 |
. . . . . . . . . . . 12
   |
274 | | 6re 10718 |
. . . . . . . . . . . . 13
 |
275 | 11, 274 | remulcli 9683 |
. . . . . . . . . . . 12
   |
276 | 168, 174 | remulcli 9683 |
. . . . . . . . . . . 12
       |
277 | 2, 96 | nnmulcli 10661 |
. . . . . . . . . . . . 13
       |
278 | 277 | nngt0i 10671 |
. . . . . . . . . . . 12
       |
279 | 273, 275,
276, 278 | ltdiv1ii 10564 |
. . . . . . . . . . 11
    
                      |
280 | 272, 279 | mpbi 213 |
. . . . . . . . . 10
                     |
281 | 121, 51, 112, 97, 75, 113 | divmuldivi 10395 |
. . . . . . . . . 10
                     |
282 | | nnexpcl 12317 |
. . . . . . . . . . . . . 14
 
       |
283 | 33, 206, 282 | mp2an 683 |
. . . . . . . . . . . . 13
     |
284 | 283 | nncni 10647 |
. . . . . . . . . . . 12
     |
285 | 283 | nnne0i 10672 |
. . . . . . . . . . . 12
     |
286 | | divcan5 10337 |
. . . . . . . . . . . . 13
                                 |
287 | 32, 286 | mp3an1 1360 |
. . . . . . . . . . . 12
                                 |
288 | 5, 38, 284, 285, 287 | mp4an 684 |
. . . . . . . . . . 11
                 |
289 | | df-4 10698 |
. . . . . . . . . . . . . . . 16
   |
290 | 289 | oveq2i 6326 |
. . . . . . . . . . . . . . 15
           |
291 | | 3nn0 10916 |
. . . . . . . . . . . . . . . 16
 |
292 | | expp1 12311 |
. . . . . . . . . . . . . . . 16
 
               |
293 | 89, 291, 292 | mp2an 683 |
. . . . . . . . . . . . . . 15
             |
294 | 22 | oveq1i 6325 |
. . . . . . . . . . . . . . 15
         |
295 | 290, 293,
294 | 3eqtri 2488 |
. . . . . . . . . . . . . 14
       |
296 | 295 | oveq1i 6325 |
. . . . . . . . . . . . 13
           |
297 | 5, 89, 32 | mulassi 9678 |
. . . . . . . . . . . . 13
         |
298 | 193 | oveq2i 6326 |
. . . . . . . . . . . . 13
       |
299 | 296, 297,
298 | 3eqtri 2488 |
. . . . . . . . . . . 12
         |
300 | | 4p3e7 10774 |
. . . . . . . . . . . . . . . 16
   |
301 | | 5p2e7 10776 |
. . . . . . . . . . . . . . . 16
   |
302 | 112, 89 | addcomi 9850 |
. . . . . . . . . . . . . . . 16
     |
303 | 300, 301,
302 | 3eqtr2i 2490 |
. . . . . . . . . . . . . . 15
     |
304 | 303 | oveq2i 6326 |
. . . . . . . . . . . . . 14
             |
305 | | expadd 12346 |
. . . . . . . . . . . . . . 15
 
                   |
306 | 89, 206, 291, 305 | mp3an 1373 |
. . . . . . . . . . . . . 14
                 |
307 | | 2nn0 10915 |
. . . . . . . . . . . . . . 15
 |
308 | | expadd 12346 |
. . . . . . . . . . . . . . 15
 
                   |
309 | 89, 307, 90, 308 | mp3an 1373 |
. . . . . . . . . . . . . 14
                 |
310 | 304, 306,
309 | 3eqtr3i 2492 |
. . . . . . . . . . . . 13
                     |
311 | 22 | oveq2i 6326 |
. . . . . . . . . . . . 13
                 |
312 | | sq2 12403 |
. . . . . . . . . . . . . 14
     |
313 | 312 | oveq1i 6325 |
. . . . . . . . . . . . 13
                 |
314 | 310, 311,
313 | 3eqtr3i 2492 |
. . . . . . . . . . . 12
             |
315 | 299, 314 | oveq12i 6327 |
. . . . . . . . . . 11
                         |
316 | 288, 315 | eqtr3i 2486 |
. . . . . . . . . 10
             |
317 | 280, 281,
316 | 3brtr4i 4445 |
. . . . . . . . 9
             |
318 | 167, 11, 38 | redivcli 10402 |
. . . . . . . . . 10
   |
319 | | 1re 9668 |
. . . . . . . . . 10
 |
320 | | ltsub2 10139 |
. . . . . . . . . 10
             
                                 |
321 | 176, 318,
319, 320 | mp3an 1373 |
. . . . . . . . 9
            
                  |
322 | 317, 321 | mpbi 213 |
. . . . . . . 8
                 |
323 | 256, 322 | eqbrtrri 4438 |
. . . . . . 7
               |
324 | 243, 11, 38 | redivcli 10402 |
. . . . . . . 8
         |
325 | 173, 11, 38 | redivcli 10402 |
. . . . . . . 8
   |
326 | 319, 176 | resubcli 9962 |
. . . . . . . 8
             |
327 | 324, 325,
326 | lttri 9786 |
. . . . . . 7
         
   
                    
              |
328 | 245, 323,
327 | mp2an 683 |
. . . . . 6
                     |
329 | 324, 176,
319 | ltaddsubi 10203 |
. . . . . 6
                    
                      |
330 | 328, 329 | mpbir 214 |
. . . . 5
                     |
331 | 205, 330 | eqbrtri 4436 |
. . . 4
                               |
332 | | 1lt2 10805 |
. . . . . . 7
 |
333 | | rplogcl 23602 |
. . . . . . 7
         |
334 | 53, 332, 333 | mp2an 683 |
. . . . . 6
     |
335 | | rpgt0 11342 |
. . . . . 6
    
      |
336 | 334, 335 | ax-mp 5 |
. . . . 5
     |
337 | 180, 319,
36, 336 | ltmul1ii 10563 |
. . . 4
                                                                           |
338 | 331, 337 | mpbi 213 |
. . 3
                                           |
339 | 37 | mulid2i 9672 |
. . . 4
           |
340 | 339 | eqcomi 2471 |
. . 3
           |
341 | 338, 166,
340 | 3brtr4i 4445 |
. 2
  ;       |
342 | 182, 341 | pm3.2i 461 |
1
   ;    ;        |