MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  caucvgrlem Unicode version

Theorem caucvgrlem 13495
Description: Lemma for caurcvgr 13496. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.)
Hypotheses
Ref Expression
caurcvgr.1
caurcvgr.2
caurcvgr.3
caurcvgr.4
caucvgrlem.4
Assertion
Ref Expression
caucvgrlem
Distinct variable groups:   , , ,   , , ,   , , ,   , , ,

Proof of Theorem caucvgrlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 caurcvgr.2 . . . . . . 7
2 caurcvgr.1 . . . . . . . 8
3 reex 9604 . . . . . . . . 9
43ssex 4596 . . . . . . . 8
52, 4syl 16 . . . . . . 7
63a1i 11 . . . . . . 7
7 fex2 6755 . . . . . . 7
81, 5, 6, 7syl3anc 1228 . . . . . 6
9 limsupcl 13296 . . . . . 6
108, 9syl 16 . . . . 5
1110adantr 465 . . . 4
121adantr 465 . . . . . 6
13 simprl 756 . . . . . 6
1412, 13ffvelrnd 6032 . . . . 5
15 caucvgrlem.4 . . . . . . 7
1615rpred 11285 . . . . . 6
1716adantr 465 . . . . 5
1814, 17readdcld 9644 . . . 4
19 mnfxr 11352 . . . . . 6
2019a1i 11 . . . . 5
2114, 17resubcld 10012 . . . . . 6
2221rexrd 9664 . . . . 5
23 mnflt 11362 . . . . . 6
2421, 23syl 16 . . . . 5
252adantr 465 . . . . . 6
26 ressxr 9658 . . . . . . . 8
27 fss 5744 . . . . . . . 8
281, 26, 27sylancl 662 . . . . . . 7
2928adantr 465 . . . . . 6
30 caurcvgr.3 . . . . . . 7
3130adantr 465 . . . . . 6
3225, 13sseldd 3504 . . . . . . 7
33 simprr 757 . . . . . . . . 9
34 breq2 4456 . . . . . . . . . . 11
35 fveq2 5871 . . . . . . . . . . . . . 14
3635oveq1d 6311 . . . . . . . . . . . . 13
3736fveq2d 5875 . . . . . . . . . . . 12
3837breq1d 4462 . . . . . . . . . . 11
3934, 38imbi12d 320 . . . . . . . . . 10
4039cbvralv 3084 . . . . . . . . 9
4133, 40sylib 196 . . . . . . . 8
4212ffvelrnda 6031 . . . . . . . . . . . . . . . 16
4314adantr 465 . . . . . . . . . . . . . . . 16
4442, 43resubcld 10012 . . . . . . . . . . . . . . 15
4544recnd 9643 . . . . . . . . . . . . . 14
4645abscld 13267 . . . . . . . . . . . . 13
4717adantr 465 . . . . . . . . . . . . 13
48 ltle 9694 . . . . . . . . . . . . 13
4946, 47, 48syl2anc 661 . . . . . . . . . . . 12
5042, 43, 47absdifled 13266 . . . . . . . . . . . 12
5149, 50sylibd 214 . . . . . . . . . . 11
52 simpl 457 . . . . . . . . . . 11
5351, 52syl6 33 . . . . . . . . . 10
5453imim2d 52 . . . . . . . . 9
5554ralimdva 2865 . . . . . . . 8
5641, 55mpd 15 . . . . . . 7
57 breq1 4455 . . . . . . . . . 10
5857imbi1d 317 . . . . . . . . 9
5958ralbidv 2896 . . . . . . . 8
6059rspcev 3210 . . . . . . 7
6132, 56, 60syl2anc 661 . . . . . 6
6225, 29, 22, 31, 61limsupbnd2 13306 . . . . 5
6320, 22, 11, 24, 62xrltletrd 11393 . . . 4
6418rexrd 9664 . . . . 5
6546adantrr 716 . . . . . . . . . . 11
6617adantr 465 . . . . . . . . . . 11
67 simprl 756 . . . . . . . . . . . 12
68 simplrr 762 . . . . . . . . . . . 12
69 simprr 757 . . . . . . . . . . . 12
7039rspcv 3206 . . . . . . . . . . . 12
7167, 68, 69, 70syl3c 61 . . . . . . . . . . 11
7265, 66, 71ltled 9754 . . . . . . . . . 10
7342adantrr 716 . . . . . . . . . . 11
7414adantr 465 . . . . . . . . . . 11
7573, 74, 66absdifled 13266 . . . . . . . . . 10
7672, 75mpbid 210 . . . . . . . . 9
7776simprd 463 . . . . . . . 8
7877expr 615 . . . . . . 7
7978ralrimiva 2871 . . . . . 6
8057imbi1d 317 . . . . . . . 8
8180ralbidv 2896 . . . . . . 7
8281rspcev 3210 . . . . . 6
8332, 79, 82syl2anc 661 . . . . 5
8425, 29, 64, 83limsupbnd1 13305 . . . 4
85 xrre 11399 . . . 4
8611, 18, 63, 84, 85syl22anc 1229 . . 3
8786adantr 465 . . . . . . . . . 10
8873, 87resubcld 10012 . . . . . . . . 9
8988recnd 9643 . . . . . . . 8
9089abscld 13267 . . . . . . 7
91 2re 10630 . . . . . . . 8
92 remulcl 9598 . . . . . . . 8
9391, 66, 92sylancr 663 . . . . . . 7
94 3re 10634 . . . . . . . 8
95 remulcl 9598 . . . . . . . 8
9694, 66, 95sylancr 663 . . . . . . 7
9773recnd 9643 . . . . . . . . 9
9887recnd 9643 . . . . . . . . 9
9997, 98abssubd 13284 . . . . . . . 8
10073, 93resubcld 10012 . . . . . . . . . 10
10121adantr 465 . . . . . . . . . 10
10266recnd 9643 . . . . . . . . . . . . . 14
1031022timesd 10806 . . . . . . . . . . . . 13
104103oveq2d 6312 . . . . . . . . . . . 12
10597, 102, 102subsub4d 9985 . . . . . . . . . . . 12
106104, 105eqtr4d 2501 . . . . . . . . . . 11
10773, 66resubcld 10012 . . . . . . . . . . . 12
10873, 66, 74lesubaddd 10174 . . . . . . . . . . . . 13
10977, 108mpbird 232 . . . . . . . . . . . 12
110107, 74, 66, 109lesub1dd 10193 . . . . . . . . . . 11
111106, 110eqbrtrd 4472 . . . . . . . . . 10
11262adantr 465 . . . . . . . . . 10
113100, 101, 87, 111, 112letrd 9760 . . . . . . . . 9
11418adantr 465 . . . . . . . . . 10
11573, 93readdcld 9644 . . . . . . . . . 10
11684adantr 465 . . . . . . . . . 10
11773, 66readdcld 9644 . . . . . . . . . . . 12
11876, 52syl 16 . . . . . . . . . . . . 13
11974, 66, 73lesubaddd 10174 . . . . . . . . . . . . 13
120118, 119mpbid 210 . . . . . . . . . . . 12
12174, 117, 66, 120leadd1dd 10191 . . . . . . . . . . 11
12297, 102, 102addassd 9639 . . . . . . . . . . . 12
123103oveq2d 6312 . . . . . . . . . . . 12
124122, 123eqtr4d 2501 . . . . . . . . . . 11
125121, 124breqtrd 4476 . . . . . . . . . 10
12687, 114, 115, 116, 125letrd 9760 . . . . . . . . 9
12787, 73, 93absdifled 13266 . . . . . . . . 9
128113, 126, 127mpbir2and 922 . . . . . . . 8
12999, 128eqbrtrd 4472 . . . . . . 7
130 2lt3 10728 . . . . . . . 8
13191a1i 11 . . . . . . . . 9
13294a1i 11 . . . . . . . . 9
13315adantr 465 . . . . . . . . . 10
134133adantr 465 . . . . . . . . 9
135131, 132, 134ltmul1d 11322 . . . . . . . 8
136130, 135mpbii 211 . . . . . . 7
13790, 93, 96, 129, 136lelttrd 9761 . . . . . 6
138137expr 615 . . . . 5
139138ralrimiva 2871 . . . 4
14035oveq1d 6311 . . . . . . . 8
141140fveq2d 5875 . . . . . . 7
142141breq1d 4462 . . . . . 6
14334, 142imbi12d 320 . . . . 5
144143cbvralv 3084 . . . 4
145139, 144sylibr 212 . . 3
14686, 145jca 532 . 2
147 caurcvgr.4 . . 3
148 breq2 4456 . . . . . 6
149148imbi2d 316 . . . . 5
150149rexralbidv 2976 . . . 4