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 9582 |
. . 3
|
8 | 1, 2, 3, 4, 5, 6 | cvg1nlemcau 9583 |
. . 3
|
9 | 7, 8 | caucvgre 9580 |
. 2
|
10 | | fveq2 5178 |
. . . . . . . . . . 11
|
11 | 10 | raleqdv 2511 |
. . . . . . . . . 10
|
12 | 11 | cbvrexv 2534 |
. . . . . . . . 9
|
13 | 12 | ralbii 2330 |
. . . . . . . 8
|
14 | 13 | anbi2i 430 |
. . . . . . 7
|
15 | 14 | anbi1i 431 |
. . . . . 6
|
16 | | simpr 103 |
. . . . . . . . . 10
|
17 | 16 | rphalfcld 8635 |
. . . . . . . . 9
|
18 | | simplr 482 |
. . . . . . . . 9
|
19 | | oveq2 5520 |
. . . . . . . . . . . . 13
|
20 | 19 | breq2d 3776 |
. . . . . . . . . . . 12
|
21 | | oveq2 5520 |
. . . . . . . . . . . . 13
|
22 | 21 | breq2d 3776 |
. . . . . . . . . . . 12
|
23 | 20, 22 | anbi12d 442 |
. . . . . . . . . . 11
|
24 | 23 | rexralbidv 2350 |
. . . . . . . . . 10
|
25 | 24 | rspcv 2652 |
. . . . . . . . 9
|
26 | 17, 18, 25 | sylc 56 |
. . . . . . . 8
|
27 | 15, 26 | sylbir 125 |
. . . . . . 7
|
28 | 2 | rpred 8622 |
. . . . . . . . . . . . . 14
|
29 | 28 | ad4antr 463 |
. . . . . . . . . . . . 13
|
30 | | 2re 7985 |
. . . . . . . . . . . . . 14
|
31 | 30 | a1i 9 |
. . . . . . . . . . . . 13
|
32 | 29, 31 | remulcld 7056 |
. . . . . . . . . . . 12
|
33 | | simplr 482 |
. . . . . . . . . . . 12
|
34 | 32, 33 | rerpdivcld 8654 |
. . . . . . . . . . 11
|
35 | 5 | ad4antr 463 |
. . . . . . . . . . 11
|
36 | 34, 35 | nndivred 7963 |
. . . . . . . . . 10
|
37 | | simprl 483 |
. . . . . . . . . . 11
|
38 | 37 | nnred 7927 |
. . . . . . . . . 10
|
39 | 36, 38 | readdcld 7055 |
. . . . . . . . 9
|
40 | | arch 8178 |
. . . . . . . . 9
|
41 | 39, 40 | syl 14 |
. . . . . . . 8
|
42 | | simprl 483 |
. . . . . . . . . 10
|
43 | 35 | adantr 261 |
. . . . . . . . . 10
|
44 | 42, 43 | nnmulcld 7962 |
. . . . . . . . 9
|
45 | 1 | ad6antr 467 |
. . . . . . . . . . . . . . 15
|
46 | | simplrl 487 |
. . . . . . . . . . . . . . . . 17
|
47 | 5 | ad6antr 467 |
. . . . . . . . . . . . . . . . 17
|
48 | 46, 47 | nnmulcld 7962 |
. . . . . . . . . . . . . . . 16
|
49 | | eluznn 8538 |
. . . . . . . . . . . . . . . 16
|
50 | 48, 49 | sylancom 397 |
. . . . . . . . . . . . . . 15
|
51 | 45, 50 | ffvelrnd 5303 |
. . . . . . . . . . . . . 14
|
52 | 45, 48 | ffvelrnd 5303 |
. . . . . . . . . . . . . . 15
|
53 | 33 | ad2antrr 457 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | rpred 8622 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | rehalfcld 8171 |
. . . . . . . . . . . . . . 15
|
56 | 52, 55 | readdcld 7055 |
. . . . . . . . . . . . . 14
|
57 | | simpllr 486 |
. . . . . . . . . . . . . . . . 17
|
58 | 57 | ad3antrrr 461 |
. . . . . . . . . . . . . . . 16
|
59 | 58, 55 | readdcld 7055 |
. . . . . . . . . . . . . . 15
|
60 | 59, 55 | readdcld 7055 |
. . . . . . . . . . . . . 14
|
61 | 28 | ad6antr 467 |
. . . . . . . . . . . . . . . . 17
|
62 | 61, 48 | nndivred 7963 |
. . . . . . . . . . . . . . . 16
|
63 | 52, 62 | readdcld 7055 |
. . . . . . . . . . . . . . 15
|
64 | | simpr 103 |
. . . . . . . . . . . . . . . . 17
|
65 | 3 | ad6antr 467 |
. . . . . . . . . . . . . . . . . 18
|
66 | | fveq2 5178 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | | fveq2 5178 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | | oveq2 5520 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
69 | 68 | oveq2d 5528 |
. . . . . . . . . . . . . . . . . . . . . 22
|
70 | 67, 69 | breq12d 3777 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 67, 68 | oveq12d 5530 |
. . . . . . . . . . . . . . . . . . . . . 22
|
72 | 71 | breq2d 3776 |
. . . . . . . . . . . . . . . . . . . . 21
|
73 | 70, 72 | anbi12d 442 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 66, 73 | raleqbidv 2517 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 74 | rspcv 2652 |
. . . . . . . . . . . . . . . . . 18
|
76 | 48, 65, 75 | sylc 56 |
. . . . . . . . . . . . . . . . 17
|
77 | | fveq2 5178 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | 77 | oveq1d 5527 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 78 | breq2d 3776 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 77 | breq1d 3774 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 79, 80 | anbi12d 442 |
. . . . . . . . . . . . . . . . . 18
|
82 | 81 | rspcv 2652 |
. . . . . . . . . . . . . . . . 17
|
83 | 64, 76, 82 | sylc 56 |
. . . . . . . . . . . . . . . 16
|
84 | 83 | simprd 107 |
. . . . . . . . . . . . . . 15
|
85 | | simpr 103 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 85 | ad3antrrr 461 |
. . . . . . . . . . . . . . . . . . 19
|
87 | 86 | rpred 8622 |
. . . . . . . . . . . . . . . . . 18
|
88 | 87 | rehalfcld 8171 |
. . . . . . . . . . . . . . . . 17
|
89 | 2 | ad6antr 467 |
. . . . . . . . . . . . . . . . . 18
|
90 | 37 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . 18
|
91 | | simplrr 488 |
. . . . . . . . . . . . . . . . . 18
|
92 | 89, 86, 47, 46, 90, 91 | cvg1nlemcxze 9581 |
. . . . . . . . . . . . . . . . 17
|
93 | 62, 88, 92 | ltled 7135 |
. . . . . . . . . . . . . . . 16
|
94 | 62, 55, 52, 93 | leadd2dd 7551 |
. . . . . . . . . . . . . . 15
|
95 | 51, 63, 56, 84, 94 | ltletrd 7420 |
. . . . . . . . . . . . . 14
|
96 | 90 | nnred 7927 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | 46 | nnred 7927 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | | 2rp 8588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
99 | 98 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
100 | 89, 99 | rpmulcld 8639 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
101 | 100, 86 | rpdivcld 8640 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
102 | 47 | nnrpd 8621 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
103 | 101, 102 | rpdivcld 8640 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
104 | 103 | rpred 8622 |
. . . . . . . . . . . . . . . . . . . . . 22
|
105 | 104, 96 | readdcld 7055 |
. . . . . . . . . . . . . . . . . . . . 21
|
106 | 96, 103 | ltaddrp2d 8657 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | 96, 105, 97, 106, 91 | lttrd 7140 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 96, 97, 107 | ltled 7135 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 90 | nnzd 8359 |
. . . . . . . . . . . . . . . . . . . 20
|
110 | 46 | nnzd 8359 |
. . . . . . . . . . . . . . . . . . . 20
|
111 | | eluz 8486 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | 109, 110,
111 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . 19
|
113 | 108, 112 | mpbird 156 |
. . . . . . . . . . . . . . . . . 18
|
114 | | simprr 484 |
. . . . . . . . . . . . . . . . . . 19
|
115 | 114 | ad2antrr 457 |
. . . . . . . . . . . . . . . . . 18
|
116 | | fveq2 5178 |
. . . . . . . . . . . . . . . . . . . . 21
|
117 | 116 | breq1d 3774 |
. . . . . . . . . . . . . . . . . . . 20
|
118 | 116 | oveq1d 5527 |
. . . . . . . . . . . . . . . . . . . . 21
|
119 | 118 | breq2d 3776 |
. . . . . . . . . . . . . . . . . . . 20
|
120 | 117, 119 | anbi12d 442 |
. . . . . . . . . . . . . . . . . . 19
|
121 | 120 | rspcv 2652 |
. . . . . . . . . . . . . . . . . 18
|
122 | 113, 115,
121 | sylc 56 |
. . . . . . . . . . . . . . . . 17
|
123 | | oveq1 5519 |
. . . . . . . . . . . . . . . . . . . . . 22
|
124 | 123 | fveq2d 5182 |
. . . . . . . . . . . . . . . . . . . . 21
|
125 | 124, 4 | fvmptg 5248 |
. . . . . . . . . . . . . . . . . . . 20
|
126 | 46, 52, 125 | syl2anc 391 |
. . . . . . . . . . . . . . . . . . 19
|
127 | 126 | breq1d 3774 |
. . . . . . . . . . . . . . . . . 18
|
128 | 126 | oveq1d 5527 |
. . . . . . . . . . . . . . . . . . 19
|
129 | 128 | breq2d 3776 |
. . . . . . . . . . . . . . . . . 18
|
130 | 127, 129 | anbi12d 442 |
. . . . . . . . . . . . . . . . 17
|
131 | 122, 130 | mpbid 135 |
. . . . . . . . . . . . . . . 16
|
132 | 131 | simpld 105 |
. . . . . . . . . . . . . . 15
|
133 | 52, 59, 55, 132 | ltadd1dd 7547 |
. . . . . . . . . . . . . 14
|
134 | 51, 56, 60, 95, 133 | lttrd 7140 |
. . . . . . . . . . . . 13
|
135 | 58 | recnd 7054 |
. . . . . . . . . . . . . 14
|
136 | 55 | recnd 7054 |
. . . . . . . . . . . . . 14
|
137 | 135, 136,
136 | addassd 7049 |
. . . . . . . . . . . . 13
|
138 | 134, 137 | breqtrd 3788 |
. . . . . . . . . . . 12
|
139 | 53 | rpcnd 8624 |
. . . . . . . . . . . . . 14
|
140 | 139 | 2halvesd 8170 |
. . . . . . . . . . . . 13
|
141 | 140 | oveq2d 5528 |
. . . . . . . . . . . 12
|
142 | 138, 141 | breqtrd 3788 |
. . . . . . . . . . 11
|
143 | 51, 55 | readdcld 7055 |
. . . . . . . . . . . . . . 15
|
144 | 143, 55 | readdcld 7055 |
. . . . . . . . . . . . . 14
|
145 | 131 | simprd 107 |
. . . . . . . . . . . . . 14
|
146 | 51, 62 | readdcld 7055 |
. . . . . . . . . . . . . . . 16
|
147 | 83 | simpld 105 |
. . . . . . . . . . . . . . . 16
|
148 | 62, 55, 51, 93 | leadd2dd 7551 |
. . . . . . . . . . . . . . . 16
|
149 | 52, 146, 143, 147, 148 | ltletrd 7420 |
. . . . . . . . . . . . . . 15
|
150 | 52, 143, 55, 149 | ltadd1dd 7547 |
. . . . . . . . . . . . . 14
|
151 | 58, 56, 144, 145, 150 | lttrd 7140 |
. . . . . . . . . . . . 13
|
152 | 51 | recnd 7054 |
. . . . . . . . . . . . . 14
|
153 | 152, 136,
136 | addassd 7049 |
. . . . . . . . . . . . 13
|
154 | 151, 153 | breqtrd 3788 |
. . . . . . . . . . . 12
|
155 | 140 | oveq2d 5528 |
. . . . . . . . . . . 12
|
156 | 154, 155 | breqtrd 3788 |
. . . . . . . . . . 11
|
157 | 142, 156 | jca 290 |
. . . . . . . . . 10
|
158 | 157 | ralrimiva 2392 |
. . . . . . . . 9
|
159 | | fveq2 5178 |
. . . . . . . . . . 11
|
160 | 159 | raleqdv 2511 |
. . . . . . . . . 10
|
161 | 160 | rspcev 2656 |
. . . . . . . . 9
|
162 | 44, 158, 161 | syl2anc 391 |
. . . . . . . 8
|
163 | 41, 162 | rexlimddv 2437 |
. . . . . . 7
|
164 | 27, 163 | rexlimddv 2437 |
. . . . . 6
|
165 | 15, 164 | sylbi 114 |
. . . . 5
|
166 | 165 | ralrimiva 2392 |
. . . 4
|
167 | 166 | ex 108 |
. . 3
|
168 | 167 | reximdva 2421 |
. 2
|
169 | 9, 168 | mpd 13 |
1
|