Step | Hyp | Ref
| Expression |
1 | | cvg1n.f |
. . . 4
       |
2 | | cvg1n.c |
. . . 4
   |
3 | | cvg1n.cau |
. . . 4
                                    |
4 | | cvg1nlem.g |
. . . 4
         |
5 | | cvg1nlem.z |
. . . 4
   |
6 | | cvg1nlem.start |
. . . 4
   |
7 | 1, 2, 3, 4, 5, 6 | cvg1nlemf 10992 |
. . 3
       |
8 | 1, 2, 3, 4, 5, 6 | cvg1nlemcau 10993 |
. . 3
                                    |
9 | 7, 8 | caucvgre 10990 |
. 2
                          |
10 | | fveq2 5516 |
. . . . . . . . . . 11
           |
11 | 10 | raleqdv 2679 |
. . . . . . . . . 10
  
         
        
                       |
12 | 11 | cbvrexv 2705 |
. . . . . . . . 9
  
                  
                       |
13 | 12 | ralbii 2483 |
. . . . . . . 8
 
                       
                     |
14 | 13 | anbi2i 457 |
. . . . . . 7
    
                     
                            |
15 | 14 | anbi1i 458 |
. . . . . 6
   
   
                   

  
 
                         |
16 | | oveq2 5883 |
. . . . . . . . . . . 12
           |
17 | 16 | breq2d 4016 |
. . . . . . . . . . 11
       
 
           |
18 | | oveq2 5883 |
. . . . . . . . . . . 12
                   |
19 | 18 | breq2d 4016 |
. . . . . . . . . . 11
   
     
           |
20 | 17, 19 | anbi12d 473 |
. . . . . . . . . 10
                                       |
21 | 20 | rexralbidv 2503 |
. . . . . . . . 9
    
                   
                            |
22 | | simplr 528 |
. . . . . . . . 9
   
   
                   
 
                       |
23 | | simpr 110 |
. . . . . . . . . 10
   
   
                   

  |
24 | 23 | rphalfcld 9709 |
. . . . . . . . 9
   
   
                   
     |
25 | 21, 22, 24 | rspcdva 2847 |
. . . . . . . 8
   
   
                   
 
                          |
26 | 15, 25 | sylbir 135 |
. . . . . . 7
   
   
                   
 
                          |
27 | 2 | rpred 9696 |
. . . . . . . . . . . . . 14
   |
28 | 27 | ad4antr 494 |
. . . . . . . . . . . . 13
                            
            
              
  |
29 | | 2re 8989 |
. . . . . . . . . . . . . 14
 |
30 | 29 | a1i 9 |
. . . . . . . . . . . . 13
                            
            
              
  |
31 | 28, 30 | remulcld 7988 |
. . . . . . . . . . . 12
                            
            
              
    |
32 | | simplr 528 |
. . . . . . . . . . . 12
                            
            
              
  |
33 | 31, 32 | rerpdivcld 9728 |
. . . . . . . . . . 11
                            
            
              
 
    |
34 | 5 | ad4antr 494 |
. . . . . . . . . . 11
                            
            
              
  |
35 | 33, 34 | nndivred 8969 |
. . . . . . . . . 10
                            
            
              
        |
36 | | simprl 529 |
. . . . . . . . . . 11
                            
            
              
  |
37 | 36 | nnred 8932 |
. . . . . . . . . 10
                            
            
              
  |
38 | 35, 37 | readdcld 7987 |
. . . . . . . . 9
                            
            
              
          |
39 | | arch 9173 |
. . . . . . . . 9
                    |
40 | 38, 39 | syl 14 |
. . . . . . . 8
                            
            
              
           |
41 | | simprl 529 |
. . . . . . . . . 10
     

                                                                |
42 | 34 | adantr 276 |
. . . . . . . . . 10
     

                                                             
  |
43 | 41, 42 | nnmulcld 8968 |
. . . . . . . . 9
     

                                                                  |
44 | 1 | ad6antr 498 |
. . . . . . . . . . . . . . 15
        
                                                            
             |
