Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cvg1nlemres Unicode version

Theorem cvg1nlemres 9584
 Description: Lemma for cvg1n 9585. The original sequence has a limit (turns out it is the same as the limit of the modified sequence ). (Contributed by Jim Kingdon, 1-Aug-2021.)
Hypotheses
Ref Expression
cvg1n.f
cvg1n.c
cvg1n.cau
cvg1nlem.g
cvg1nlem.z
cvg1nlem.start
Assertion
Ref Expression
cvg1nlemres
Distinct variable groups:   ,,   ,,   ,,,   ,,,   ,   ,,,   ,,,   ,   ,,,,   ,,   ,,
Allowed substitution hints:   (,,)   (,,)   ()   (,)

Proof of Theorem cvg1nlemres
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef 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
71, 2, 3, 4, 5, 6cvg1nlemf 9582 . . 3
81, 2, 3, 4, 5, 6cvg1nlemcau 9583 . . 3
97, 8caucvgre 9580 . 2
10 fveq2 5178 . . . . . . . . . . 11
1110raleqdv 2511 . . . . . . . . . 10
1211cbvrexv 2534 . . . . . . . . 9
1312ralbii 2330 . . . . . . . 8
1413anbi2i 430 . . . . . . 7
1514anbi1i 431 . . . . . 6
16 simpr 103 . . . . . . . . . 10
1716rphalfcld 8635 . . . . . . . . 9
18 simplr 482 . . . . . . . . 9
19 oveq2 5520 . . . . . . . . . . . . 13
2019breq2d 3776 . . . . . . . . . . . 12
21 oveq2 5520 . . . . . . . . . . . . 13
2221breq2d 3776 . . . . . . . . . . . 12
2320, 22anbi12d 442 . . . . . . . . . . 11
2423rexralbidv 2350 . . . . . . . . . 10
2524rspcv 2652 . . . . . . . . 9
2617, 18, 25sylc 56 . . . . . . . 8
2715, 26sylbir 125 . . . . . . 7
282rpred 8622 . . . . . . . . . . . . . 14
2928ad4antr 463 . . . . . . . . . . . . 13
30 2re 7985 . . . . . . . . . . . . . 14
3130a1i 9 . . . . . . . . . . . . 13
3229, 31remulcld 7056 . . . . . . . . . . . 12
33 simplr 482 . . . . . . . . . . . 12
3432, 33rerpdivcld 8654 . . . . . . . . . . 11
355ad4antr 463 . . . . . . . . . . 11
3634, 35nndivred 7963 . . . . . . . . . 10
37 simprl 483 . . . . . . . . . . 11
3837nnred 7927 . . . . . . . . . 10
3936, 38readdcld 7055 . . . . . . . . 9
40 arch 8178 . . . . . . . . 9
4139, 40syl 14 . . . . . . . 8
42 simprl 483 . . . . . . . . . 10
4335adantr 261 . . . . . . . . . 10
4442, 43nnmulcld 7962 . . . . . . . . 9
451ad6antr 467 . . . . . . . . . . . . . . 15
46 simplrl 487 . . . . . . . . . . . . . . . . 17
475ad6antr 467 . . . . . . . . . . . . . . . . 17
4846, 47nnmulcld 7962 . . . . . . . . . . . . . . . 16
49 eluznn 8538 . . . . . . . . . . . . . . . 16
5048, 49sylancom 397 . . . . . . . . . . . . . . 15
5145, 50ffvelrnd 5303 . . . . . . . . . . . . . 14
5245, 48ffvelrnd 5303 . . . . . . . . . . . . . . 15
5333ad2antrr 457 . . . . . . . . . . . . . . . . 17
5453rpred 8622 . . . . . . . . . . . . . . . 16
5554rehalfcld 8171 . . . . . . . . . . . . . . 15
5652, 55readdcld 7055 . . . . . . . . . . . . . 14
57 simpllr 486 . . . . . . . . . . . . . . . . 17
5857ad3antrrr 461 . . . . . . . . . . . . . . . 16
5958, 55readdcld 7055 . . . . . . . . . . . . . . 15
6059, 55readdcld 7055 . . . . . . . . . . . . . 14
6128ad6antr 467 . . . . . . . . . . . . . . . . 17
6261, 48nndivred 7963 . . . . . . . . . . . . . . . 16
6352, 62readdcld 7055 . . . . . . . . . . . . . . 15
64 simpr 103 . . . . . . . . . . . . . . . . 17
653ad6antr 467 . . . . . . . . . . . . . . . . . 18
66 fveq2 5178 . . . . . . . . . . . . . . . . . . . 20
67 fveq2 5178 . . . . . . . . . . . . . . . . . . . . . 22
68 oveq2 5520 . . . . . . . . . . . . . . . . . . . . . . 23
6968oveq2d 5528 . . . . . . . . . . . . . . . . . . . . . 22
7067, 69breq12d 3777 . . . . . . . . . . . . . . . . . . . . 21
7167, 68oveq12d 5530 . . . . . . . . . . . . . . . . . . . . . 22
7271breq2d 3776 . . . . . . . . . . . . . . . . . . . . 21
7370, 72anbi12d 442 . . . . . . . . . . . . . . . . . . . 20
7466, 73raleqbidv 2517 . . . . . . . . . . . . . . . . . . 19
7574rspcv 2652 . . . . . . . . . . . . . . . . . 18
7648, 65, 75sylc 56 . . . . . . . . . . . . . . . . 17
77 fveq2 5178 . . . . . . . . . . . . . . . . . . . . 21
7877oveq1d 5527 . . . . . . . . . . . . . . . . . . . 20
7978breq2d 3776 . . . . . . . . . . . . . . . . . . 19
8077breq1d 3774 . . . . . . . . . . . . . . . . . . 19
8179, 80anbi12d 442 . . . . . . . . . . . . . . . . . 18
8281rspcv 2652 . . . . . . . . . . . . . . . . 17
8364, 76, 82sylc 56 . . . . . . . . . . . . . . . 16
8483simprd 107 . . . . . . . . . . . . . . 15
85 simpr 103 . . . . . . . . . . . . . . . . . . . 20
8685ad3antrrr 461 . . . . . . . . . . . . . . . . . . 19
8786rpred 8622 . . . . . . . . . . . . . . . . . 18
8887rehalfcld 8171 . . . . . . . . . . . . . . . . 17
892ad6antr 467 . . . . . . . . . . . . . . . . . 18
9037ad2antrr 457 . . . . . . . . . . . . . . . . . 18
91 simplrr 488 . . . . . . . . . . . . . . . . . 18
9289, 86, 47, 46, 90, 91cvg1nlemcxze 9581 . . . . . . . . . . . . . . . . 17
9362, 88, 92ltled 7135 . . . . . . . . . . . . . . . 16
9462, 55, 52, 93leadd2dd 7551 . . . . . . . . . . . . . . 15
9551, 63, 56, 84, 94ltletrd 7420 . . . . . . . . . . . . . 14
9690nnred 7927 . . . . . . . . . . . . . . . . . . . 20
9746nnred 7927 . . . . . . . . . . . . . . . . . . . 20
98 2rp 8588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9998a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10089, 99rpmulcld 8639 . . . . . . . . . . . . . . . . . . . . . . . . 25
101100, 86rpdivcld 8640 . . . . . . . . . . . . . . . . . . . . . . . 24
10247nnrpd 8621 . . . . . . . . . . . . . . . . . . . . . . . 24
103101, 102rpdivcld 8640 . . . . . . . . . . . . . . . . . . . . . . 23
104103rpred 8622 . . . . . . . . . . . . . . . . . . . . . 22
105104, 96readdcld 7055 . . . . . . . . . . . . . . . . . . . . 21
10696, 103ltaddrp2d 8657 . . . . . . . . . . . . . . . . . . . . 21
10796, 105, 97, 106, 91lttrd 7140 . . . . . . . . . . . . . . . . . . . 20
10896, 97, 107ltled 7135 . . . . . . . . . . . . . . . . . . 19
10990nnzd 8359 . . . . . . . . . . . . . . . . . . . 20
11046nnzd 8359 . . . . . . . . . . . . . . . . . . . 20
111 eluz 8486 . . . . . . . . . . . . . . . . . . . 20
112109, 110, 111syl2anc 391 . . . . . . . . . . . . . . . . . . 19
113108, 112mpbird 156 . . . . . . . . . . . . . . . . . 18
114 simprr 484 . . . . . . . . . . . . . . . . . . 19
115114ad2antrr 457 . . . . . . . . . . . . . . . . . 18
116 fveq2 5178 . . . . . . . . . . . . . . . . . . . . 21
117116breq1d 3774 . . . . . . . . . . . . . . . . . . . 20
118116oveq1d 5527 . . . . . . . . . . . . . . . . . . . . 21
119118breq2d 3776 . . . . . . . . . . . . . . . . . . . 20
120117, 119anbi12d 442 . . . . . . . . . . . . . . . . . . 19
121120rspcv 2652 . . . . . . . . . . . . . . . . . 18
122113, 115, 121sylc 56 . . . . . . . . . . . . . . . . 17
123 oveq1 5519 . . . . . . . . . . . . . . . . . . . . . 22
124123fveq2d 5182 . . . . . . . . . . . . . . . . . . . . 21
125124, 4fvmptg 5248 . . . . . . . . . . . . . . . . . . . 20
12646, 52, 125syl2anc 391 . . . . . . . . . . . . . . . . . . 19
127126breq1d 3774 . . . . . . . . . . . . . . . . . 18
128126oveq1d 5527 . . . . . . . . . . . . . . . . . . 19
129128breq2d 3776 . . . . . . . . . . . . . . . . . 18
130127, 129anbi12d 442 . . . . . . . . . . . . . . . . 17
131122, 130mpbid 135 . . . . . . . . . . . . . . . 16
132131simpld 105 . . . . . . . . . . . . . . 15
13352, 59, 55, 132ltadd1dd 7547 . . . . . . . . . . . . . 14
13451, 56, 60, 95, 133lttrd 7140 . . . . . . . . . . . . 13
13558recnd 7054 . . . . . . . . . . . . . 14
13655recnd 7054 . . . . . . . . . . . . . 14
137135, 136, 136addassd 7049 . . . . . . . . . . . . 13
138134, 137breqtrd 3788 . . . . . . . . . . . 12
13953rpcnd 8624 . . . . . . . . . . . . . 14
1401392halvesd 8170 . . . . . . . . . . . . 13
141140oveq2d 5528 . . . . . . . . . . . 12
142138, 141breqtrd 3788 . . . . . . . . . . 11
14351, 55readdcld 7055 . . . . . . . . . . . . . . 15
144143, 55readdcld 7055 . . . . . . . . . . . . . 14
145131simprd 107 . . . . . . . . . . . . . 14