Metamath Proof Explorer

Theorem rexabslelem

Description: An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rexabslelem.1 
|- F/ x ph
rexabslelem.2 
|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion rexabslelem 
|- ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) )

Proof

Step Hyp Ref Expression
1 rexabslelem.1 
 |-  F/ x ph
2 rexabslelem.2 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
3 simp2 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> y e. RR )
4 nfv 
 |-  F/ x y e. RR
5 nfra1 
 |-  F/ x A. x e. A ( abs ` B ) <_ y
6 1 4 5 nf3an 
 |-  F/ x ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y )
7 2 3ad2antl1 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> B e. RR )
8 2 recnd 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
9 8 3ad2antl1 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> B e. CC )
10 9 abscld 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> ( abs ` B ) e. RR )
11 3 adantr 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> y e. RR )
12 7 leabsd 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> B <_ ( abs ` B ) )
13 rspa 
 |-  ( ( A. x e. A ( abs ` B ) <_ y /\ x e. A ) -> ( abs ` B ) <_ y )
14 13 3ad2antl3 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> ( abs ` B ) <_ y )
15 7 10 11 12 14 letrd 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> B <_ y )
16 15 ex 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> ( x e. A -> B <_ y ) )
17 6 16 ralrimi 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> A. x e. A B <_ y )
18 brralrspcev 
 |-  ( ( y e. RR /\ A. x e. A B <_ y ) -> E. w e. RR A. x e. A B <_ w )
19 3 17 18 syl2anc 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> E. w e. RR A. x e. A B <_ w )
20 3 renegcld 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> -u y e. RR )
21 2 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> B e. RR )
22 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> y e. RR )
23 absle 
 |-  ( ( B e. RR /\ y e. RR ) -> ( ( abs ` B ) <_ y <-> ( -u y <_ B /\ B <_ y ) ) )
24 21 22 23 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. A ) -> ( ( abs ` B ) <_ y <-> ( -u y <_ B /\ B <_ y ) ) )
25 24 3adantl3 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> ( ( abs ` B ) <_ y <-> ( -u y <_ B /\ B <_ y ) ) )
26 14 25 mpbid 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> ( -u y <_ B /\ B <_ y ) )
27 26 simpld 
 |-  ( ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) /\ x e. A ) -> -u y <_ B )
28 27 ex 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> ( x e. A -> -u y <_ B ) )
29 6 28 ralrimi 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> A. x e. A -u y <_ B )
30 breq1 
 |-  ( z = -u y -> ( z <_ B <-> -u y <_ B ) )
31 30 ralbidv 
 |-  ( z = -u y -> ( A. x e. A z <_ B <-> A. x e. A -u y <_ B ) )
32 31 rspcev 
 |-  ( ( -u y e. RR /\ A. x e. A -u y <_ B ) -> E. z e. RR A. x e. A z <_ B )
33 20 29 32 syl2anc 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> E. z e. RR A. x e. A z <_ B )
34 19 33 jca 
 |-  ( ( ph /\ y e. RR /\ A. x e. A ( abs ` B ) <_ y ) -> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) )