45 | | simplrl 535 |
. . . . . . . . . . . . . . . . 17
        
                                                            
         |
46 | 5 | ad6antr 498 |
. . . . . . . . . . . . . . . . 17
        
                                                            
      
  |
47 | 45, 46 | nnmulcld 8968 |
. . . . . . . . . . . . . . . 16
        
                                                            
           |
48 | | eluznn 9600 |
. . . . . . . . . . . . . . . 16
   
         |
49 | 47, 48 | sylancom 420 |
. . . . . . . . . . . . . . 15
        
                                                            
         |
50 | 44, 49 | ffvelcdmd 5653 |
. . . . . . . . . . . . . 14
        
                                                            
             |
51 | 44, 47 | ffvelcdmd 5653 |
. . . . . . . . . . . . . . 15
        
                                                            
               |
52 | 32 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
        
                                                            
      
  |
53 | 52 | rpred 9696 |
. . . . . . . . . . . . . . . 16
        
                                                            
      
  |
54 | 53 | rehalfcld 9165 |
. . . . . . . . . . . . . . 15
        
                                                            
           |
55 | 51, 54 | readdcld 7987 |
. . . . . . . . . . . . . 14
        
                                                            
                   |
56 | | simpllr 534 |
. . . . . . . . . . . . . . . . 17
   
   
                   
   |
57 | 56 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
        
                                                            
         |
58 | 57, 54 | readdcld 7987 |
. . . . . . . . . . . . . . 15
        
                                                            
             |
59 | 58, 54 | readdcld 7987 |
. . . . . . . . . . . . . 14
        
                                                            
                 |
60 | 27 | ad6antr 498 |
. . . . . . . . . . . . . . . . 17
        
                                                            
      
  |
61 | 60, 47 | nndivred 8969 |
. . . . . . . . . . . . . . . 16
        
                                                            
             |
62 | 51, 61 | readdcld 7987 |
. . . . . . . . . . . . . . 15
        
                                                            
                     |
63 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . 20
           |
64 | 63 | oveq1d 5890 |
. . . . . . . . . . . . . . . . . . 19
                       |
65 | 64 | breq2d 4016 |
. . . . . . . . . . . . . . . . . 18
                 
                   |
66 | 63 | breq1d 4014 |
. . . . . . . . . . . . . . . . . 18
     
           
                   |
67 | 65, 66 | anbi12d 473 |
. . . . . . . . . . . . . . . . 17
                                                                         |
68 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . 19
               |
69 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . . 21
               |
70 | | oveq2 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
71 | 70 | oveq2d 5891 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
72 | 69, 71 | breq12d 4017 |
. . . . . . . . . . . . . . . . . . . 20
       
       
                   |
73 | 69, 70 | oveq12d 5893 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
74 | 73 | breq2d 4016 |
. . . . . . . . . . . . . . . . . . . 20
       
       
                   |
75 | 72, 74 | anbi12d 473 |
. . . . . . . . . . . . . . . . . . 19
                                                                   |
76 | 68, 75 | raleqbidv 2685 |
. . . . . . . . . . . . . . . . . 18
    
         
                    
                                             |
77 | 3 | ad6antr 498 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
       
                                  |
78 | 76, 77, 47 | rspcdva 2847 |
. . . . . . . . . . . . . . . . 17
        
                                                            
       
                                           |
79 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
        
                                                            
               |
80 | 67, 78, 79 | rspcdva 2847 |
. . . . . . . . . . . . . . . 16
        
                                                            
                                           |
81 | 80 | simprd 114 |
. . . . . . . . . . . . . . 15
        
                                                            
          
              |
82 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . 20
   
   
                   

  |
83 | 82 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . . 19
        
                                                            
      
  |
84 | 83 | rpred 9696 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
      
  |
85 | 84 | rehalfcld 9165 |
. . . . . . . . . . . . . . . . 17
        
                                                            
           |
86 | 2 | ad6antr 498 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
      
  |
87 | 36 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
         |
88 | | simplrr 536 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
                 |
89 | 86, 83, 46, 45, 87, 88 | cvg1nlemcxze 10991 |
. . . . . . . . . . . . . . . . 17
        
                                                            
               |
