Step | Hyp | Ref
| Expression |
1 | | oveq2 6298 |
. . . . . . 7
       |
2 | 1 | fveq2d 5869 |
. . . . . 6
               |
3 | 1 | oveq1d 6305 |
. . . . . . 7
           |
4 | 3 | fveq2d 5869 |
. . . . . 6
                   |
5 | 2, 4 | oveq12d 6308 |
. . . . 5
                                   |
6 | | fveq2 5865 |
. . . . . . 7
               |
7 | 6 | oveq2d 6306 |
. . . . . 6
                   |
8 | 7 | oveq2d 6306 |
. . . . 5
                           |
9 | 5, 8 | eqeq12d 2466 |
. . . 4
                                                             |
10 | | oveq2 6298 |
. . . . . . 7
       |
11 | 10 | fveq2d 5869 |
. . . . . 6
               |
12 | 10 | oveq1d 6305 |
. . . . . . 7
           |
13 | 12 | fveq2d 5869 |
. . . . . 6
                   |
14 | 11, 13 | oveq12d 6308 |
. . . . 5
                                   |
15 | | fveq2 5865 |
. . . . . . 7
               |
16 | 15 | oveq2d 6306 |
. . . . . 6
                   |
17 | 16 | oveq2d 6306 |
. . . . 5
                           |
18 | 14, 17 | eqeq12d 2466 |
. . . 4
                                                             |
19 | | oveq2 6298 |
. . . . . . 7
           |
20 | 19 | fveq2d 5869 |
. . . . . 6
                   |
21 | 19 | oveq1d 6305 |
. . . . . . 7
               |
22 | 21 | fveq2d 5869 |
. . . . . 6
                       |
23 | 20, 22 | oveq12d 6308 |
. . . . 5
                                         |
24 | | fveq2 5865 |
. . . . . . 7
                   |
25 | 24 | oveq2d 6306 |
. . . . . 6
                       |
26 | 25 | oveq2d 6306 |
. . . . 5
                               |
27 | 23, 26 | eqeq12d 2466 |
. . . 4
                                                                     |
28 | | oveq2 6298 |
. . . . . . 7
       |
29 | 28 | fveq2d 5869 |
. . . . . 6
               |
30 | 28 | oveq1d 6305 |
. . . . . . 7
           |
31 | 30 | fveq2d 5869 |
. . . . . 6
                   |
32 | 29, 31 | oveq12d 6308 |
. . . . 5
                                   |
33 | | fveq2 5865 |
. . . . . . 7
               |
34 | 33 | oveq2d 6306 |
. . . . . 6
                   |
35 | 34 | oveq2d 6306 |
. . . . 5
                           |
36 | 32, 35 | eqeq12d 2466 |
. . . 4
                                                             |
37 | | 2t1e2 10758 |
. . . . . . 7
   |
38 | 37 | fveq2i 5868 |
. . . . . 6
           |
39 | 37 | oveq1i 6300 |
. . . . . . . 8
       |
40 | | 2p1e3 10733 |
. . . . . . . 8
   |
41 | 39, 40 | eqtri 2473 |
. . . . . . 7
     |
42 | 41 | fveq2i 5868 |
. . . . . 6
             |
43 | 38, 42 | oveq12i 6302 |
. . . . 5
                           |
44 | | 2z 10969 |
. . . . . . . . 9
 |
45 | | uzid 11173 |
. . . . . . . . 9
       |
46 | 44, 45 | ax-mp 5 |
. . . . . . . 8
     |
47 | | wallispilem4.2 |
. . . . . . . . . 10
                  |
48 | 47 | wallispilem2 37928 |
. . . . . . . . 9
                                 |
49 | 48 | simp3i 1019 |
. . . . . . . 8
    
                  |
50 | 46, 49 | ax-mp 5 |
. . . . . . 7
                 |
51 | | 2m1e1 10724 |
. . . . . . . . 9
   |
52 | 51 | oveq1i 6300 |
. . . . . . . 8
       |
53 | | 2cn 10680 |
. . . . . . . . . . 11
 |
