Step | Hyp | Ref
| Expression |
1 | | 0nn0 9190 |
. . . . . . . . 9
 |
2 | | nn0uz 9561 |
. . . . . . . . 9
     |
3 | 1, 2 | eleqtri 2252 |
. . . . . . . 8
     |
4 | 3 | a1i 9 |
. . . . . . 7
      |
5 | | elnn0uz 9564 |
. . . . . . . . . 10

      |
6 | 5 | biimpri 133 |
. . . . . . . . 9
    
  |
7 | | faccl 10714 |
. . . . . . . . . . . 12

      |
8 | 7 | nnrecred 8965 |
. . . . . . . . . . 11

        |
9 | | fveq2 5515 |
. . . . . . . . . . . . 13
           |
10 | 9 | oveq2d 5890 |
. . . . . . . . . . . 12
               |
11 | | erelem1.2 |
. . . . . . . . . . . 12
         |
12 | 10, 11 | fvmptg 5592 |
. . . . . . . . . . 11
                     |
13 | 8, 12 | mpdan 421 |
. . . . . . . . . 10

            |
14 | 13, 8 | eqeltrd 2254 |
. . . . . . . . 9

      |
15 | 6, 14 | syl 14 |
. . . . . . . 8
    
      |
16 | 15 | adantl 277 |
. . . . . . 7
     
      |
17 | | readdcl 7936 |
. . . . . . . 8
 
     |
18 | 17 | adantl 277 |
. . . . . . 7
        |
19 | 4, 16, 18 | seq3p1 10461 |
. . . . . 6
                        |
20 | | 0zd 9264 |
. . . . . . . . 9
  |
21 | 20, 16, 18 | seq3-1 10459 |
. . . . . . . 8
            |
22 | | fveq2 5515 |
. . . . . . . . . . . . 13
           |
23 | | fac0 10707 |
. . . . . . . . . . . . 13
     |
24 | 22, 23 | eqtrdi 2226 |
. . . . . . . . . . . 12
       |
25 | 24 | oveq2d 5890 |
. . . . . . . . . . 11
           |
26 | | ax-1cn 7903 |
. . . . . . . . . . . 12
 |
27 | 26 | div1i 8696 |
. . . . . . . . . . 11
   |
28 | 25, 27 | eqtrdi 2226 |
. . . . . . . . . 10
         |
29 | | 1ex 7951 |
. . . . . . . . . 10
 |
30 | 28, 11, 29 | fvmpt 5593 |
. . . . . . . . 9

      |
31 | 1, 30 | mp1i 10 |
. . . . . . . 8
      |
32 | 21, 31 | eqtrd 2210 |
. . . . . . 7
        |
33 | | 1e0p1 9424 |
. . . . . . . . 9
   |
34 | 33 | fveq2i 5518 |
. . . . . . . 8
           |
35 | | 1nn0 9191 |
. . . . . . . . 9
 |
36 | | fveq2 5515 |
. . . . . . . . . . . . 13
           |
37 | | fac1 10708 |
. . . . . . . . . . . . 13
     |
38 | 36, 37 | eqtrdi 2226 |
. . . . . . . . . . . 12
       |
39 | 38 | oveq2d 5890 |
. . . . . . . . . . 11
           |
40 | 39, 27 | eqtrdi 2226 |
. . . . . . . . . 10
         |
41 | 40, 11, 29 | fvmpt 5593 |
. . . . . . . . 9

      |
42 | 35, 41 | mp1i 10 |
. . . . . . . 8
      |
43 | 34, 42 | eqtr3id 2224 |
. . . . . . 7
        |
44 | 32, 43 | oveq12d 5892 |
. . . . . 6
                  |
45 | 19, 44 | eqtrd 2210 |
. . . . 5
            |
46 | 33 | fveq2i 5518 |
. . . . 5
               |
47 | | df-2 8977 |
. . . . 5
   |
48 | 45, 46, 47 | 3eqtr4g 2235 |
. . . 4
        |