90 | 61, 85, 89 | ltled 8076 |
. . . . . . . . . . . . . . . 16
        
                                                            
          
    |
91 | 61, 54, 51, 90 | leadd2dd 8517 |
. . . . . . . . . . . . . . 15
        
                                                            
                  
            |
92 | 50, 62, 55, 81, 91 | ltletrd 8380 |
. . . . . . . . . . . . . 14
        
                                                            
          
            |
93 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . 20
           |
94 | 93 | breq1d 4014 |
. . . . . . . . . . . . . . . . . . 19
     
   
           |
95 | 93 | oveq1d 5890 |
. . . . . . . . . . . . . . . . . . . 20
                   |
96 | 95 | breq2d 4016 |
. . . . . . . . . . . . . . . . . . 19
 
       
           |
97 | 94, 96 | anbi12d 473 |
. . . . . . . . . . . . . . . . . 18
                                         |
98 | | simprr 531 |
. . . . . . . . . . . . . . . . . . 19
                            
            
              
                          |
99 | 98 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
       
         
               |
100 | 87 | nnred 8932 |
. . . . . . . . . . . . . . . . . . . 20
        
                                                            
         |
101 | 45 | nnred 8932 |
. . . . . . . . . . . . . . . . . . . 20
        
                                                            
         |
102 | | 2rp 9658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
103 | 102 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
                                                            
         |
104 | 86, 103 | rpmulcld 9713 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
                                                            
           |
105 | 104, 83 | rpdivcld 9714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
                                                            
             |
106 | 46 | nnrpd 9694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
                                                            
      
  |
107 | 105, 106 | rpdivcld 9714 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
                                                            
               |
108 | 107 | rpred 9696 |
. . . . . . . . . . . . . . . . . . . . . 22
        
                                                            
               |
109 | 108, 100 | readdcld 7987 |
. . . . . . . . . . . . . . . . . . . . 21
        
                                                            
                 |
110 | 100, 107 | ltaddrp2d 9731 |
. . . . . . . . . . . . . . . . . . . . 21
        
                                                            
      
          |
111 | 100, 109,
101, 110, 88 | lttrd 8083 |
. . . . . . . . . . . . . . . . . . . 20
        
                                                            
      
  |
112 | 100, 101,
111 | ltled 8076 |
. . . . . . . . . . . . . . . . . . 19
        
                                                            
      
  |
113 | 87 | nnzd 9374 |
. . . . . . . . . . . . . . . . . . . 20
        
                                                            
         |
114 | 45 | nnzd 9374 |
. . . . . . . . . . . . . . . . . . . 20
        
                                                            
         |
115 | | eluz 9541 |
. . . . . . . . . . . . . . . . . . . 20
 
     
   |
116 | 113, 114,
115 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
        
                                                            
           
   |
117 | 112, 116 | mpbird 167 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
             |
118 | 97, 99, 117 | rspcdva 2847 |
. . . . . . . . . . . . . . . . 17
        
                                                            
                           |
119 | | oveq1 5882 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
120 | 119 | fveq2d 5520 |
. . . . . . . . . . . . . . . . . . . . 21
               |
121 | 120, 4 | fvmptg 5593 |
. . . . . . . . . . . . . . . . . . . 20
                     |
122 | 45, 51, 121 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
        
                                                            
                   |
123 | 122 | breq1d 4014 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
                             |
124 | 122 | oveq1d 5890 |
. . . . . . . . . . . . . . . . . . 19
        
                                                            
                           |
125 | 124 | breq2d 4016 |
. . . . . . . . . . . . . . . . . 18
        
                                                            
               
             |
126 | 123, 125 | anbi12d 473 |
. . . . . . . . . . . . . . . . 17
        
                                                            
                         
                         |
127 | 118, 126 | mpbid 147 |
. . . . . . . . . . . . . . . 16
        
                                                            
                               |
128 | 127 | simpld 112 |
. . . . . . . . . . . . . . 15
        
                                                            
                   |