54 | 53 | subidi 9945 |
. . . . . . . . . 10
   |
55 | 54 | fveq2i 5868 |
. . . . . . . . 9
           |
56 | 48 | simp1i 1017 |
. . . . . . . . 9
     |
57 | 55, 56 | eqtri 2473 |
. . . . . . . 8
       |
58 | 52, 57 | oveq12i 6302 |
. . . . . . 7
                 |
59 | | ax-1cn 9597 |
. . . . . . . . 9
 |
60 | | 2cnne0 10824 |
. . . . . . . . 9
   |
61 | | picn 23414 |
. . . . . . . . 9
 |
62 | | div32 10290 |
. . . . . . . . 9
               |
63 | 59, 60, 61, 62 | mp3an 1364 |
. . . . . . . 8
     
   |
64 | | 2ne0 10702 |
. . . . . . . . . 10
 |
65 | 61, 53, 64 | divcli 10349 |
. . . . . . . . 9
   |
66 | 65 | mulid2i 9646 |
. . . . . . . 8
       |
67 | 63, 66 | eqtri 2473 |
. . . . . . 7
       |
68 | 50, 58, 67 | 3eqtri 2477 |
. . . . . 6
       |
69 | | 3z 10970 |
. . . . . . . . 9
 |
70 | | 2re 10679 |
. . . . . . . . . 10
 |
71 | | 3re 10683 |
. . . . . . . . . 10
 |
72 | | 2lt3 10777 |
. . . . . . . . . 10
 |
73 | 70, 71, 72 | ltleii 9757 |
. . . . . . . . 9
 |
74 | | eluz2 11165 |
. . . . . . . . 9
         |
75 | 44, 69, 73, 74 | mpbir3an 1190 |
. . . . . . . 8
     |
76 | 47 | wallispilem2 37928 |
. . . . . . . . 9
                                 |
77 | 76 | simp3i 1019 |
. . . . . . . 8
    
                  |
78 | 75, 77 | ax-mp 5 |
. . . . . . 7
                 |
79 | | 3m1e2 10726 |
. . . . . . . . . 10
   |
80 | 79 | eqcomi 2460 |
. . . . . . . . 9
   |
81 | 80 | oveq1i 6300 |
. . . . . . . 8
       |
82 | | 3cn 10684 |
. . . . . . . . . . 11
 |
83 | 82, 53, 59, 40 | subaddrii 9964 |
. . . . . . . . . 10
   |
84 | 83 | fveq2i 5868 |
. . . . . . . . 9
           |
85 | 48 | simp2i 1018 |
. . . . . . . . 9
     |
86 | 84, 85 | eqtr2i 2474 |
. . . . . . . 8
       |
87 | 81, 86 | oveq12i 6302 |
. . . . . . 7
                 |
88 | | 3ne0 10704 |
. . . . . . . . 9
 |
89 | 53, 82, 88 | divcli 10349 |
. . . . . . . 8
   |
90 | 89, 53 | mulcomi 9649 |
. . . . . . 7
         |
91 | 78, 87, 90 | 3eqtr2i 2479 |
. . . . . 6
         |
92 | 68, 91 | oveq12i 6302 |
. . . . 5
                   |
93 | | 1z 10967 |
. . . . . . . . 9
 |
94 | | seq1 12226 |
. . . . . . . . 9
             |
95 | 93, 94 | ax-mp 5 |
. . . . . . . 8
           |
96 | | 1nn 10620 |
. . . . . . . . 9
 |
97 | | oveq2 6298 |
. . . . . . . . . . . . . 14
       |
98 | 97, 37 | syl6eq 2501 |
. . . . . . . . . . . . 13
     |
99 | 97 | oveq1d 6305 |
. . . . . . . . . . . . . 14
           |
100 | 37 | oveq1i 6300 |
. . . . . . . . . . . . . . 15
       |
101 | 100, 51 | eqtri 2473 |
. . . . . . . . . . . . . 14
     |
102 | 99, 101 | syl6eq 2501 |
. . . . . . . . . . . . 13
       |
103 | 98, 102 | oveq12d 6308 |
. . . . . . . . . . . 12
             |