35 34 3exp 
 |-  ( ph -> ( y e. RR -> ( A. x e. A ( abs ` B ) <_ y -> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) ) )
36 35 rexlimdv 
 |-  ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y -> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) )
37 renegcl 
 |-  ( z e. RR -> -u z e. RR )
38 37 adantl 
 |-  ( ( w e. RR /\ z e. RR ) -> -u z e. RR )
39 simpl 
 |-  ( ( w e. RR /\ z e. RR ) -> w e. RR )
40 38 39 ifcld 
 |-  ( ( w e. RR /\ z e. RR ) -> if ( w <_ -u z , -u z , w ) e. RR )
41 40 ad5ant24 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) -> if ( w <_ -u z , -u z , w ) e. RR )
42 nfv 
 |-  F/ x w e. RR
43 1 42 nfan 
 |-  F/ x ( ph /\ w e. RR )
44 nfra1 
 |-  F/ x A. x e. A B <_ w
45 43 44 nfan 
 |-  F/ x ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w )
46 nfv 
 |-  F/ x z e. RR
47 45 46 nfan 
 |-  F/ x ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR )
48 nfra1 
 |-  F/ x A. x e. A z <_ B
49 47 48 nfan 
 |-  F/ x ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B )
50 40 ad5ant23 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> if ( w <_ -u z , -u z , w ) e. RR )
51 50 renegcld 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> -u if ( w <_ -u z , -u z , w ) e. RR )
52 simpllr 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> z e. RR )
53 2 ad5ant15 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> B e. RR )
54 max2 
 |-  ( ( w e. RR /\ -u z e. RR ) -> -u z <_ if ( w <_ -u z , -u z , w ) )
55 39 38 54 syl2anc 
 |-  ( ( w e. RR /\ z e. RR ) -> -u z <_ if ( w <_ -u z , -u z , w ) )
56 38 40 lenegd 
 |-  ( ( w e. RR /\ z e. RR ) -> ( -u z <_ if ( w <_ -u z , -u z , w ) <-> -u if ( w <_ -u z , -u z , w ) <_ -u -u z ) )
57 55 56 mpbid 
 |-  ( ( w e. RR /\ z e. RR ) -> -u if ( w <_ -u z , -u z , w ) <_ -u -u z )
58 recn 
 |-  ( z e. RR -> z e. CC )
59 58 adantl 
 |-  ( ( w e. RR /\ z e. RR ) -> z e. CC )
60 59 negnegd 
 |-  ( ( w e. RR /\ z e. RR ) -> -u -u z = z )
61 57 60 breqtrd 
 |-  ( ( w e. RR /\ z e. RR ) -> -u if ( w <_ -u z , -u z , w ) <_ z )
62 61 ad5ant23 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> -u if ( w <_ -u z , -u z , w ) <_ z )
63 rspa 
 |-  ( ( A. x e. A z <_ B /\ x e. A ) -> z <_ B )
64 63 adantll 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> z <_ B )
65 51 52 53 62 64 letrd 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> -u if ( w <_ -u z , -u z , w ) <_ B )
66 65 adantl3r 
 |-  ( ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> -u if ( w <_ -u z , -u z , w ) <_ B )
67 2 ad5ant15 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ x e. A ) -> B e. RR )
68 simp-4r 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ x e. A ) -> w e. RR )
69 40 ad5ant24 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ x e. A ) -> if ( w <_ -u z , -u z , w ) e. RR )
70 rspa 
 |-  ( ( A. x e. A B <_ w /\ x e. A ) -> B <_ w )
71 70 ad4ant24 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ x e. A ) -> B <_ w )
72 max1 
 |-  ( ( w e. RR /\ -u z e. RR ) -> w <_ if ( w <_ -u z , -u z , w ) )
73 39 38 72 syl2anc 
 |-  ( ( w e. RR /\ z e. RR ) -> w <_ if ( w <_ -u z , -u z , w ) )
74 73 ad5ant24 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ x e. A ) -> w <_ if ( w <_ -u z , -u z , w ) )
75 67 68 69 71 74 letrd 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ x e. A ) -> B <_ if ( w <_ -u z , -u z , w ) )
76 75 adantlr 
 |-  ( ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> B <_ if ( w <_ -u z , -u z , w ) )
77 66 76 jca 
 |-  ( ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> ( -u if ( w <_ -u z , -u z , w ) <_ B /\ B <_ if ( w <_ -u z , -u z , w ) ) )
78 2 adantlr 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A ) -> B e. RR )
79 78 3adant2 
 |-  ( ( ( ph /\ w e. RR ) /\ z e. RR /\ x e. A ) -> B e. RR )
80 40 adantll 
 |-  ( ( ( ph /\ w e. RR ) /\ z e. RR ) -> if ( w <_ -u z , -u z , w ) e. RR )
81 80 3adant3 
 |-  ( ( ( ph /\ w e. RR ) /\ z e. RR /\ x e. A ) -> if ( w <_ -u z , -u z , w ) e. RR )
82 79 81 absled 
 |-  ( ( ( ph /\ w e. RR ) /\ z e. RR /\ x e. A ) -> ( ( abs ` B ) <_ if ( w <_ -u z , -u z , w ) <-> ( -u if ( w <_ -u z , -u z , w ) <_ B /\ B <_ if ( w <_ -u z , -u z , w ) ) ) )
83 82 ad5ant135 
 |-  ( ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> ( ( abs ` B ) <_ if ( w <_ -u z , -u z , w ) <-> ( -u if ( w <_ -u z , -u z , w ) <_ B /\ B <_ if ( w <_ -u z , -u z , w ) ) ) )
84 77 83 mpbird 
 |-  ( ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) /\ x e. A ) -> ( abs ` B ) <_ if ( w <_ -u z , -u z , w ) )
85 84 ex 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) -> ( x e. A -> ( abs ` B ) <_ if ( w <_ -u z , -u z , w ) ) )
86 49 85 ralrimi 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) -> A. x e. A ( abs ` B ) <_ if ( w <_ -u z , -u z , w ) )
87 brralrspcev 
 |-  ( ( if ( w <_ -u z , -u z , w ) e. RR /\ A. x e. A ( abs ` B ) <_ if ( w <_ -u z , -u z , w ) ) -> E. y e. RR A. x e. A ( abs ` B ) <_ y )
88 41 86 87 syl2anc 
 |-  ( ( ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) /\ z e. RR ) /\ A. x e. A z <_ B ) -> E. y e. RR A. x e. A ( abs ` B ) <_ y )
89 88 exp31 
 |-  ( ( ( ph /\ w e. RR ) /\ A. x e. A B <_ w ) -> ( z e. RR -> ( A. x e. A z <_ B -> E. y e. RR A. x e. A ( abs ` B ) <_ y ) ) )
90 89 exp31 
 |-  ( ph -> ( w e. RR -> ( A. x e. A B <_ w -> ( z e. RR -> ( A. x e. A z <_ B -> E. y e. RR A. x e. A ( abs ` B ) <_ y ) ) ) ) )
91 90 rexlimdv 
 |-  ( ph -> ( E. w e. RR A. x e. A B <_ w -> ( z e. RR -> ( A. x e. A z <_ B -> E. y e. RR A. x e. A ( abs ` B ) <_ y ) ) ) )
92 91 imp 
 |-  ( ( ph /\ E. w e. RR A. x e. A B <_ w ) -> ( z e. RR -> ( A. x e. A z <_ B -> E. y e. RR A. x e. A ( abs ` B ) <_ y ) ) )
93 92 rexlimdv 
 |-  ( ( ph /\ E. w e. RR A. x e. A B <_ w ) -> ( E. z e. RR A. x e. A z <_ B -> E. y e. RR A. x e. A ( abs ` B ) <_ y ) )
94 93 imp 
 |-  ( ( ( ph /\ E. w e. RR A. x e. A B <_ w ) /\ E. z e. RR A. x e. A z <_ B ) -> E. y e. RR A. x e. A ( abs ` B ) <_ y )
95 94 anasss 
 |-  ( ( ph /\ ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) -> E. y e. RR A. x e. A ( abs ` B ) <_ y )
96 95 ex 
 |-  ( ph -> ( ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) -> E. y e. RR A. x e. A ( abs ` B ) <_ y ) )
97 36 96 impbid 
 |-  ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) )