Step | Hyp | Ref
| Expression |
1 | | stirlinglem3.4 |
. 2
                                     |
2 | | nnnn0 10900 |
. . . . . . . . . . . . 13
   |
3 | | faccl 12507 |
. . . . . . . . . . . . 13

      |
4 | | nncn 10639 |
. . . . . . . . . . . . 13
           |
5 | 2, 3, 4 | 3syl 18 |
. . . . . . . . . . . 12
       |
6 | | 2cnd 10704 |
. . . . . . . . . . . . . . 15
   |
7 | | nncn 10639 |
. . . . . . . . . . . . . . 15
   |
8 | 6, 7 | mulcld 9681 |
. . . . . . . . . . . . . 14
     |
9 | 8 | sqrtcld 13576 |
. . . . . . . . . . . . 13
         |
10 | | ere 14220 |
. . . . . . . . . . . . . . . . 17
 |
11 | 10 | recni 9673 |
. . . . . . . . . . . . . . . 16
 |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
13 | | epos 14336 |
. . . . . . . . . . . . . . . . 17
 |
14 | 10, 13 | gt0ne0ii 10171 |
. . . . . . . . . . . . . . . 16
 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
16 | 7, 12, 15 | divcld 10405 |
. . . . . . . . . . . . . 14
     |
17 | 16, 2 | expcld 12454 |
. . . . . . . . . . . . 13
         |
18 | 9, 17 | mulcld 9681 |
. . . . . . . . . . . 12
                 |
19 | | 2rp 11330 |
. . . . . . . . . . . . . . . . 17
 |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
21 | | nnrp 11334 |
. . . . . . . . . . . . . . . 16
   |
22 | 20, 21 | rpmulcld 11380 |
. . . . . . . . . . . . . . 15
     |
23 | 22 | sqrtgt0d 13551 |
. . . . . . . . . . . . . 14
         |
24 | 23 | gt0ne0d 10199 |
. . . . . . . . . . . . 13
         |
25 | | nnne0 10664 |
. . . . . . . . . . . . . . 15
   |
26 | 7, 12, 25, 15 | divne0d 10421 |
. . . . . . . . . . . . . 14
     |
27 | | nnz 10983 |
. . . . . . . . . . . . . 14
   |
28 | 16, 26, 27 | expne0d 12460 |
. . . . . . . . . . . . 13
         |
29 | 9, 17, 24, 28 | mulne0d 10286 |
. . . . . . . . . . . 12
                 |
30 | 5, 18, 29 | divcld 10405 |
. . . . . . . . . . 11
                       |
31 | | stirlinglem3.1 |
. . . . . . . . . . . 12
                       |
32 | 31 | fvmpt2 5972 |
. . . . . . . . . . 11
                                                 |
33 | 30, 32 | mpdan 681 |
. . . . . . . . . 10
                           |
34 | 33 | oveq1d 6323 |
. . . . . . . . 9
                                   |
35 | | stirlinglem3.3 |
. . . . . . . . . . . 12
                 |
36 | 35 | fvmpt2 5972 |
. . . . . . . . . . 11
                                     |
37 | 18, 36 | mpdan 681 |
. . . . . . . . . 10
                     |
38 | 37 | oveq1d 6323 |
. . . . . . . . 9
                             |
39 | 34, 38 | oveq12d 6326 |
. . . . . . . 8
                                                                 |
40 | | 4nn0 10912 |
. . . . . . . . . . 11
 |
41 | 40 | a1i 11 |
. . . . . . . . . 10
   |
42 | 5, 18, 29, 41 | expdivd 12468 |
. . . . . . . . 9
                                                       |
43 | 42 | oveq1d 6323 |
. . . . . . . 8
                                                                                               |
44 | 5, 41 | expcld 12454 |
. . . . . . . . 9
           |
45 | 18, 41 | expcld 12454 |
. . . . . . . . 9
                     |
46 | 41 | nn0zd 11061 |
. . . . . . . . . 10
   |
47 | 18, 29, 46 | expne0d 12460 |
. . . . . . . . 9
                     |
48 | 44, 45, 47 | divcan1d 10406 |
. . . . . . . 8
                                                           |
49 | 39, 43, 48 | 3eqtrd 2509 |
. . . . . . 7
                             |
