Metamath Proof Explorer

Theorem uzublem

Description: A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses uzublem.1 
|- F/ j ph
uzublem.2 
|- F/_ j X
uzublem.3 
|- ( ph -> M e. ZZ )
uzublem.4 
|- Z = ( ZZ>= ` M )
uzublem.5 
|- ( ph -> Y e. RR )
uzublem.6 
|- W = sup ( ran ( j e. ( M ... K ) |-> B ) , RR , < )
uzublem.7 
|- X = if ( W <_ Y , Y , W )
uzublem.8 
|- ( ph -> K e. Z )
uzublem.9 
|- ( ( ph /\ j e. Z ) -> B e. RR )
uzublem.10 
|- ( ph -> A. j e. ( ZZ>= ` K ) B <_ Y )
Assertion uzublem 
|- ( ph -> E. x e. RR A. j e. Z B <_ x )

Proof

Step Hyp Ref Expression
1 uzublem.1 
 |-  F/ j ph
2 uzublem.2 
 |-  F/_ j X
3 uzublem.3 
 |-  ( ph -> M e. ZZ )
4 uzublem.4 
 |-  Z = ( ZZ>= ` M )
5 uzublem.5 
 |-  ( ph -> Y e. RR )
6 uzublem.6 
 |-  W = sup ( ran ( j e. ( M ... K ) |-> B ) , RR , < )
7 uzublem.7 
 |-  X = if ( W <_ Y , Y , W )
8 uzublem.8 
 |-  ( ph -> K e. Z )
9 uzublem.9 
 |-  ( ( ph /\ j e. Z ) -> B e. RR )
10 uzublem.10 
 |-  ( ph -> A. j e. ( ZZ>= ` K ) B <_ Y )
11 6 a1i 
 |-  ( ph -> W = sup ( ran ( j e. ( M ... K ) |-> B ) , RR , < ) )
12 ltso 
 |-  < Or RR
13 12 a1i 
 |-  ( ph -> < Or RR )
14 fzfid 
 |-  ( ph -> ( M ... K ) e. Fin )
15 4 eluzelz2 
 |-  ( K e. Z -> K e. ZZ )
16 8 15 syl 
 |-  ( ph -> K e. ZZ )
17 3 zred 
 |-  ( ph -> M e. RR )
18 17 leidd 
 |-  ( ph -> M <_ M )
19 8 4 eleqtrdi 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
20 eluzle 
 |-  ( K e. ( ZZ>= ` M ) -> M <_ K )
21 19 20 syl 
 |-  ( ph -> M <_ K )
22 3 16 3 18 21 elfzd 
 |-  ( ph -> M e. ( M ... K ) )
23 22 ne0d 
 |-  ( ph -> ( M ... K ) =/= (/) )
24 fzssuz 
 |-  ( M ... K ) C_ ( ZZ>= ` M )
25 4 eqcomi 
 |-  ( ZZ>= ` M ) = Z
26 24 25 sseqtri 
 |-  ( M ... K ) C_ Z
27 id 
 |-  ( j e. ( M ... K ) -> j e. ( M ... K ) )
28 26 27 sseldi 
 |-  ( j e. ( M ... K ) -> j e. Z )
29 28 9 sylan2 
 |-  ( ( ph /\ j e. ( M ... K ) ) -> B e. RR )
30 1 13 14 23 29 fisupclrnmpt 
 |-  ( ph -> sup ( ran ( j e. ( M ... K ) |-> B ) , RR , < ) e. RR )
31 11 30 eqeltrd 
 |-  ( ph -> W e. RR )
32 5 31 ifcld 
 |-  ( ph -> if ( W <_ Y , Y , W ) e. RR )
33 7 32 eqeltrid 
 |-  ( ph -> X e. RR )
34 9 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> B e. RR )
35 5 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> Y e. RR )
36 33 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> X e. RR )
37 10 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> A. j e. ( ZZ>= ` K ) B <_ Y )
38 eqid 
 |-  ( ZZ>= ` K ) = ( ZZ>= ` K )
39 16 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> K e. ZZ )
40 4 eluzelz2 
 |-  ( j e. Z -> j e. ZZ )
41 40 ad2antlr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> j e. ZZ )
42 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> K <_ j )
43 38 39 41 42 eluzd 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> j e. ( ZZ>= ` K ) )
44 rspa 
 |-  ( ( A. j e. ( ZZ>= ` K ) B <_ Y /\ j e. ( ZZ>= ` K ) ) -> B <_ Y )
45 37 43 44 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> B <_ Y )
46 max2 
 |-  ( ( W e. RR /\ Y e. RR ) -> Y <_ if ( W <_ Y , Y , W ) )
47 31 5 46 syl2anc 
 |-  ( ph -> Y <_ if ( W <_ Y , Y , W ) )
48 47 7 breqtrrdi 
 |-  ( ph -> Y <_ X )
49 48 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> Y <_ X )
50 34 35 36 45 49 letrd 
 |-  ( ( ( ph /\ j e. Z ) /\ K <_ j ) -> B <_ X )
51 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. K <_ j ) -> -. K <_ j )
52 uzssre 
 |-  ( ZZ>= ` M ) C_ RR
