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 ∈ A B ≤ y ↔ ∃ w ∈ ℝ ∀ x ∈ A B ≤ w ∧ ∃ z ∈ ℝ ∀ x ∈ A z ≤ B

Proof

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