50 | 49 | eqcomd 2477 |
. . . . . 6
                             |
51 | 50 | oveq2d 6324 |
. . . . 5
                                             |
52 | | 2nn0 10910 |
. . . . . . . . . . . . 13
 |
53 | 52 | a1i 11 |
. . . . . . . . . . . 12
   |
54 | 53, 2 | nn0mulcld 10954 |
. . . . . . . . . . 11
     |
55 | | faccl 12507 |
. . . . . . . . . . 11
  
        |
56 | | nncn 10639 |
. . . . . . . . . . 11
               |
57 | 54, 55, 56 | 3syl 18 |
. . . . . . . . . 10
         |
58 | 57 | sqcld 12452 |
. . . . . . . . 9
             |
59 | 6, 8 | mulcld 9681 |
. . . . . . . . . . . 12
       |
60 | 59 | sqrtcld 13576 |
. . . . . . . . . . 11
           |
61 | 8, 12, 15 | divcld 10405 |
. . . . . . . . . . . 12
       |
62 | 61, 54 | expcld 12454 |
. . . . . . . . . . 11
             |
63 | 60, 62 | mulcld 9681 |
. . . . . . . . . 10
                       |
64 | 63 | sqcld 12452 |
. . . . . . . . 9
                           |
65 | 20, 22 | rpmulcld 11380 |
. . . . . . . . . . . . 13
       |
66 | 65 | sqrtgt0d 13551 |
. . . . . . . . . . . 12
           |
67 | 66 | gt0ne0d 10199 |
. . . . . . . . . . 11
           |
68 | 20 | rpne0d 11369 |
. . . . . . . . . . . . . 14
   |
69 | 6, 7, 68, 25 | mulne0d 10286 |
. . . . . . . . . . . . 13
     |
70 | 8, 12, 69, 15 | divne0d 10421 |
. . . . . . . . . . . 12
       |
71 | | 2z 10993 |
. . . . . . . . . . . . . 14
 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . 13
   |
73 | 72, 27 | zmulcld 11069 |
. . . . . . . . . . . 12
     |
74 | 61, 70, 73 | expne0d 12460 |
. . . . . . . . . . 11
             |
75 | 60, 62, 67, 74 | mulne0d 10286 |
. . . . . . . . . 10
                       |
76 | 63, 75, 72 | expne0d 12460 |
. . . . . . . . 9
                           |
77 | 58, 64, 76 | divcan1d 10406 |
. . . . . . . 8
                                                                           |
78 | 57, 63, 75, 53 | expdivd 12468 |
. . . . . . . . . 10
                                                                       |
79 | 78 | eqcomd 2477 |
. . . . . . . . 9
                                                                       |
80 | 79 | oveq1d 6323 |
. . . . . . . 8
                                                                                                                           |
81 | 77, 80 | eqtr3d 2507 |
. . . . . . 7
                                                                       |
82 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
83 | | oveq2 6316 |
. . . . . . . . . . . . . . . . 17
       |
84 | 83 | fveq2d 5883 |
. . . . . . . . . . . . . . . 16
               |
85 | | oveq1 6315 |
. . . . . . . . . . . . . . . . 17
       |
86 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
87 | 85, 86 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
               |
88 | 84, 87 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
                               |
89 | 82, 88 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                                           |
90 | 89 | cbvmptv 4488 |
. . . . . . . . . . . . 13
                                             |
91 | 31, 90 | eqtri 2493 |
. . . . . . . . . . . 12
                       |
92 | 91 | a1i 11 |
. . . . . . . . . . 11
                         |
93 | | fveq2 5879 |
. . . . . . . . . . . . 13
               |
94 | | oveq2 6316 |
. . . . . . . . . . . . . . 15
           |
95 | 94 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                   |
96 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
           |
97 | | id 22 |
. . . . . . . . . . . . . . 15
       |
98 | 96, 97 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                     |
99 | 95, 98 | oveq12d 6326 |
. . . . . . . . . . . . 13
                                       |
100 | 93, 99 | oveq12d 6326 |
. . . . . . . . . . . 12
                                                     |
101 | 100 | adantl 473 |
. . . . . . . . . . 11
 
                                                     |
102 | | 2nn 10790 |
. . . . . . . . . . . . 13
 |