129 | 51, 58, 54, 128 | ltadd1dd 8513 |
. . . . . . . . . . . . . 14
        
                                                            
                           |
130 | 50, 55, 59, 92, 129 | lttrd 8083 |
. . . . . . . . . . . . 13
        
                                                            
          
          |
131 | 57 | recnd 7986 |
. . . . . . . . . . . . . 14
        
                                                            
         |
132 | 54 | recnd 7986 |
. . . . . . . . . . . . . 14
        
                                                            
           |
133 | 131, 132,
132 | addassd 7980 |
. . . . . . . . . . . . 13
        
                                                            
                         |
134 | 130, 133 | breqtrd 4030 |
. . . . . . . . . . . 12
        
                                                            
          
          |
135 | 52 | rpcnd 9698 |
. . . . . . . . . . . . . 14
        
                                                            
      
  |
136 | 135 | 2halvesd 9164 |
. . . . . . . . . . . . 13
        
                                                            
               |
137 | 136 | oveq2d 5891 |
. . . . . . . . . . . 12
        
                                                            
                   |
138 | 134, 137 | breqtrd 4030 |
. . . . . . . . . . 11
        
                                                            
          
    |
139 | 50, 54 | readdcld 7987 |
. . . . . . . . . . . . . . 15
        
                                                            
                 |
140 | 139, 54 | readdcld 7987 |
. . . . . . . . . . . . . 14
        
                                                            
                     |
141 | 127 | simprd 114 |
. . . . . . . . . . . . . 14
        
                                                            
      
            |
142 | 50, 61 | readdcld 7987 |
. . . . . . . . . . . . . . . 16
        
                                                            
                   |
143 | 80 | simpld 112 |
. . . . . . . . . . . . . . . 16
        
                                                            
                         |
144 | 61, 54, 50, 90 | leadd2dd 8517 |
. . . . . . . . . . . . . . . 16
        
                                                            
                
          |
145 | 51, 142, 139, 143, 144 | ltletrd 8380 |
. . . . . . . . . . . . . . 15
        
                                                            
                       |
146 | 51, 139, 54, 145 | ltadd1dd 8513 |
. . . . . . . . . . . . . 14
        
                                                            
                               |
147 | 57, 55, 140, 141, 146 | lttrd 8083 |
. . . . . . . . . . . . 13
        
                                                            
      
              |
148 | 50 | recnd 7986 |
. . . . . . . . . . . . . 14
        
                                                            
             |
149 | 148, 132,
132 | addassd 7980 |
. . . . . . . . . . . . 13
        
                                                            
                                 |
150 | 147, 149 | breqtrd 4030 |
. . . . . . . . . . . 12
        
                                                            
      
              |
151 | 136 | oveq2d 5891 |
. . . . . . . . . . . 12
        
                                                            
                           |
152 | 150, 151 | breqtrd 4030 |
. . . . . . . . . . 11
        
                                                            
      
        |
153 | 138, 152 | jca 306 |
. . . . . . . . . 10
        
                                                            
                       |
154 | 153 | ralrimiva 2550 |
. . . . . . . . 9
     

                                                              
           
           |
155 | | fveq2 5516 |
. . . . . . . . . . 11
               |
156 | 155 | raleqdv 2679 |
. . . . . . . . . 10
    
         
        
            
            |
157 | 156 | rspcev 2842 |
. . . . . . . . 9
                           
                      |
158 | 43, 154, 157 | syl2anc 411 |
. . . . . . . 8
     

                                                              
                      |
159 | 40, 158 | rexlimddv 2599 |
. . . . . . 7
                            
            
              
                       |
160 | 26, 159 | rexlimddv 2599 |
. . . . . 6
   
   
                   
 
                      |
161 | 15, 160 | sylbi 121 |
. . . . 5
   
   
                   
 
                      |
162 | 161 | ralrimiva 2550 |
. . . 4
    
                                              |
163 | 162 | ex 115 |
. . 3
 

 
                    
                         |
164 | 163 | reximdva 2579 |
. 2
                                                   |
165 | 9, 164 | mpd 13 |
1
                          |