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

Theorem limsupgre 13304
Description: If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014.)
Hypotheses
Ref Expression
limsupval.1
limsupgre.z
Assertion
Ref Expression
limsupgre
Distinct variable groups:   ,   ,M   ,

Proof of Theorem limsupgre
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrltso 11376 . . . 4
21supex 7943 . . 3
32a1i 11 . 2
4 limsupval.1 . . 3
54a1i 11 . 2
64limsupgval 13299 . . . 4
76adantl 466 . . 3
8 simpl3 1001 . . . . . . 7
9 limsupgre.z . . . . . . . . . . 11
10 uzssz 11129 . . . . . . . . . . 11
119, 10eqsstri 3533 . . . . . . . . . 10
12 zssre 10896 . . . . . . . . . 10
1311, 12sstri 3512 . . . . . . . . 9
1413a1i 11 . . . . . . . 8
15 simpl2 1000 . . . . . . . . 9
16 ressxr 9658 . . . . . . . . 9
17 fss 5744 . . . . . . . . 9
1815, 16, 17sylancl 662 . . . . . . . 8
19 pnfxr 11350 . . . . . . . . 9
2019a1i 11 . . . . . . . 8
214limsuplt 13302 . . . . . . . 8
2214, 18, 20, 21syl3anc 1228 . . . . . . 7
238, 22mpbid 210 . . . . . 6
24 fzfi 12082 . . . . . . . 8
2515adantr 465 . . . . . . . . . 10
26 elfzuz 11713 . . . . . . . . . . 11
2726, 9syl6eleqr 2556 . . . . . . . . . 10
28 ffvelrn 6029 . . . . . . . . . 10
2925, 27, 28syl2an 477 . . . . . . . . 9
3029ralrimiva 2871 . . . . . . . 8
31 fimaxre3 10517 . . . . . . . 8
3224, 30, 31sylancr 663 . . . . . . 7
33 simpr 461 . . . . . . . . . 10
3433ad2antrr 725 . . . . . . . . 9
354limsupgf 13298 . . . . . . . . . 10
3635ffvelrni 6030 . . . . . . . . 9
3734, 36syl 16 . . . . . . . 8
38 simprl 756 . . . . . . . . . 10
3916, 38sseldi 3501 . . . . . . . . 9
40 simprl 756 . . . . . . . . . . 11
4140adantr 465 . . . . . . . . . 10
4235ffvelrni 6030 . . . . . . . . . 10
4341, 42syl 16 . . . . . . . . 9
4439, 43ifcld 3984 . . . . . . . 8
4519a1i 11 . . . . . . . 8
4640ad2antrr 725 . . . . . . . . . . . 12
4713a1i 11 . . . . . . . . . . . . 13
4847sselda 3503 . . . . . . . . . . . 12
49 xrleid 11385 . . . . . . . . . . . . . . . . 17
5043, 49syl 16 . . . . . . . . . . . . . . . 16
5118ad2antrr 725 . . . . . . . . . . . . . . . . 17
524limsupgle 13300 . . . . . . . . . . . . . . . . 17
5347, 51, 41, 43, 52syl211anc 1234 . . . . . . . . . . . . . . . 16
5450, 53mpbid 210 . . . . . . . . . . . . . . 15
5554r19.21bi 2826 . . . . . . . . . . . . . 14
5655imp 429 . . . . . . . . . . . . 13
5746, 42syl 16 . . . . . . . . . . . . . . . 16
5839adantr 465 . . . . . . . . . . . . . . . 16
59 xrmax1 11405 . . . . . . . . . . . . . . . 16
6057, 58, 59syl2anc 661 . . . . . . . . . . . . . . 15
6151ffvelrnda 6031 . . . . . . . . . . . . . . . 16
6244adantr 465 . . . . . . . . . . . . . . . 16
63 xrletr 11390 . . . . . . . . . . . . . . . 16
6461, 57, 62, 63syl3anc 1228 . . . . . . . . . . . . . . 15
6560, 64mpan2d 674 . . . . . . . . . . . . . 14
6665adantr 465 . . . . . . . . . . . . 13
6756, 66mpd 15 . . . . . . . . . . . 12
68 simpr 461 . . . . . . . . . . . . . . . . . 18
6968, 9syl6eleq 2555 . . . . . . . . . . . . . . . . 17
7041flcld 11935 . . . . . . . . . . . . . . . . . 18
7170adantr 465 . . . . . . . . . . . . . . . . 17
72 elfz5 11709 . . . . . . . . . . . . . . . . 17
7369, 71, 72syl2anc 661 . . . . . . . . . . . . . . . 16
7411, 68sseldi 3501 . . . . . . . . . . . . . . . . 17
75 flge 11942 . . . . . . . . . . . . . . . . 17
7646, 74, 75syl2anc 661 . . . . . . . . . . . . . . . 16
7773, 76bitr4d 256 . . . . . . . . . . . . . . 15
7877biimpar 485 . . . . . . . . . . . . . 14
79 simprr 757 . . . . . . . . . . . . . . 15
8079ad2antrr 725 . . . . . . . . . . . . . 14
81 fveq2 5871 . . . . . . . . . . . . . . . 16
8281breq1d 4462 . . . . . . . . . . . . . . 15
8382rspcv 3206 . . . . . . . . . . . . . 14
8478, 80, 83sylc 60 . . . . . . . . . . . . 13
85 xrmax2 11406 . . . . . . . . . . . . . . . . 17
8643, 39, 85syl2anc 661 . . . . . . . . . . . . . . . 16
8786adantr 465 . . . . . . . . . . . . . . 15
88 xrletr 11390 . . . . . . . . . . . . . . . 16
8961, 58, 62, 88syl3anc 1228 . . . . . . . . . . . . . . 15
9087, 89mpan2d 674 . . . . . . . . . . . . . 14
9190adantr 465 . . . . . . . . . . . . 13
9284, 91mpd 15 . . . . . . . . . . . 12
9346, 48, 67, 92lecasei 9711 . . . . . . . . . . 11
9493a1d 25 . . . . . . . . . 10
9594ralrimiva 2871 . . . . . . . . 9
964limsupgle 13300 . . . . . . . . . 10
9747, 51, 34, 44, 96syl211anc 1234 . . . . . . . . 9
9895, 97mpbird 232 . . . . . . . 8
99 ltpnf 11360 . . . . . . . . . 10
10038, 99syl 16 . . . . . . . . 9
101 simplrr 762 . . . . . . . . 9
102 breq1 4455 . . . . . . . . . 10
103 breq1 4455 . . . . . . . . . 10
104102, 103ifboth 3977 . . . . . . . . 9
105100, 101, 104syl2anc 661 . . . . . . . 8
10637, 44, 45, 98, 105xrlelttrd 11392 . . . . . . 7
10732, 106rexlimddv 2953 . . . . . 6
10823, 107rexlimddv 2953 . . . . 5
1097, 108eqbrtrrd 4474 . . . 4
110 imassrn 5353 . . . . . . . . 9
111 frn 5742 . . . . . . . . . 10
11215, 111syl 16 . . . . . . . . 9
113110, 112syl5ss 3514 . . . . . . . 8
114113, 16syl6ss 3515 . . . . . . 7
115 df-ss 3489 . . . . . . 7
116114, 115sylib 196 . . . . . 6
117116, 113eqsstrd 3537 . . . . 5