49 | 35 | a1i 9 |
. . . . 5
  |
50 | | nn0z 9272 |
. . . . . . . . . . . 12

  |
51 | | 1exp 10548 |
. . . . . . . . . . . 12
       |
52 | 50, 51 | syl 14 |
. . . . . . . . . . 11

      |
53 | 52 | oveq1d 5889 |
. . . . . . . . . 10

                  |
54 | 53 | mpteq2ia 4089 |
. . . . . . . . 9

                    |
55 | 11, 54 | eqtr4i 2201 |
. . . . . . . 8
             |
56 | 55 | efcvg 11673 |
. . . . . . 7
          |
57 | 26, 56 | mp1i 10 |
. . . . . 6
         |
58 | | df-e 11656 |
. . . . . 6
     |
59 | 57, 58 | breqtrrdi 4045 |
. . . . 5
     |
60 | 13 | adantl 277 |
. . . . . 6
              |
61 | 7 | adantl 277 |
. . . . . . 7
        |
62 | 61 | nnrecred 8965 |
. . . . . 6
          |
63 | 60, 62 | eqeltrd 2254 |
. . . . 5
        |
64 | 61 | nnred 8931 |
. . . . . . 7
        |
65 | 61 | nngt0d 8962 |
. . . . . . 7
        |
66 | | 1re 7955 |
. . . . . . . 8
 |
67 | | 0le1 8437 |
. . . . . . . 8
 |
68 | | divge0 8829 |
. . . . . . . 8
  
           
        |
69 | 66, 67, 68 | mpanl12 436 |
. . . . . . 7
          
        |
70 | 64, 65, 69 | syl2anc 411 |
. . . . . 6
          |
71 | 70, 60 | breqtrrd 4031 |
. . . . 5
        |
72 | 2, 49, 59, 63, 71 | climserle 11352 |
. . . 4
        |
73 | 48, 72 | eqbrtrrd 4027 |
. . 3
  |
74 | 73 | mptru 1362 |
. 2
 |
75 | | nnuz 9562 |
. . . . . 6
     |
76 | | 1zzd 9279 |
. . . . . 6
  |
77 | 1 | a1i 9 |
. . . . . . . 8
  |
78 | 63 | recnd 7985 |
. . . . . . . 8
        |
79 | 2, 77, 78, 59 | clim2ser 11344 |
. . . . . . 7
               |
80 | | 0p1e1 9032 |
. . . . . . . 8
   |
81 | | seqeq1 10447 |
. . . . . . . 8
             |
82 | 80, 81 | ax-mp 5 |
. . . . . . 7
         |
83 | 32 | mptru 1362 |
. . . . . . . 8
       |
84 | 83 | oveq2i 5885 |
. . . . . . 7
           |
85 | 79, 82, 84 | 3brtr3g 4036 |
. . . . . 6
       |
86 | | 2cnd 8991 |
. . . . . . . 8
  |
87 | | halfre 9131 |
. . . . . . . . . . . . . . 15
   |
88 | 87 | a1i 9 |
. . . . . . . . . . . . . 14

    |
89 | | id 19 |
. . . . . . . . . . . . . 14

  |
90 | 88, 89 | reexpcld 10670 |
. . . . . . . . . . . . 13

        |
91 | | oveq2 5882 |
. . . . . . . . . . . . . 14
               |
92 | | eqid 2177 |
. . . . . . . . . . . . . 14

                |
93 | 91, 92 | fvmptg 5592 |
. . . . . . . . . . . . 13
          
                  |
94 | 90, 93 | mpdan 421 |
. . . . . . . . . . . 12

                    |
95 | 94 | adantl 277 |
. . . . . . . . . . 11
                      |
96 | | simpr 110 |
. . . . . . . . . . . . 13
    |
97 | | reexpcl 10536 |
. . . . . . . . . . . . 13
   
         |
98 | 87, 96, 97 | sylancr 414 |
. . . . . . . . . . . 12
          |
