Step | Hyp | Ref
| Expression |
1 | | nnuz 9563 |
. . 3
     |
2 | | 1zzd 9280 |
. . 3
   |
3 | | climcvg1n.f |
. . . . . . . 8
       |
4 | 3 | ffvelcdmda 5652 |
. . . . . . 7
 

      |
5 | 4 | recld 10947 |
. . . . . 6
 

          |
6 | | climcvg1nlem.g |
. . . . . 6
           |
7 | 5, 6 | fmptd 5671 |
. . . . 5
       |
8 | | climcvg1n.c |
. . . . 5
   |
9 | | climcvg1n.cau |
. . . . . 6
                          |
10 | | eluznn 9600 |
. . . . . . . . . . . . . . 15
 
       |
11 | 10 | adantll 476 |
. . . . . . . . . . . . . 14
        
  |
12 | 3 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
        
      |
13 | 12, 11 | ffvelcdmd 5653 |
. . . . . . . . . . . . . . 15
        
      |
14 | 13 | recld 10947 |
. . . . . . . . . . . . . 14
        
          |
15 | | fveq2 5516 |
. . . . . . . . . . . . . . . 16
           |
16 | 15 | fveq2d 5520 |
. . . . . . . . . . . . . . 15
                   |
17 | 16, 6 | fvmptg 5593 |
. . . . . . . . . . . . . 14
                         |
18 | 11, 14, 17 | syl2anc 411 |
. . . . . . . . . . . . 13
        
              |
19 | | simplr 528 |
. . . . . . . . . . . . . 14
        
  |
20 | 12, 19 | ffvelcdmd 5653 |
. . . . . . . . . . . . . . 15
        
      |
21 | 20 | recld 10947 |
. . . . . . . . . . . . . 14
        
          |
22 | | fveq2 5516 |
. . . . . . . . . . . . . . . 16
           |
23 | 22 | fveq2d 5520 |
. . . . . . . . . . . . . . 15
                   |
24 | 23, 6 | fvmptg 5593 |
. . . . . . . . . . . . . 14
                         |
25 | 19, 21, 24 | syl2anc 411 |
. . . . . . . . . . . . 13
        
              |
26 | 18, 25 | oveq12d 5893 |
. . . . . . . . . . . 12
        
                              |
27 | 13, 20 | resubd 10970 |
. . . . . . . . . . . 12
        
                                  |
28 | 26, 27 | eqtr4d 2213 |
. . . . . . . . . . 11
        
                          |
29 | 28 | fveq2d 5520 |
. . . . . . . . . 10
        
                                  |
30 | 13, 20 | subcld 8268 |
. . . . . . . . . . 11
        
            |
31 | | absrele 11092 |
. . . . . . . . . . 11
                                             |
32 | 30, 31 | syl 14 |
. . . . . . . . . 10
        
                                  |
33 | 29, 32 | eqbrtrd 4026 |
. . . . . . . . 9
        
                              |
34 | 30 | recld 10947 |
. . . . . . . . . . . . 13
        
                |
35 | 34 | recnd 7986 |
. . . . . . . . . . . 12
        
                |
36 | 28, 35 | eqeltrd 2254 |
. . . . . . . . . . 11
        
            |
37 | 36 | abscld 11190 |
. . . . . . . . . 10
        
                |
38 | 30 | abscld 11190 |
. . . . . . . . . 10
        
                |
39 | 8 | ad2antrr 488 |
. . . . . . . . . . . 12
        
  |
40 | 19 | nnrpd 9694 |
. . . . . . . . . . . 12
        
  |
41 | 39, 40 | rpdivcld 9714 |
. . . . . . . . . . 11
        
    |
42 | 41 | rpred 9696 |
. . . . . . . . . 10
        
    |
43 | | lelttr 8046 |
. . . . . . . . . 10
                                                
                                                  |
44 | 37, 38, 42, 43 | syl3anc 1238 |
. . . . . . . . 9
        
               
                                                  |
45 | 33, 44 | mpand 429 |
. . . . . . . 8
        
                                    |
46 | 45 | ralimdva 2544 |
. . . . . . 7
 

 
                     
                        |
47 | 46 | ralimdva 2544 |
. . . . . 6
                         
                         |
48 | 9, 47 | mpd 13 |
. . . . 5
                          |
49 | 7, 8, 48 | climrecvg1n 11356 |
. . . 4
  |
50 | | climdm 11303 |
. . . 4

    |
51 | 49, 50 | sylib 122 |
. . 3
     |
52 | | nnex 8925 |
. . . 4
 |
53 | | fex 5746 |
. . . 4
      
  |
54 | 3, 52, 53 | sylancl 413 |
. . 3
   |
55 | 4 | imcld 10948 |
. . . . . . 7
 

          |
56 | | climcvg1nlem.h |
. . . . . . 7
           |
57 | 55, 56 | fmptd 5671 |
. . . . . 6
       |
58 | 13 | imcld 10948 |
. . . . . . . . . . . . . . 15
        
          |
59 | 15 | fveq2d 5520 |
. . . . . . . . . . . . . . . 16
                   |
60 | 59, 56 | fvmptg 5593 |
. . . . . . . . . . . . . . 15
                         |