103 | 102 | a1i 11 |
. . . . . . . . . . . 12
   |
104 | | id 22 |
. . . . . . . . . . . 12
   |
105 | 103, 104 | nnmulcld 10679 |
. . . . . . . . . . 11
     |
106 | 57, 63, 75 | divcld 10405 |
. . . . . . . . . . 11
                               |
107 | 92, 101, 105, 106 | fvmptd 5969 |
. . . . . . . . . 10
                                     |
108 | 107 | oveq1d 6323 |
. . . . . . . . 9
                                             |
109 | 108 | eqcomd 2477 |
. . . . . . . 8
                                             |
110 | 109 | oveq1d 6323 |
. . . . . . 7
                                                                                                 |
111 | | eqidd 2472 |
. . . . . . . . . . 11
                                   |
112 | 99 | adantl 473 |
. . . . . . . . . . 11
 
                                       |
113 | 111, 112,
105, 63 | fvmptd 5969 |
. . . . . . . . . 10
                                             |
114 | 113 | oveq1d 6323 |
. . . . . . . . 9
                                                     |
115 | 114 | eqcomd 2477 |
. . . . . . . 8
                                                     |
116 | 115 | oveq2d 6324 |
. . . . . . 7
                                                                             |
117 | 81, 110, 116 | 3eqtrd 2509 |
. . . . . 6
                                                   |
118 | 88 | cbvmptv 4488 |
. . . . . . . . . . 11
                                 |
119 | 118 | a1i 11 |
. . . . . . . . . 10
                                   |
120 | 119 | fveq1d 5881 |
. . . . . . . . 9
                                               |
121 | 120 | eqcomd 2477 |
. . . . . . . 8
                                               |
122 | 121 | oveq1d 6323 |
. . . . . . 7
                                                       |
123 | 122 | oveq2d 6324 |
. . . . . 6
                                                                               |
124 | 107, 106 | eqeltrd 2549 |
. . . . . . . . . 10
         |
125 | | stirlinglem3.2 |
. . . . . . . . . . 11
         |
126 | 125 | fvmpt2 5972 |
. . . . . . . . . 10
                     |
127 | 124, 126 | mpdan 681 |
. . . . . . . . 9
             |
128 | 127 | eqcomd 2477 |
. . . . . . . 8
             |
129 | 128 | oveq1d 6323 |
. . . . . . 7
                     |
130 | 35 | a1i 11 |
. . . . . . . . . 10
                   |
131 | 130 | fveq1d 5881 |
. . . . . . . . 9
                               |
132 | 131 | eqcomd 2477 |
. . . . . . . 8
                               |
133 | 132 | oveq1d 6323 |
. . . . . . 7
                                       |
134 | 129, 133 | oveq12d 6326 |
. . . . . 6
                                                             |
135 | 117, 123,
134 | 3eqtrd 2509 |
. . . . 5
                                 |
136 | 51, 135 | oveq12d 6326 |
. . . 4
                                                                               |
137 | 136 | oveq1d 6323 |
. . 3
                                                                                           |
138 | 137 | mpteq2ia 4478 |
. 2
                                                                                             |
139 | 41, 2 | nn0mulcld 10954 |
. . . . . . . 8
     |
140 | 6, 139 | expcld 12454 |
. . . . . . 7
         |
141 | 49, 44 | eqeltrd 2549 |
. . . . . . 7
                     |
142 | 140, 141 | mulcomd 9682 |
. . . . . 6
                                                       |
143 | 142 | oveq1d 6323 |
. . . . 5
                                                                                                   |
144 | 143 | oveq1d 6323 |
. . . 4
                                                                                                               |
145 | 127, 124 | eqeltrd 2549 |
. . . . . . . 8
       |
146 | 145 | sqcld 12452 |
. . . . . . 7
           |
147 | 130, 119 | eqtrd 2505 |
. . . . . . . . . 10
                   |
148 | 147, 112,
105, 63 | fvmptd 5969 |
. . . . . . . . 9
                             |
149 | 148, 63 | eqeltrd 2549 |
. . . . . . . 8
         |
150 | 149 | sqcld 12452 |
. . . . . . 7
             |
151 | | nnne0 10664 |
. . . . . . . . . . . 12
               |
152 | 54, 55, 151 | 3syl 18 |
. . . . . . . . . . 11
         |