99 | 98 | recnd 7985 |
. . . . . . . . . . 11
          |
100 | 95, 99 | eqeltrd 2254 |
. . . . . . . . . 10
                |
101 | | 1lt2 9087 |
. . . . . . . . . . . . . 14
 |
102 | | 2re 8988 |
. . . . . . . . . . . . . . 15
 |
103 | | 0le2 9008 |
. . . . . . . . . . . . . . 15
 |
104 | | absid 11079 |
. . . . . . . . . . . . . . 15
         |
105 | 102, 103,
104 | mp2an 426 |
. . . . . . . . . . . . . 14
     |
106 | 101, 105 | breqtrri 4030 |
. . . . . . . . . . . . 13
     |
107 | 106 | a1i 9 |
. . . . . . . . . . . 12
      |
108 | 86, 107, 95 | georeclim 11520 |
. . . . . . . . . . 11
                 |
109 | | 2m1e1 9036 |
. . . . . . . . . . . . 13
   |
110 | 109 | oveq2i 5885 |
. . . . . . . . . . . 12
       |
111 | | 2cn 8989 |
. . . . . . . . . . . . 13
 |
112 | 111 | div1i 8696 |
. . . . . . . . . . . 12
   |
113 | 110, 112 | eqtri 2198 |
. . . . . . . . . . 11
     |
114 | 108, 113 | breqtrdi 4044 |
. . . . . . . . . 10
             |
115 | 2, 77, 100, 114 | clim2ser 11344 |
. . . . . . . . 9
                               |
116 | | seqeq1 10447 |
. . . . . . . . . 10
                             |
117 | 80, 116 | ax-mp 5 |
. . . . . . . . 9
                         |
118 | 6 | adantl 277 |
. . . . . . . . . . . . . . 15
     
  |
119 | 94, 90 | eqeltrd 2254 |
. . . . . . . . . . . . . . 15

              |
120 | 118, 119 | syl 14 |
. . . . . . . . . . . . . 14
     
              |
121 | 20, 120, 18 | seq3-1 10459 |
. . . . . . . . . . . . 13
               
            |
122 | | halfcn 9132 |
. . . . . . . . . . . . . . . . 17
   |
123 | | exp0 10523 |
. . . . . . . . . . . . . . . . 17
           |
124 | 122, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
       |
125 | 124, 35 | eqeltri 2250 |
. . . . . . . . . . . . . . 15
       |
126 | | oveq2 5882 |
. . . . . . . . . . . . . . . 16
               |
127 | 126, 92 | fvmptg 5592 |
. . . . . . . . . . . . . . 15
                             |
128 | 1, 125, 127 | mp2an 426 |
. . . . . . . . . . . . . 14
                   |
129 | 128, 124 | eqtri 2198 |
. . . . . . . . . . . . 13
             |
130 | 121, 129 | eqtrdi 2226 |
. . . . . . . . . . . 12
                |
131 | 130 | mptru 1362 |
. . . . . . . . . . 11
               |
132 | 131 | oveq2i 5885 |
. . . . . . . . . 10
                   |
133 | 132, 109 | eqtri 2198 |
. . . . . . . . 9
                 |
134 | 115, 117,
133 | 3brtr3g 4036 |
. . . . . . . 8
             |
135 | | nnnn0 9182 |
. . . . . . . . 9
   |
136 | 135, 100 | sylan2 286 |
. . . . . . . 8
                |
137 | 102 | a1i 9 |
. . . . . . . . . . . 12
   |
138 | 135, 90 | syl 14 |
. . . . . . . . . . . 12
         |
139 | 137, 138 | remulcld 7987 |
. . . . . . . . . . 11
           |
140 | 91 | oveq2d 5890 |
. . . . . . . . . . . 12
                   |
141 | | erelem1.1 |
. . . . . . . . . . . 12
           |
142 | 140, 141 | fvmptg 5592 |
. . . . . . . . . . 11
                         |