104 | 53 | div1i 10335 |
. . . . . . . . . . . 12
   |
105 | 103, 104 | syl6eq 2501 |
. . . . . . . . . . 11
           |
106 | 98 | oveq1d 6305 |
. . . . . . . . . . . . 13
         |
107 | 106, 40 | syl6eq 2501 |
. . . . . . . . . . . 12
       |
108 | 98, 107 | oveq12d 6308 |
. . . . . . . . . . 11
             |
109 | 105, 108 | oveq12d 6308 |
. . . . . . . . . 10
                         |
110 | | wallispilem4.1 |
. . . . . . . . . 10
                     |
111 | | ovex 6318 |
. . . . . . . . . 10
     |
112 | 109, 110,
111 | fvmpt 5948 |
. . . . . . . . 9
           |
113 | 96, 112 | ax-mp 5 |
. . . . . . . 8
         |
114 | 95, 113 | eqtr2i 2474 |
. . . . . . 7
           |
115 | 114 | oveq2i 6301 |
. . . . . 6
                   |
116 | 53, 89 | mulcli 9648 |
. . . . . . . . 9
     |
117 | 113, 116 | eqeltri 2525 |
. . . . . . . 8
     |
118 | 95, 117 | eqeltri 2525 |
. . . . . . 7
       |
119 | 53, 82, 64, 88 | divne0i 10355 |
. . . . . . . . 9
   |
120 | 53, 89, 64, 119 | mulne0i 10255 |
. . . . . . . 8
     |
121 | 114, 120 | eqnetrri 2695 |
. . . . . . 7
       |
122 | 65, 118, 121 | divreci 10352 |
. . . . . 6
                       |
123 | 115, 122 | eqtri 2473 |
. . . . 5
                     |
124 | 43, 92, 123 | 3eqtri 2477 |
. . . 4
                             |
125 | | oveq2 6298 |
. . . . . . 7
                                                                                                           |
126 | 125 | adantl 468 |
. . . . . 6
                              
                                                                              |
127 | | 2cnd 10682 |
. . . . . . . . . . . . . . . 16
   |
128 | | nncn 10617 |
. . . . . . . . . . . . . . . 16
   |
129 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
   |
130 | 127, 128,
129 | adddid 9667 |
. . . . . . . . . . . . . . 15
             |
131 | 127 | mulid1d 9660 |
. . . . . . . . . . . . . . . 16
     |
132 | 131 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
             |
133 | 130, 132 | eqtrd 2485 |
. . . . . . . . . . . . . 14
           |
134 | 133 | oveq1d 6305 |
. . . . . . . . . . . . 13
               |
135 | 127, 128 | mulcld 9663 |
. . . . . . . . . . . . . 14
     |
136 | 135, 127,
129 | addsubassd 10006 |
. . . . . . . . . . . . 13
               |
137 | 51 | a1i 11 |
. . . . . . . . . . . . . 14
     |
138 | 137 | oveq2d 6306 |
. . . . . . . . . . . . 13
             |
139 | 134, 136,
138 | 3eqtrd 2489 |
. . . . . . . . . . . 12
             |
140 | 139 | oveq1d 6305 |
. . . . . . . . . . 11
                         |
141 | 140 | oveq1d 6305 |
. . . . . . . . . 10
                                         |
142 | 79 | a1i 11 |
. . . . . . . . . . . . . 14
     |
143 | 142 | oveq2d 6306 |
. . . . . . . . . . . . 13
             |
144 | 82 | a1i 11 |
. . . . . . . . . . . . . 14
   |
145 | 135, 144,
129 | addsubassd 10006 |
. . . . . . . . . . . . 13
               |
146 | 143, 145,
133 | 3eqtr4d 2495 |
. . . . . . . . . . . 12
             |
147 | 146 | oveq1d 6305 |
. . . . . . . . . . 11
                         |
148 | 147 | oveq1d 6305 |
. . . . . . . . . 10
                                                 |
149 | 141, 148 | oveq12d 6308 |
. . . . . . . . 9
                                                                                           |