53 4 52 eqsstri 
 |-  Z C_ RR
54 53 sseli 
 |-  ( j e. Z -> j e. RR )
55 54 ad2antlr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. K <_ j ) -> j e. RR )
56 53 8 sseldi 
 |-  ( ph -> K e. RR )
57 56 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ -. K <_ j ) -> K e. RR )
58 55 57 ltnled 
 |-  ( ( ( ph /\ j e. Z ) /\ -. K <_ j ) -> ( j < K <-> -. K <_ j ) )
59 51 58 mpbird 
 |-  ( ( ( ph /\ j e. Z ) /\ -. K <_ j ) -> j < K )
60 9 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> B e. RR )
61 6 31 eqeltrrid 
 |-  ( ph -> sup ( ran ( j e. ( M ... K ) |-> B ) , RR , < ) e. RR )
62 6 61 eqeltrid 
 |-  ( ph -> W e. RR )
63 62 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> W e. RR )
64 5 62 ifcld 
 |-  ( ph -> if ( W <_ Y , Y , W ) e. RR )
65 7 64 eqeltrid 
 |-  ( ph -> X e. RR )
66 65 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> X e. RR )
67 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> ph )
68 3 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> M e. ZZ )
69 16 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> K e. ZZ )
70 4 eleq2i 
 |-  ( j e. Z <-> j e. ( ZZ>= ` M ) )
71 70 biimpi 
 |-  ( j e. Z -> j e. ( ZZ>= ` M ) )
72 71 ad2antlr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> j e. ( ZZ>= ` M ) )
73 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> j < K )
74 72 69 73 elfzod 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> j e. ( M ..^ K ) )
75 elfzouz 
 |-  ( j e. ( M ..^ K ) -> j e. ( ZZ>= ` M ) )
76 75 25 eleqtrdi 
 |-  ( j e. ( M ..^ K ) -> j e. Z )
77 74 76 40 3syl 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> j e. ZZ )
78 eluzle 
 |-  ( j e. ( ZZ>= ` M ) -> M <_ j )
79 71 78 syl 
 |-  ( j e. Z -> M <_ j )
80 79 ad2antlr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> M <_ j )
81 74 76 54 3syl 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> j e. RR )
82 56 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> K e. RR )
83 81 82 73 ltled 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> j <_ K )
84 68 69 77 80 83 elfzd 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> j e. ( M ... K ) )
85 1 29 ralrimia 
 |-  ( ph -> A. j e. ( M ... K ) B e. RR )
86 fimaxre3 
 |-  ( ( ( M ... K ) e. Fin /\ A. j e. ( M ... K ) B e. RR ) -> E. y e. RR A. j e. ( M ... K ) B <_ y )
87 14 85 86 syl2anc 
 |-  ( ph -> E. y e. RR A. j e. ( M ... K ) B <_ y )
88 1 29 87 suprubrnmpt 
 |-  ( ( ph /\ j e. ( M ... K ) ) -> B <_ sup ( ran ( j e. ( M ... K ) |-> B ) , RR , < ) )
89 67 84 88 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> B <_ sup ( ran ( j e. ( M ... K ) |-> B ) , RR , < ) )
90 89 6 breqtrrdi 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> B <_ W )
91 max1 
 |-  ( ( W e. RR /\ Y e. RR ) -> W <_ if ( W <_ Y , Y , W ) )
92 31 5 91 syl2anc 
 |-  ( ph -> W <_ if ( W <_ Y , Y , W ) )
93 92 7 breqtrrdi 
 |-  ( ph -> W <_ X )
94 93 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> W <_ X )
95 60 63 66 90 94 letrd 
 |-  ( ( ( ph /\ j e. Z ) /\ j < K ) -> B <_ X )
96 59 95 syldan 
 |-  ( ( ( ph /\ j e. Z ) /\ -. K <_ j ) -> B <_ X )
97 50 96 pm2.61dan 
 |-  ( ( ph /\ j e. Z ) -> B <_ X )
98 97 ex 
 |-  ( ph -> ( j e. Z -> B <_ X ) )
99 1 98 ralrimi 
 |-  ( ph -> A. j e. Z B <_ X )
100 nfv 
 |-  F/ x A. j e. Z B <_ X
101 nfcv 
 |-  F/_ j x
102 101 2 nfeq 
 |-  F/ j x = X
103 breq2 
 |-  ( x = X -> ( B <_ x <-> B <_ X ) )
104 102 103 ralbid 
 |-  ( x = X -> ( A. j e. Z B <_ x <-> A. j e. Z B <_ X ) )
105 100 104 rspce 
 |-  ( ( X e. RR /\ A. j e. Z B <_ X ) -> E. x e. RR A. j e. Z B <_ x )
106 33 99 105 syl2anc 
 |-  ( ph -> E. x e. RR A. j e. Z B <_ x )