143 | 139, 142 | mpdan 421 |
. . . . . . . . . 10
               |
144 | 143 | adantl 277 |
. . . . . . . . 9
                |
145 | 135, 95 | sylan2 286 |
. . . . . . . . . 10
                      |
146 | 145 | oveq2d 5890 |
. . . . . . . . 9
                          |
147 | 144, 146 | eqtr4d 2213 |
. . . . . . . 8
                      |
148 | 75, 76, 86, 134, 136, 147 | isermulc2 11347 |
. . . . . . 7
       |
149 | | 2t1e2 9071 |
. . . . . . 7
   |
150 | 148, 149 | breqtrdi 4044 |
. . . . . 6
     |
151 | 135, 63 | sylan2 286 |
. . . . . 6
        |
152 | | remulcl 7938 |
. . . . . . . . 9
                   |
153 | 102, 98, 152 | sylancr 414 |
. . . . . . . 8
            |
154 | 135, 153 | sylan2 286 |
. . . . . . 7
            |
155 | 144, 154 | eqeltrd 2254 |
. . . . . 6
        |
156 | | faclbnd2 10721 |
. . . . . . . . . . 11

            |
157 | 156 | adantl 277 |
. . . . . . . . . 10
              |
158 | | 2nn 9079 |
. . . . . . . . . . . . . 14
 |
159 | | nnexpcl 10532 |
. . . . . . . . . . . . . 14
 
       |
160 | 158, 96, 159 | sylancr 414 |
. . . . . . . . . . . . 13
        |
161 | 160 | nnrpd 9693 |
. . . . . . . . . . . 12
        |
162 | 161 | rphalfcld 9708 |
. . . . . . . . . . 11
          |
163 | 61 | nnrpd 9693 |
. . . . . . . . . . 11
        |
164 | 162, 163 | lerecd 9715 |
. . . . . . . . . 10
        
   
                 |
165 | 157, 164 | mpbid 147 |
. . . . . . . . 9
                  |
166 | | 2cnd 8991 |
. . . . . . . . . . 11
    |
167 | 160 | nncnd 8932 |
. . . . . . . . . . 11
        |
168 | 160 | nnap0d 8964 |
. . . . . . . . . . 11
      #   |
169 | 166, 167,
168 | divrecapd 8749 |
. . . . . . . . . 10
                  |
170 | | 2ap0 9011 |
. . . . . . . . . . . 12
#  |
171 | 170 | a1i 9 |
. . . . . . . . . . 11
  #   |
172 | 167, 166,
168, 171 | recdivapd 8763 |
. . . . . . . . . 10
                  |
173 | | nn0z 9272 |
. . . . . . . . . . . . 13

  |
174 | 173 | adantl 277 |
. . . . . . . . . . . 12
    |
175 | 166, 171,
174 | exprecapd 10661 |
. . . . . . . . . . 11
                |
176 | 175 | oveq2d 5890 |
. . . . . . . . . 10
                    |
177 | 169, 172,
176 | 3eqtr4rd 2221 |
. . . . . . . . 9
                    |
178 | 165, 177 | breqtrrd 4031 |
. . . . . . . 8
                  |
179 | 135, 178 | sylan2 286 |
. . . . . . 7
                  |
180 | 135, 60 | sylan2 286 |
. . . . . . 7
              |
181 | 179, 180,
144 | 3brtr4d 4035 |
. . . . . 6
            |
182 | 75, 76, 85, 150, 151, 155, 181 | iserle 11349 |
. . . . 5
 
  |
183 | 182 | mptru 1362 |
. . . 4
   |
184 | | ere 11677 |
. . . . 5
 |
185 | 184, 66, 102 | lesubaddi 8462 |
. . . 4
  
    |
186 | 183, 185 | mpbi 145 |
. . 3
   |
187 | | df-3 8978 |
. . 3
   |
188 | 186, 187 | breqtrri 4030 |
. 2
 |
189 | 74, 188 | pm3.2i 272 |
1
   |