Step | Hyp | Ref
| Expression |
1 | | nn0uz 11217 |
. . 3
     |
2 | | 0zd 10973 |
. . 3
   |
3 | | 1rp 11329 |
. . . 4
 |
4 | 3 | a1i 11 |
. . 3
   |
5 | | radcnvlem2.y |
. . . 4
   |
6 | | pser.g |
. . . . 5
 
             |
7 | 6 | pserval2 23445 |
. . . 4
 
                     |
8 | 5, 7 | sylan 479 |
. . 3
 

                    |
9 | | fvex 5889 |
. . . . 5
     |
10 | 9 | a1i 11 |
. . . 4
       |
11 | | radcnvlem2.c |
. . . 4
         |
12 | | radcnv.a |
. . . . . 6
       |
13 | 6, 12, 5 | psergf 23446 |
. . . . 5
           |
14 | 13 | ffvelrnda 6037 |
. . . 4
 

          |
15 | 1, 2, 10, 11, 14 | serf0 13824 |
. . 3
       |
16 | 1, 2, 4, 8, 15 | climi0 13653 |
. 2
                        |
17 | | simprl 772 |
. . 3
 
                      
  |
18 | | nn0re 10902 |
. . . . . . 7

  |
19 | 18 | adantl 473 |
. . . . . 6
                             |
20 | | psergf.x |
. . . . . . . . . 10
   |
21 | 20 | adantr 472 |
. . . . . . . . 9
 
                      
  |
22 | 21 | abscld 13575 |
. . . . . . . 8
 
                      
      |
23 | 5 | adantr 472 |
. . . . . . . . 9
 
                      
  |
24 | 23 | abscld 13575 |
. . . . . . . 8
 
                      
      |
25 | | 0red 9662 |
. . . . . . . . . . 11
   |
26 | 20 | abscld 13575 |
. . . . . . . . . . 11
       |
27 | 5 | abscld 13575 |
. . . . . . . . . . 11
       |
28 | 20 | absge0d 13583 |
. . . . . . . . . . 11

      |
29 | | radcnvlem2.a |
. . . . . . . . . . 11
    
      |
30 | 25, 26, 27, 28, 29 | lelttrd 9810 |
. . . . . . . . . 10
       |
31 | 30 | gt0ne0d 10199 |
. . . . . . . . 9
       |
32 | 31 | adantr 472 |
. . . . . . . 8
 
                      
      |
33 | 22, 24, 32 | redivcld 10457 |
. . . . . . 7
 
                      
            |
34 | | reexpcl 12327 |
. . . . . . 7
                             |
35 | 33, 34 | sylan 479 |
. . . . . 6
                                           |
36 | 19, 35 | remulcld 9689 |
. . . . 5
                                             |
37 | | eqid 2471 |
. . . . 5

                                    |
38 | 36, 37 | fmptd 6061 |
. . . 4
 
                      
                        |
39 | 38 | ffvelrnda 6037 |
. . 3
                                                   |
40 | | nn0re 10902 |
. . . . . . . . 9

  |
41 | 40 | adantl 473 |
. . . . . . . 8
 

  |
42 | 6, 12, 20 | psergf 23446 |
. . . . . . . . . 10
           |
43 | 42 | ffvelrnda 6037 |
. . . . . . . . 9
 

          |
44 | 43 | abscld 13575 |
. . . . . . . 8
 

              |
45 | 41, 44 | remulcld 9689 |
. . . . . . 7
 

                |
46 | | radcnvlem1.h |
. . . . . . 7
 
               |
47 | 45, 46 | fmptd 6061 |
. . . . . 6
       |
48 | 47 | adantr 472 |
. . . . 5
 
                      
      |
49 | 48 | ffvelrnda 6037 |
. . . 4
                                 |
50 | 49 | recnd 9687 |
. . 3
                                 |
51 | 26, 27, 31 | redivcld 10457 |
. . . . . 6
             |
52 | 51 | recnd 9687 |
. . . . 5
             |
53 | | divge0 10496 |
. . . . . . . 8
                      
            |
54 | 26, 28, 27, 30, 53 | syl22anc 1293 |
. . . . . . 7

            |
55 | 51, 54 | absidd 13561 |
. . . . . 6
                           |
56 | 27 | recnd 9687 |
. . . . . . . . 9
       |
57 | 56 | mulid1d 9678 |
. . . . . . . 8
             |
58 | 29, 57 | breqtrrd 4422 |
. . . . . . 7
    
        |
59 | | 1red 9676 |
. . . . . . . 8
   |