150 | 44 | a1i 11 |
. . . . . . . . . . . . . 14
   |
151 | | nnz 10959 |
. . . . . . . . . . . . . . 15
   |
152 | 151 | peano2zd 11043 |
. . . . . . . . . . . . . 14
     |
153 | 150, 152 | zmulcld 11046 |
. . . . . . . . . . . . 13
       |
154 | 70 | a1i 11 |
. . . . . . . . . . . . . 14
   |
155 | | nnre 10616 |
. . . . . . . . . . . . . . 15
   |
156 | | 1red 9658 |
. . . . . . . . . . . . . . 15
   |
157 | 155, 156 | readdcld 9670 |
. . . . . . . . . . . . . 14
     |
158 | | 0le2 10700 |
. . . . . . . . . . . . . . 15
 |
159 | 158 | a1i 11 |
. . . . . . . . . . . . . 14
   |
160 | | nnnn0 10876 |
. . . . . . . . . . . . . . . 16
   |
161 | 160 | nn0ge0d 10928 |
. . . . . . . . . . . . . . 15
   |
162 | 156, 155 | addge02d 10202 |
. . . . . . . . . . . . . . 15
 
     |
163 | 161, 162 | mpbid 214 |
. . . . . . . . . . . . . 14
     |
164 | 154, 157,
159, 163 | lemulge11d 10544 |
. . . . . . . . . . . . 13
       |
165 | 44 | eluz1i 11166 |
. . . . . . . . . . . . 13
                     |
166 | 153, 164,
165 | sylanbrc 670 |
. . . . . . . . . . . 12
           |
167 | 47, 166 | itgsinexp 37831 |
. . . . . . . . . . 11
                                   |
168 | 133 | oveq1d 6305 |
. . . . . . . . . . . . . 14
               |
169 | 135, 127 | pncand 9987 |
. . . . . . . . . . . . . 14
           |
170 | 168, 169 | eqtrd 2485 |
. . . . . . . . . . . . 13
           |
171 | 170 | fveq2d 5869 |
. . . . . . . . . . . 12
                   |
172 | 171 | oveq2d 6306 |
. . . . . . . . . . 11
                                               |
173 | 167, 172 | eqtrd 2485 |
. . . . . . . . . 10
                               |
174 | 133 | oveq1d 6305 |
. . . . . . . . . . . . 13
               |
175 | 135, 127,
129 | addassd 9665 |
. . . . . . . . . . . . 13
               |
176 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
     |
177 | 176 | oveq2d 6306 |
. . . . . . . . . . . . 13
             |
178 | 174, 175,
177 | 3eqtrd 2489 |
. . . . . . . . . . . 12
             |
179 | 178 | fveq2d 5869 |
. . . . . . . . . . 11
                     |
180 | 150, 151 | zmulcld 11046 |
. . . . . . . . . . . . . 14
     |
181 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
   |
182 | 180, 181 | zaddcld 11044 |
. . . . . . . . . . . . 13
       |
183 | 154, 155 | remulcld 9671 |
. . . . . . . . . . . . . 14
     |
184 | 71 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
185 | 183, 184 | readdcld 9670 |
. . . . . . . . . . . . . 14
       |
186 | | nnge1 10635 |
. . . . . . . . . . . . . . 15
   |
187 | 154, 155,
159, 186 | lemulge11d 10544 |
. . . . . . . . . . . . . 14
     |
188 | | 0re 9643 |
. . . . . . . . . . . . . . . 16
 |
189 | | 3pos 10703 |
. . . . . . . . . . . . . . . 16
 |
190 | 188, 71, 189 | ltleii 9757 |
. . . . . . . . . . . . . . 15
 |
191 | 183, 184 | addge01d 10201 |
. . . . . . . . . . . . . . 15
 
         |
192 | 190, 191 | mpbii 215 |
. . . . . . . . . . . . . 14
         |
193 | 154, 183,
185, 187, 192 | letrd 9792 |
. . . . . . . . . . . . 13
       |
194 | 44 | eluz1i 11166 |
. . . . . . . . . . . . 13
                     |
