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 ⊢Ⅎxφ
rexabslelem.2 ⊢φ∧x∈A→B∈ℝ
Assertion rexabslelem ⊢φ→∃y∈ℝ∀x∈AB≤y↔∃w∈ℝ∀x∈AB≤w∧∃z∈ℝ∀x∈Az≤B

Proof

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