60 | | ltdivmul 10502 |
. . . . . . . 8
     
                     
             |
61 | 26, 59, 27, 30, 60 | syl112anc 1296 |
. . . . . . 7
           
             |
62 | 58, 61 | mpbird 240 |
. . . . . 6
             |
63 | 55, 62 | eqbrtrd 4416 |
. . . . 5
                 |
64 | 37 | geomulcvg 14009 |
. . . . 5
                                                 |
65 | 52, 63, 64 | syl2anc 673 |
. . . 4
                       |
66 | 65 | adantr 472 |
. . 3
 
                      
                      |
67 | | 1red 9676 |
. . 3
 
                      
  |
68 | 42 | ad2antrr 740 |
. . . . . . . 8
                              
          |
69 | | eluznn0 11251 |
. . . . . . . . 9
 
    
  |
70 | 17, 69 | sylan 479 |
. . . . . . . 8
                              
  |
71 | 68, 70 | ffvelrnd 6038 |
. . . . . . 7
                              
          |
72 | 71 | abscld 13575 |
. . . . . 6
                              
              |
73 | 33 | adantr 472 |
. . . . . . 7
                              
            |
74 | 73, 70 | reexpcld 12471 |
. . . . . 6
                              
                |
75 | 70 | nn0red 10950 |
. . . . . 6
                              
  |
76 | 70 | nn0ge0d 10952 |
. . . . . 6
                              
  |
77 | 12 | ad2antrr 740 |
. . . . . . . . . . . . 13
                              
      |
78 | 77, 70 | ffvelrnd 6038 |
. . . . . . . . . . . 12
                              
      |
79 | 5 | ad2antrr 740 |
. . . . . . . . . . . . 13
                              
  |
80 | 79, 70 | expcld 12454 |
. . . . . . . . . . . 12
                              
      |
81 | 78, 80 | mulcld 9681 |
. . . . . . . . . . 11
                              
            |
82 | 81 | abscld 13575 |
. . . . . . . . . 10
                              
                |
83 | | 1red 9676 |
. . . . . . . . . 10
                              
  |
84 | 20 | ad2antrr 740 |
. . . . . . . . . . . 12
                              
  |
85 | 84 | abscld 13575 |
. . . . . . . . . . 11
                              
      |
86 | 85, 70 | reexpcld 12471 |
. . . . . . . . . 10
                              
          |
87 | 84 | absge0d 13583 |
. . . . . . . . . . 11
                              
      |
88 | 85, 70, 87 | expge0d 12472 |
. . . . . . . . . 10
                              
          |
89 | | simprr 774 |
. . . . . . . . . . . 12
 
                      
                      |
90 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
           |
91 | | oveq2 6316 |
. . . . . . . . . . . . . . . 16
           |
92 | 90, 91 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
                       |
93 | 92 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                               |
94 | 93 | breq1d 4405 |
. . . . . . . . . . . . 13
                                 |
95 | 94 | rspccva 3135 |
. . . . . . . . . . . 12
                          
                |
96 | 89, 95 | sylan 479 |
. . . . . . . . . . 11
                              
                |
97 | | 1re 9660 |
. . . . . . . . . . . 12
 |
98 | | ltle 9740 |
. . . . . . . . . . . 12
               
                             
   |
99 | 82, 97, 98 | sylancl 675 |
. . . . . . . . . . 11
                              
              
             
   |
100 | 96, 99 | mpd 15 |
. . . . . . . . . 10
                              
             
  |
101 | 82, 83, 86, 88, 100 | lemul1ad 10568 |
. . . . . . . . 9
                              
                       
            |
102 | 84, 70 | expcld 12454 |
. . . . . . . . . . . 12
                              
      |
103 | 78, 102 | mulcld 9681 |
. . . . . . . . . . 11
                              
            |
104 | 103, 80 | absmuld 13593 |
. . . . . . . . . 10
                              
                                              |
105 | 81, 102 | absmuld 13593 |
. . . . . . . . . . 11
                              
                                              |
106 | 78, 80, 102 | mul32d 9861 |
. . . . . . . . . . . 12
                              
                                  |
107 | 106 | fveq2d 5883 |
. . . . . . . . . . 11
                              
                                          |
108 | 84, 70 | absexpd 13591 |
. . . . . . . . . . . 12
                              
                  |
109 | 108 | oveq2d 6324 |
. . . . . . . . . . 11
                              
                                                  |
110 | 105, 107,
109 | 3eqtr3d 2513 |
. . . . . . . . . 10
                              
                                              |