195 | 182, 193,
194 | sylanbrc 670 |
. . . . . . . . . . . 12
           |
196 | 47, 195 | itgsinexp 37831 |
. . . . . . . . . . 11
                                   |
197 | 179, 196 | eqtrd 2485 |
. . . . . . . . . 10
                                     |
198 | 173, 197 | oveq12d 6308 |
. . . . . . . . 9
                                                                     |
199 | 135, 129 | addcld 9662 |
. . . . . . . . . . 11
       |
200 | 128, 129 | addcld 9662 |
. . . . . . . . . . . 12
     |
201 | 127, 200 | mulcld 9663 |
. . . . . . . . . . 11
       |
202 | 64 | a1i 11 |
. . . . . . . . . . . 12
   |
203 | | peano2nn 10621 |
. . . . . . . . . . . . 13
     |
204 | 203 | nnne0d 10654 |
. . . . . . . . . . . 12
     |
205 | 127, 200,
202, 204 | mulne0d 10264 |
. . . . . . . . . . 11
       |
206 | 199, 201,
205 | divcld 10383 |
. . . . . . . . . 10
             |
207 | | 2nn0 10886 |
. . . . . . . . . . . . 13
 |
208 | 207 | a1i 11 |
. . . . . . . . . . . 12
   |
209 | 208, 160 | nn0mulcld 10930 |
. . . . . . . . . . 11
     |
210 | 47 | wallispilem3 37929 |
. . . . . . . . . . . 12
  
        |
211 | 210 | rpcnd 11343 |
. . . . . . . . . . 11
  
        |
212 | 209, 211 | syl 17 |
. . . . . . . . . 10
         |
213 | 135, 144 | addcld 9662 |
. . . . . . . . . . . 12
       |
214 | | 0red 9644 |
. . . . . . . . . . . . . 14
   |
215 | | 2pos 10701 |
. . . . . . . . . . . . . . . 16
 |
216 | 215 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
217 | | nngt0 10638 |
. . . . . . . . . . . . . . 15
   |
218 | 154, 155,
216, 217 | mulgt0d 9790 |
. . . . . . . . . . . . . 14
     |
219 | 184, 189 | jctir 541 |
. . . . . . . . . . . . . . . 16
     |
220 | | elrp 11304 |
. . . . . . . . . . . . . . . 16

    |
221 | 219, 220 | sylibr 216 |
. . . . . . . . . . . . . . 15
   |
222 | 183, 221 | ltaddrpd 11371 |
. . . . . . . . . . . . . 14
         |
223 | 214, 183,
185, 218, 222 | lttrd 9796 |
. . . . . . . . . . . . 13
       |
224 | 223 | gt0ne0d 10178 |
. . . . . . . . . . . 12
       |
225 | 201, 213,
224 | divcld 10383 |
. . . . . . . . . . 11
             |
226 | 201, 213,
205, 224 | divne0d 10399 |
. . . . . . . . . . 11
             |
227 | 182, 150 | zsubcld 11045 |
. . . . . . . . . . . . . 14
         |
228 | 185, 154 | subge0d 10203 |
. . . . . . . . . . . . . . 15
 
     
       |
229 | 193, 228 | mpbird 236 |
. . . . . . . . . . . . . 14
         |
230 | | elnn0z 10950 |
. . . . . . . . . . . . . 14
      
                |
231 | 227, 229,
230 | sylanbrc 670 |
. . . . . . . . . . . . 13
         |
232 | 47 | wallispilem3 37929 |
. . . . . . . . . . . . 13
      
            |
233 | 231, 232 | syl 17 |
. . . . . . . . . . . 12
             |
234 | 233 | rpcnne0d 11350 |
. . . . . . . . . . 11
                         |
235 | 225, 226,
234 | jca31 537 |
. . . . . . . . . 10
                                                 |
236 | | divmuldiv 10307 |
. . . . . . . . . 10
                                                                                                                                                         |
237 | 206, 212,
235, 236 | syl21anc 1267 |
. . . . . . . . 9
                                                                                       |