153 | 57, 63, 152, 75 | divne0d 10421 |
. . . . . . . . . 10
                               |
154 | 107, 153 | eqnetrd 2710 |
. . . . . . . . 9
         |
155 | 127, 154 | eqnetrd 2710 |
. . . . . . . 8
       |
156 | 145, 155,
72 | expne0d 12460 |
. . . . . . 7
           |
157 | 148, 75 | eqnetrd 2710 |
. . . . . . . 8
         |
158 | 149, 157,
72 | expne0d 12460 |
. . . . . . 7
             |
159 | 141, 146,
140, 150, 156, 158 | divmuldivd 10446 |
. . . . . 6
                                                                                                   |
160 | 159 | eqcomd 2477 |
. . . . 5
                                                                                                   |
161 | 160 | oveq1d 6323 |
. . . 4
                                                                                                               |
162 | 33, 30 | eqeltrd 2549 |
. . . . . . . . 9
       |
163 | 162, 41 | expcld 12454 |
. . . . . . . 8
           |
164 | 38, 45 | eqeltrd 2549 |
. . . . . . . 8
           |
165 | 163, 164,
146, 156 | div23d 10442 |
. . . . . . 7
                                                           |
166 | 165 | oveq1d 6323 |
. . . . . 6
                                                                                                   |
167 | 166 | oveq1d 6323 |
. . . . 5
                                                                                                               |
168 | 163, 146,
156 | divcld 10405 |
. . . . . . 7
                     |
169 | 140, 150,
158 | divcld 10405 |
. . . . . . 7
                     |
170 | 168, 164,
169 | mulassd 9684 |
. . . . . 6
                                                                                                   |
171 | 170 | oveq1d 6323 |
. . . . 5
                                                                                                               |
172 | 164, 169 | mulcld 9681 |
. . . . . . 7
                               |
173 | | 1cnd 9677 |
. . . . . . . 8
   |
174 | 8, 173 | addcld 9680 |
. . . . . . 7
       |
175 | | 0red 9662 |
. . . . . . . . 9
   |
176 | 105 | nnred 10646 |
. . . . . . . . 9
     |
177 | | 2re 10701 |
. . . . . . . . . . . 12
 |
178 | 177 | a1i 11 |
. . . . . . . . . . 11
   |
179 | | nnre 10638 |
. . . . . . . . . . 11
   |
180 | 178, 179 | remulcld 9689 |
. . . . . . . . . 10
     |
181 | | 1red 9676 |
. . . . . . . . . 10
   |
182 | 180, 181 | readdcld 9688 |
. . . . . . . . 9
       |
183 | 105 | nngt0d 10675 |
. . . . . . . . 9
     |
184 | 176 | ltp1d 10559 |
. . . . . . . . 9
         |
185 | 175, 176,
182, 183, 184 | lttrd 9813 |
. . . . . . . 8
       |
186 | 185 | gt0ne0d 10199 |
. . . . . . 7
       |
187 | 168, 172,
174, 186 | divassd 10440 |
. . . . . 6
                                                                                                               |
188 | 164, 140,
150, 158 | div12d 10441 |
. . . . . . . . . 10
                                                           |
189 | 9, 17, 41 | mulexpd 12469 |
. . . . . . . . . . . . 13
                                           |
190 | 60, 62 | sqmuld 12466 |
. . . . . . . . . . . . 13
                                                       |
191 | 189, 190 | oveq12d 6326 |
. . . . . . . . . . . 12
                                                                                                   |
192 | 148 | oveq1d 6323 |
. . . . . . . . . . . . 13
                                     |
193 | 38, 192 | oveq12d 6326 |
. . . . . . . . . . . 12
                                                                   |
194 | 9, 41 | expcld 12454 |
. . . . . . . . . . . . 13
             |
195 | 60 | sqcld 12452 |
. . . . . . . . . . . . 13
               |
196 | 17, 41 | expcld 12454 |
. . . . . . . . . . . . 13
             |
197 | 62 | sqcld 12452 |
. . . . . . . . . . . . 13
                 |
198 | 60, 67, 72 | expne0d 12460 |
. . . . . . . . . . . . 13
               |
199 | 62, 74, 72 | expne0d 12460 |
. . . . . . . . . . . . 13
                 |