111 | 79, 70 | absexpd 13591 |
. . . . . . . . . . 11
                              
                  |
112 | 111 | oveq2d 6324 |
. . . . . . . . . 10
                              
                                                  |
113 | 104, 110,
112 | 3eqtr3d 2513 |
. . . . . . . . 9
                              
                                                  |
114 | 86 | recnd 9687 |
. . . . . . . . . 10
                              
          |
115 | 114 | mulid2d 9679 |
. . . . . . . . 9
                              
                    |
116 | 101, 113,
115 | 3brtr3d 4425 |
. . . . . . . 8
                              
                       
          |
117 | 103 | abscld 13575 |
. . . . . . . . 9
                              
                |
118 | 24 | adantr 472 |
. . . . . . . . . 10
                              
      |
119 | 118, 70 | reexpcld 12471 |
. . . . . . . . 9
                              
          |
120 | | eluzelz 11192 |
. . . . . . . . . . 11
    
  |
121 | 120 | adantl 473 |
. . . . . . . . . 10
                              
  |
122 | 30 | ad2antrr 740 |
. . . . . . . . . 10
                              
      |
123 | | expgt0 12343 |
. . . . . . . . . 10
     
               |
124 | 118, 121,
122, 123 | syl3anc 1292 |
. . . . . . . . 9
                              
          |
125 | | lemuldiv 10508 |
. . . . . . . . 9
                                                                                         
                     |
126 | 117, 86, 119, 124, 125 | syl112anc 1296 |
. . . . . . . 8
                              
                                              
                     |
127 | 116, 126 | mpbid 215 |
. . . . . . 7
                              
             
                    |
128 | 6 | pserval2 23445 |
. . . . . . . . 9
 
                     |
129 | 84, 70, 128 | syl2anc 673 |
. . . . . . . 8
                              
                    |
130 | 129 | fveq2d 5883 |
. . . . . . 7
                              
                            |
131 | 22 | recnd 9687 |
. . . . . . . . 9
 
                      
      |
132 | 131 | adantr 472 |
. . . . . . . 8
                              
      |
133 | 24 | recnd 9687 |
. . . . . . . . 9
 
                      
      |
134 | 133 | adantr 472 |
. . . . . . . 8
                              
      |
135 | 31 | ad2antrr 740 |
. . . . . . . 8
                              
      |
136 | 132, 134,
135, 70 | expdivd 12468 |
. . . . . . 7
                              
                                  |
137 | 127, 130,
136 | 3brtr4d 4426 |
. . . . . 6
                              
                            |
138 | 72, 74, 75, 76, 137 | lemul2ad 10569 |
. . . . 5
                              
                                |
139 | 75, 72 | remulcld 9689 |
. . . . . 6
                              
                |
140 | 71 | absge0d 13583 |
. . . . . . 7
                              
              |
141 | 75, 72, 76, 140 | mulge0d 10211 |
. . . . . 6
                              
                |
142 | 139, 141 | absidd 13561 |
. . . . 5
                              
                                  |
143 | 75, 74 | remulcld 9689 |
. . . . . . 7
                              
                  |
144 | 143 | recnd 9687 |
. . . . . 6
                              
                  |
145 | 144 | mulid2d 9679 |
. . . . 5
                              
                                    |
146 | 138, 142,
145 | 3brtr4d 4426 |
. . . 4
                              
                 
                    |
147 | | ovex 6336 |
. . . . . 6
               |
148 | 46 | fvmpt2 5972 |
. . . . . 6
  
                                  |
149 | 70, 147, 148 | sylancl 675 |
. . . . 5
                              
                    |
150 | 149 | fveq2d 5883 |
. . . 4
                              
                            |
151 | | id 22 |
. . . . . . . 8
   |
152 | | oveq2 6316 |
. . . . . . . 8
                               |
153 | 151, 152 | oveq12d 6326 |
. . . . . . 7
                                   |
154 | | ovex 6336 |
. . . . . . 7
                 |
155 | 153, 37, 154 | fvmpt 5963 |
. . . . . 6

                                        |
156 | 70, 155 | syl 17 |
. . . . 5
                              
                                        |
157 | 156 | oveq2d 6324 |
. . . 4
                              
  
                                         |
158 | 146, 150,
157 | 3brtr4d 4426 |
. . 3
                              
                                  |
159 | 1, 17, 39, 50, 66, 67, 158 | cvgcmpce 13955 |
. 2
 
                      
    |
160 | 16, 159 | rexlimddv 2875 |
1
     |