238 | 149, 198,
237 | 3eqtr4d 2495 |
. . . . . . . 8
                                                                 |
239 | 135, 144,
127 | addsubassd 10006 |
. . . . . . . . . . . 12
               |
240 | 83 | a1i 11 |
. . . . . . . . . . . . 13
     |
241 | 240 | oveq2d 6306 |
. . . . . . . . . . . 12
             |
242 | 239, 241 | eqtrd 2485 |
. . . . . . . . . . 11
             |
243 | 242 | fveq2d 5869 |
. . . . . . . . . 10
                     |
244 | 243 | oveq2d 6306 |
. . . . . . . . 9
                                     |
245 | 244 | oveq2d 6306 |
. . . . . . . 8
                                                                                     |
246 | 238, 245 | eqtrd 2485 |
. . . . . . 7
                                                               |
247 | 246 | adantr 467 |
. . . . . 6
                              
                                                              |
248 | | elnnuz 11195 |
. . . . . . . . . . . . 13

      |
249 | 248 | biimpi 198 |
. . . . . . . . . . . 12
       |
250 | | seqp1 12228 |
. . . . . . . . . . . 12
    
                        |
251 | 249, 250 | syl 17 |
. . . . . . . . . . 11
                         |
252 | 110 | a1i 11 |
. . . . . . . . . . . . 13
                       |
253 | | oveq2 6298 |
. . . . . . . . . . . . . . . 16
           |
254 | 253 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
               |
255 | 253, 254 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
                         |
256 | 253 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
               |
257 | 253, 256 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
                         |
258 | 255, 257 | oveq12d 6308 |
. . . . . . . . . . . . . 14
                                                 |
259 | 258 | adantl 468 |
. . . . . . . . . . . . 13
 
                                                 |
260 | 154, 157 | remulcld 9671 |
. . . . . . . . . . . . . . 15
       |
261 | 260, 156 | resubcld 10047 |
. . . . . . . . . . . . . . 15
         |
262 | | 1lt2 10776 |
. . . . . . . . . . . . . . . . . . 19
 |
263 | 262 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   |
264 | | nnrp 11311 |
. . . . . . . . . . . . . . . . . . 19
   |
265 | 156, 264 | ltaddrp2d 11372 |
. . . . . . . . . . . . . . . . . 18
     |
266 | 154, 157,
263, 265 | mulgt1d 10543 |
. . . . . . . . . . . . . . . . 17
       |
267 | 156, 266 | gtned 9770 |
. . . . . . . . . . . . . . . 16
       |
268 | 201, 129,
267 | subne0d 9995 |
. . . . . . . . . . . . . . 15
         |
269 | 260, 261,
268 | redivcld 10435 |
. . . . . . . . . . . . . 14
               |
270 | 178, 185 | eqeltrd 2529 |
. . . . . . . . . . . . . . 15
         |
271 | 178, 224 | eqnetrd 2691 |
. . . . . . . . . . . . . . 15
         |
272 | 260, 270,
271 | redivcld 10435 |
. . . . . . . . . . . . . 14
               |
273 | 269, 272 | remulcld 9671 |
. . . . . . . . . . . . 13
                             |
274 | 252, 259,
203, 273 | fvmptd 5954 |
. . . . . . . . . . . 12
                                   |
275 | 274 | oveq2d 6306 |
. . . . . . . . . . 11
                                                   |
276 | 251, 275 | eqtrd 2485 |
. . . . . . . . . 10
                                             |
277 | 276 | oveq2d 6306 |
. . . . . . . . 9
                                                 |
278 | 277 | oveq2d 6306 |
. . . . . . . 8
                                                         |
279 | 139 | oveq2d 6306 |
. . . . . . . . . . . . 13
                         |
280 | 178 | oveq2d 6306 |
. . . . . . . . . . . . 13
                         |
281 | 279, 280 | oveq12d 6308 |
. . . . . . . . . . . 12
                                                   |
282 | 281 | oveq2d 6306 |
. . . . . . . . . . 11
                                                                   |
283 | 282 | oveq2d 6306 |
. . . . . . . . . 10
                                                                       |