200 | 194, 195,
196, 197, 198, 199 | divmuldivd 10446 |
. . . . . . . . . . . 12
                                                                                                           |
201 | 191, 193,
200 | 3eqtr4d 2515 |
. . . . . . . . . . 11
                                                                           |
202 | 201 | oveq2d 6324 |
. . . . . . . . . 10
                                                                                           |
203 | 65 | rprege0d 11371 |
. . . . . . . . . . . . . . . 16
             |
204 | | resqrtth 13396 |
. . . . . . . . . . . . . . . 16
                             |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . 15
                   |
206 | 205 | oveq2d 6324 |
. . . . . . . . . . . . . 14
                                           |
207 | | 2t2e4 10782 |
. . . . . . . . . . . . . . . . . . 19
   |
208 | 207 | eqcomi 2480 |
. . . . . . . . . . . . . . . . . 18
   |
209 | 208 | a1i 11 |
. . . . . . . . . . . . . . . . 17
     |
210 | 209 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
                         |
211 | 9, 53, 53 | expmuld 12457 |
. . . . . . . . . . . . . . . 16
                             |
212 | 22 | rprege0d 11371 |
. . . . . . . . . . . . . . . . . 18
         |
213 | | resqrtth 13396 |
. . . . . . . . . . . . . . . . . 18
                     |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . . 17
               |
215 | 214 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
                       |
216 | 210, 211,
215 | 3eqtrd 2509 |
. . . . . . . . . . . . . . 15
                   |
217 | 6, 6, 7 | mulassd 9684 |
. . . . . . . . . . . . . . . 16
           |
218 | 207 | a1i 11 |
. . . . . . . . . . . . . . . . 17
     |
219 | 218 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
         |
220 | 217, 219 | eqtr3d 2507 |
. . . . . . . . . . . . . . 15
         |
221 | 216, 220 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                             |
222 | 6, 7 | sqmuld 12466 |
. . . . . . . . . . . . . . . . 17
                   |
223 | | sq2 12409 |
. . . . . . . . . . . . . . . . . . 19
     |
224 | 223 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
       |
225 | 224 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                   |
226 | 222, 225 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
               |
227 | 226 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
                       |
228 | | 4cn 10709 |
. . . . . . . . . . . . . . . . . . 19
 |
229 | | 4ne0 10728 |
. . . . . . . . . . . . . . . . . . 19
 |
230 | 228, 229 | dividi 10362 |
. . . . . . . . . . . . . . . . . 18
   |
231 | 230 | a1i 11 |
. . . . . . . . . . . . . . . . 17
     |
232 | 7 | sqvald 12451 |
. . . . . . . . . . . . . . . . . . 19
         |
233 | 232 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
             |
234 | 7, 7, 25 | divcan4d 10411 |
. . . . . . . . . . . . . . . . . 18
       |
235 | 233, 234 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
         |
236 | 231, 235 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
               |
237 | 41 | nn0cnd 10951 |
. . . . . . . . . . . . . . . . 17
   |
238 | 7 | sqcld 12452 |
. . . . . . . . . . . . . . . . 17
       |
239 | 229 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
240 | 237, 237,
238, 7, 239, 25 | divmuldivd 10446 |
. . . . . . . . . . . . . . . 16
                       |
241 | 7 | mulid2d 9679 |
. . . . . . . . . . . . . . . 16
     |
242 | 236, 240,
241 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . 15
             |
243 | 227, 242 | eqtrd 2505 |
. . . . . . . . . . . . . 14
             |
244 | 206, 221,
243 | 3eqtrd 2509 |
. . . . . . . . . . . . 13
                           |
245 | 7, 237 | mulcomd 9682 |
. . . . . . . . . . . . . . . . 17
       |
246 | 245 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
                   |
247 | 16, 41, 2 | expmuld 12457 |
. . . . . . . . . . . . . . . 16
                     |
248 | 7, 12, 15, 139 | expdivd 12468 |
. . . . . . . . . . . . . . . 16
                         |
249 | 246, 247,
248 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . 15
                           |
250 | 6, 7, 6 | mul32d 9861 |
. . . . . . . . . . . . . . . . . 18
           |
251 | 250, 219 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
         |
252 | 251 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
                         |