61 | 11, 58, 60 | syl2anc 411 |
. . . . . . . . . . . . . 14
        
              |
62 | 20 | imcld 10948 |
. . . . . . . . . . . . . . 15
        
          |
63 | 22 | fveq2d 5520 |
. . . . . . . . . . . . . . . 16
                   |
64 | 63, 56 | fvmptg 5593 |
. . . . . . . . . . . . . . 15
                         |
65 | 19, 62, 64 | syl2anc 411 |
. . . . . . . . . . . . . 14
        
              |
66 | 61, 65 | oveq12d 5893 |
. . . . . . . . . . . . 13
        
                              |
67 | 13, 20 | imsubd 10971 |
. . . . . . . . . . . . 13
        
                                  |
68 | 66, 67 | eqtr4d 2213 |
. . . . . . . . . . . 12
        
                          |
69 | 68 | fveq2d 5520 |
. . . . . . . . . . 11
        
                                  |
70 | | absimle 11093 |
. . . . . . . . . . . 12
                                             |
71 | 30, 70 | syl 14 |
. . . . . . . . . . 11
        
                                  |
72 | 69, 71 | eqbrtrd 4026 |
. . . . . . . . . 10
        
                              |
73 | 61, 58 | eqeltrd 2254 |
. . . . . . . . . . . . . 14
        
      |
74 | 65, 62 | eqeltrd 2254 |
. . . . . . . . . . . . . 14
        
      |
75 | 73, 74 | resubcld 8338 |
. . . . . . . . . . . . 13
        
            |
76 | 75 | recnd 7986 |
. . . . . . . . . . . 12
        
            |
77 | 76 | abscld 11190 |
. . . . . . . . . . 11
        
                |
78 | | lelttr 8046 |
. . . . . . . . . . 11
                                                
                                                  |
79 | 77, 38, 42, 78 | syl3anc 1238 |
. . . . . . . . . 10
        
               
                                                  |
80 | 72, 79 | mpand 429 |
. . . . . . . . 9
        
                                    |
81 | 80 | ralimdva 2544 |
. . . . . . . 8
 

 
                     
                        |
82 | 81 | ralimdva 2544 |
. . . . . . 7
                         
                         |
83 | 9, 82 | mpd 13 |
. . . . . 6
                          |
84 | 57, 8, 83 | climrecvg1n 11356 |
. . . . 5
  |
85 | | climdm 11303 |
. . . . 5

    |
86 | 84, 85 | sylib 122 |
. . . 4
     |
87 | | ax-icn 7906 |
. . . . 5
 |
88 | 87 | a1i 9 |
. . . 4
   |
89 | | climcvg1nlem.j |
. . . . . 6
 
       |
90 | 52 | mptex 5743 |
. . . . . 6
         |
91 | 89, 90 | eqeltri 2250 |
. . . . 5
 |
92 | 91 | a1i 9 |
. . . 4
   |
93 | | ax-resscn 7903 |
. . . . . . 7
 |
94 | 93 | a1i 9 |
. . . . . 6

  |
95 | 57, 94 | fssd 5379 |
. . . . 5
       |
96 | 95 | ffvelcdmda 5652 |
. . . 4
 

      |
97 | 89 | a1i 9 |
. . . . 5
 

 
        |
98 | | fveq2 5516 |
. . . . . . 7
           |
99 | 98 | oveq2d 5891 |
. . . . . 6
 
             |
100 | 99 | adantl 277 |
. . . . 5
                   |
101 | | simpr 110 |
. . . . 5
 

  |
102 | 87 | a1i 9 |
. . . . . 6
 

  |
103 | 102, 96 | mulcld 7978 |
. . . . 5
 

        |
104 | 97, 100, 101, 103 | fvmptd 5598 |
. . . 4
 

            |
105 | 1, 2, 86, 88, 92, 96, 104 | climmulc2 11339 |
. . 3
       |
106 | 7 | ffvelcdmda 5652 |
. . . 4
 

      |
107 | 106 | recnd 7986 |
. . 3
 

      |
108 | 104, 103 | eqeltrd 2254 |
. . 3
 

      |
109 | 3 | ffvelcdmda 5652 |
. . . . 5
 

      |
110 | 109 | replimd 10950 |
. . . 4
 

                          |
111 | 109 | recld 10947 |
. . . . . 6
 

          |
112 | 101, 111,
17 | syl2anc 411 |
. . . . 5
 

              |
113 | 109 | imcld 10948 |
. . . . . . . 8
 

          |
114 | 101, 113,
60 | syl2anc 411 |
. . . . . . 7
 

              |
115 | 114 | oveq2d 5891 |
. . . . . 6
 

                  |
116 | 104, 115 | eqtrd 2210 |
. . . . 5
 

                |
117 | 112, 116 | oveq12d 5893 |
. . . 4
 

                                |
118 | 110, 117 | eqtr4d 2213 |
. . 3
 

                |
119 | 1, 2, 51, 54, 105, 107, 108, 118 | climadd 11334 |
. 2
           |
120 | | climrel 11288 |
. . 3
 |
121 | 120 | releldmi 4867 |
. 2
        
 |
122 | 119, 121 | syl 14 |
1
  |