284 | 283 | oveq2d 6306 |
. . . . . . . . 9
                                                                               |
285 | | elfznn 11828 |
. . . . . . . . . . . . . . . . 17
       |
286 | 285 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
       |
287 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
                       |
288 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . . 21
       |
289 | 288 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . 21
           |
290 | 288, 289 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . 20
                   |
291 | 288 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . . 21
           |
292 | 288, 291 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . . 20
                   |
293 | 290, 292 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . . 19
                                       |
294 | 293 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
                                       |
295 | | id 22 |
. . . . . . . . . . . . . . . . . 18
   |
296 | | 2rp 11307 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
297 | 296 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   |
298 | | nnrp 11311 |
. . . . . . . . . . . . . . . . . . . . 21
   |
299 | 297, 298 | rpmulcld 11357 |
. . . . . . . . . . . . . . . . . . . 20
     |
300 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
301 | | nnre 10616 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
302 | 300, 301 | remulcld 9671 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
303 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
304 | 302, 303 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . . 21
       |
305 | | nnge1 10635 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
306 | | nncn 10617 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
307 | 306 | mulid2d 9661 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
308 | 303, 300,
298 | ltmul1d 11379 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
309 | 262, 308 | mpbii 215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
310 | 307, 309 | eqbrtrrd 4425 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
311 | 303, 301,
302, 305, 310 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
312 | 303, 302 | posdifd 10200 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
       |
313 | 311, 312 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . 21
       |
314 | 304, 313 | elrpd 11338 |
. . . . . . . . . . . . . . . . . . . 20
       |
315 | 299, 314 | rpdivcld 11358 |
. . . . . . . . . . . . . . . . . . 19
           |
316 | 158 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
317 | 298 | rpge0d 11345 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
318 | 300, 301,
316, 317 | mulge0d 10190 |
. . . . . . . . . . . . . . . . . . . . 21
     |
319 | 302, 318 | ge0p1rpd 11368 |
. . . . . . . . . . . . . . . . . . . 20
       |
320 | 299, 319 | rpdivcld 11358 |
. . . . . . . . . . . . . . . . . . 19
           |
321 | 315, 320 | rpmulcld 11357 |
. . . . . . . . . . . . . . . . . 18
                     |
322 | 287, 294,
295, 321 | fvmptd 5954 |
. . . . . . . . . . . . . . . . 17
                         |
323 | 322, 321 | eqeltrd 2529 |
. . . . . . . . . . . . . . . 16
       |
324 | 286, 323 | syl 17 |
. . . . . . . . . . . . . . 15
 
           |
325 | | rpmulcl 11324 |
. . . . . . . . . . . . . . . 16
       |
326 | 325 | adantl 468 |
. . . . . . . . . . . . . . 15
  
      |
327 | 249, 324,
326 | seqcl 12233 |
. . . . . . . . . . . . . 14
         |
328 | 327 | rpcnne0d 11350 |
. . . . . . . . . . . . 13
                 |
329 | 296 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
330 | 155, 161 | ge0p1rpd 11368 |
. . . . . . . . . . . . . . . . 17
     |
331 | 329, 330 | rpmulcld 11357 |
. . . . . . . . . . . . . . . 16
       |
332 | 154, 155,
159, 161 | mulge0d 10190 |
. . . . . . . . . . . . . . . . 17
     |
333 | 183, 332 | ge0p1rpd 11368 |
. . . . . . . . . . . . . . . 16
       |
334 | 331, 333 | rpdivcld 11358 |
. . . . . . . . . . . . . . 15
             |
335 | 329, 264 | rpmulcld 11357 |
. . . . . . . . . . . . . . . . 17
     |
336 | 335, 221 | rpaddcld 11356 |
. . . . . . . . . . . . . . . 16
       |
337 | 331, 336 | rpdivcld 11358 |
. . . . . . . . . . . . . . 15
             |
338 | 334, 337 | rpmulcld 11357 |
. . . . . . . . . . . . . 14
                         |
339 | 338 | rpcnne0d 11350 |
. . . . . . . . . . . . 13
                                                 |