253 | 61, 53, 54 | expmuld 12457 |
. . . . . . . . . . . . . . . 16
                             |
254 | 8, 12, 15, 139 | expdivd 12468 |
. . . . . . . . . . . . . . . 16
                             |
255 | 252, 253,
254 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . 15
                                 |
256 | 249, 255 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                                                             |
257 | 249, 196 | eqeltrrd 2550 |
. . . . . . . . . . . . . . 15
                 |
258 | 8, 139 | expcld 12454 |
. . . . . . . . . . . . . . 15
           |
259 | 12, 139 | expcld 12454 |
. . . . . . . . . . . . . . 15
         |
260 | 46, 27 | zmulcld 11069 |
. . . . . . . . . . . . . . . 16
     |
261 | 8, 69, 260 | expne0d 12460 |
. . . . . . . . . . . . . . 15
           |
262 | 12, 15, 260 | expne0d 12460 |
. . . . . . . . . . . . . . 15
         |
263 | 257, 258,
259, 261, 262 | divdiv2d 10437 |
. . . . . . . . . . . . . 14
                                                                   |
264 | 7, 139 | expcld 12454 |
. . . . . . . . . . . . . . . . 17
         |
265 | 264, 259,
262 | divcan1d 10406 |
. . . . . . . . . . . . . . . 16
                               |
266 | 265 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
                                                   |
267 | 6, 7, 139 | mulexpd 12469 |
. . . . . . . . . . . . . . . 16
                         |
268 | 267 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
                                         |
269 | 140, 264 | mulcomd 9682 |
. . . . . . . . . . . . . . . . 17
                               |
270 | 269 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
                                               |
271 | 7, 25, 260 | expne0d 12460 |
. . . . . . . . . . . . . . . . 17
         |
272 | 6, 68, 260 | expne0d 12460 |
. . . . . . . . . . . . . . . . 17
         |
273 | 264, 264,
140, 271, 272 | divdiv1d 10436 |
. . . . . . . . . . . . . . . 16
                                               |
274 | 264, 271 | dividd 10403 |
. . . . . . . . . . . . . . . . 17
                 |
275 | 274 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
                                 |
276 | 270, 273,
275 | 3eqtr2d 2511 |
. . . . . . . . . . . . . . 15
                                 |
277 | 266, 268,
276 | 3eqtrd 2509 |
. . . . . . . . . . . . . 14
                                           |
278 | 256, 263,
277 | 3eqtrd 2509 |
. . . . . . . . . . . . 13
                                     |
279 | 244, 278 | oveq12d 6326 |
. . . . . . . . . . . 12
                                                                 |
280 | 279 | oveq2d 6324 |
. . . . . . . . . . 11
                                                                                 |
281 | 140, 272 | reccld 10398 |
. . . . . . . . . . . 12
           |
282 | 140, 7, 281 | mul12d 9860 |
. . . . . . . . . . 11
                                       |
283 | 7 | mulid1d 9678 |
. . . . . . . . . . . 12
     |
284 | 140, 272 | recidd 10400 |
. . . . . . . . . . . . 13
                   |
285 | 284 | oveq2d 6324 |
. . . . . . . . . . . 12
                       |
286 | 283, 285,
235 | 3eqtr4d 2515 |
. . . . . . . . . . 11
                           |
287 | 280, 282,
286 | 3eqtrd 2509 |
. . . . . . . . . 10
                                                                     |
288 | 188, 202,
287 | 3eqtrd 2509 |
. . . . . . . . 9
                                     |
289 | 288 | oveq1d 6323 |
. . . . . . . 8
                                                 |
290 | 238, 7, 174, 25, 186 | divdiv1d 10436 |
. . . . . . . 8
                           |
291 | 289, 290 | eqtrd 2505 |
. . . . . . 7
                                                 |
292 | 291 | oveq2d 6324 |
. . . . . 6
                                                                                         |
293 | 187, 292 | eqtrd 2505 |
. . . . 5
                                                                                         |
294 | 167, 171,
293 | 3eqtrd 2509 |
. . . 4
                                                                                         |
295 | 144, 161,
294 | 3eqtrd 2509 |
. . 3
                                                                                         |
296 | 295 | mpteq2ia 4478 |
. 2
                                                                                           |
297 | 1, 138, 296 | 3eqtri 2497 |
1
                                   |