340 | | divdiv1 10318 |
. . . . . . . . . . . . 13
                                                                                                                                 |
341 | 129, 328,
339, 340 | syl3anc 1268 |
. . . . . . . . . . . 12
                                                                   |
342 | 341 | eqcomd 2457 |
. . . . . . . . . . 11
                                                                   |
343 | 342 | oveq2d 6306 |
. . . . . . . . . 10
                                                                           |
344 | 65 | a1i 11 |
. . . . . . . . . . 11
 
   |
345 | 327 | rpcnd 11343 |
. . . . . . . . . . . 12
         |
346 | 327 | rpne0d 11346 |
. . . . . . . . . . . 12
         |
347 | 345, 346 | reccld 10376 |
. . . . . . . . . . 11
           |
348 | 338 | rpcnd 11343 |
. . . . . . . . . . 11
                         |
349 | 338 | rpne0d 11346 |
. . . . . . . . . . 11
                         |
350 | 344, 347,
348, 349 | divassd 10418 |
. . . . . . . . . 10
                                                                           |
351 | 139, 268 | eqnetrrd 2692 |
. . . . . . . . . . . . 13
       |
352 | 201, 199,
201, 213, 351, 224 | divmuldivd 10424 |
. . . . . . . . . . . 12
                                               |
353 | 352 | oveq2d 6306 |
. . . . . . . . . . 11
                                                                           |
354 | 344, 347 | mulcld 9663 |
. . . . . . . . . . . . 13
               |
355 | 201, 201 | mulcld 9663 |
. . . . . . . . . . . . 13
             |
356 | 199, 213 | mulcld 9663 |
. . . . . . . . . . . . 13
             |
357 | 201, 201,
205, 205 | mulne0d 10264 |
. . . . . . . . . . . . 13
             |
358 | 199, 213,
351, 224 | mulne0d 10264 |
. . . . . . . . . . . . 13
             |
359 | 354, 355,
356, 357, 358 | divdiv2d 10415 |
. . . . . . . . . . . 12
                                                                           |
360 | 354, 356,
355, 357 | divassd 10418 |
. . . . . . . . . . . 12
                                                                           |
361 | 359, 360 | eqtrd 2485 |
. . . . . . . . . . 11
                                                                           |
362 | 199, 201,
201, 213, 205, 224, 205 | divdivdivd 10430 |
. . . . . . . . . . . . 13
                                               |
363 | 362 | eqcomd 2457 |
. . . . . . . . . . . 12
                                               |
364 | 363 | oveq2d 6306 |
. . . . . . . . . . 11
                                                                           |
365 | 353, 361,
364 | 3eqtrd 2489 |
. . . . . . . . . 10
                                                                           |
366 | 343, 350,
365 | 3eqtr2d 2491 |
. . . . . . . . 9
                                                                           |
367 | 61 | a1i 11 |
. . . . . . . . . . . 12
   |
368 | 367 | halfcld 10857 |
. . . . . . . . . . 11
 
   |
369 | 368, 347 | mulcld 9663 |
. . . . . . . . . 10
               |
370 | 206, 225,
226 | divcld 10383 |
. . . . . . . . . 10
                         |
371 | 369, 370 | mulcomd 9664 |
. . . . . . . . 9
                                                                           |
372 | 284, 366,
371 | 3eqtrd 2489 |
. . . . . . . 8
                                                                               |
373 | 278, 372 | eqtrd 2485 |
. . . . . . 7
                                                     |
374 | 373 | adantr 467 |
. . . . . 6
                              
 
                                                  |
375 | 126, 247,
374 | 3eqtr4d 2495 |
. . . . 5
                              
                                    |
376 | 375 | ex 436 |
. . . 4
                                                                   |
377 | 9, 18, 27, 36, 124, 376 | nnind 10627 |
. . 3
                               |
378 | 377 | mpteq2ia 4485 |
. 2
                                 |
379 | | wallispilem4.3 |
. 2
                   |
380 | | wallispilem4.4 |
. 2
               |
381 | 378, 379,
380 | 3eqtr4i 2483 |
1
 |