Metamath Proof Explorer

Theorem o1lo1

Description: A real function is eventually bounded iff it is eventually lower bounded and eventually upper bounded. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypothesis o1lo1.1 ⊢φ∧x∈A→B∈ℝ
Assertion o1lo1 ⊢φ→x∈A⟼B∈𝑂⁡1↔x∈A⟼B∈≤𝑂⁡1∧x∈A⟼−B∈≤𝑂⁡1

Proof

Step Hyp Ref Expression
1 o1lo1.1 ⊢φ∧x∈A→B∈ℝ
2 o1dm ⊢x∈A⟼B∈𝑂⁡1→dom⁡x∈A⟼B⊆ℝ
3 2 a1i ⊢φ→x∈A⟼B∈𝑂⁡1→dom⁡x∈A⟼B⊆ℝ
4 lo1dm ⊢x∈A⟼B∈≤𝑂⁡1→dom⁡x∈A⟼B⊆ℝ
5 4 adantr ⊢x∈A⟼B∈≤𝑂⁡1∧x∈A⟼−B∈≤𝑂⁡1→dom⁡x∈A⟼B⊆ℝ
6 5 a1i ⊢φ→x∈A⟼B∈≤𝑂⁡1∧x∈A⟼−B∈≤𝑂⁡1→dom⁡x∈A⟼B⊆ℝ
7 1 ralrimiva ⊢φ→∀x∈AB∈ℝ
8 dmmptg ⊢∀x∈AB∈ℝ→dom⁡x∈A⟼B=A
9 7 8 syl ⊢φ→dom⁡x∈A⟼B=A
10 9 sseq1d ⊢φ→dom⁡x∈A⟼B⊆ℝ↔A⊆ℝ
11 simpr ⊢φ∧A⊆ℝ∧m∈ℝ→m∈ℝ
12 1 adantlr ⊢φ∧A⊆ℝ∧x∈A→B∈ℝ
13 12 adantlr ⊢φ∧A⊆ℝ∧m∈ℝ∧x∈A→B∈ℝ
14 simplr ⊢φ∧A⊆ℝ∧m∈ℝ∧x∈A→m∈ℝ
15 13 14 absled ⊢φ∧A⊆ℝ∧m∈ℝ∧x∈A→B≤m↔−m≤B∧B≤m
16 ancom ⊢−m≤B∧B≤m↔B≤m∧−m≤B
17 lenegcon1 ⊢m∈ℝ∧B∈ℝ→−m≤B↔−B≤m
18 14 13 17 syl2anc ⊢φ∧A⊆ℝ∧m∈ℝ∧x∈A→−m≤B↔−B≤m
19 18 anbi2d ⊢φ∧A⊆ℝ∧m∈ℝ∧x∈A→B≤m∧−m≤B↔B≤m∧−B≤m
20 16 19 bitrid ⊢φ∧A⊆ℝ∧m∈ℝ∧x∈A→−m≤B∧B≤m↔B≤m∧−B≤m
21 15 20 bitrd ⊢φ∧A⊆ℝ∧m∈ℝ∧x∈A→B≤m↔B≤m∧−B≤m
22 21 imbi2d ⊢φ∧A⊆ℝ∧m∈ℝ∧x∈A→c≤x→B≤m↔c≤x→B≤m∧−B≤m
23 22 ralbidva ⊢φ∧A⊆ℝ∧m∈ℝ→∀x∈Ac≤x→B≤m↔∀x∈Ac≤x→B≤m∧−B≤m
24 23 rexbidv ⊢φ∧A⊆ℝ∧m∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m↔∃c∈ℝ∀x∈Ac≤x→B≤m∧−B≤m
25 24 biimpd ⊢φ∧A⊆ℝ∧m∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m→∃c∈ℝ∀x∈Ac≤x→B≤m∧−B≤m
26 breq2 ⊢n=m→B≤n↔B≤m
27 26 anbi1d ⊢n=m→B≤n∧−B≤p↔B≤m∧−B≤p
28 27 imbi2d ⊢n=m→c≤x→B≤n∧−B≤p↔c≤x→B≤m∧−B≤p
29 28 rexralbidv ⊢n=m→∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p↔∃c∈ℝ∀x∈Ac≤x→B≤m∧−B≤p
30 breq2 ⊢p=m→−B≤p↔−B≤m
31 30 anbi2d ⊢p=m→B≤m∧−B≤p↔B≤m∧−B≤m
32 31 imbi2d ⊢p=m→c≤x→B≤m∧−B≤p↔c≤x→B≤m∧−B≤m
33 32 rexralbidv ⊢p=m→∃c∈ℝ∀x∈Ac≤x→B≤m∧−B≤p↔∃c∈ℝ∀x∈Ac≤x→B≤m∧−B≤m
34 29 33 rspc2ev ⊢m∈ℝ∧m∈ℝ∧∃c∈ℝ∀x∈Ac≤x→B≤m∧−B≤m→∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p
35 34 3anidm12 ⊢m∈ℝ∧∃c∈ℝ∀x∈Ac≤x→B≤m∧−B≤m→∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p
36 11 25 35 syl6an ⊢φ∧A⊆ℝ∧m∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤m→∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p
37 36 rexlimdva ⊢φ∧A⊆ℝ→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m→∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p
38 simplrr ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧n≤p→p∈ℝ
39 simplrl ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧¬n≤p→n∈ℝ
40 38 39 ifclda ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ→ifn≤ppn∈ℝ
41 max2 ⊢n∈ℝ∧p∈ℝ→p≤ifn≤ppn
42 41 ad2antlr ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→p≤ifn≤ppn
43 12 adantlr ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→B∈ℝ
44 43 renegcld ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→−B∈ℝ
45 simplrr ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→p∈ℝ
46 simplrl ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→n∈ℝ
47 45 46 ifcld ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→ifn≤ppn∈ℝ
48 letr ⊢−B∈ℝ∧p∈ℝ∧ifn≤ppn∈ℝ→−B≤p∧p≤ifn≤ppn→−B≤ifn≤ppn
49 44 45 47 48 syl3anc ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→−B≤p∧p≤ifn≤ppn→−B≤ifn≤ppn
50 42 49 mpan2d ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→−B≤p→−B≤ifn≤ppn
51 lenegcon1 ⊢B∈ℝ∧ifn≤ppn∈ℝ→−B≤ifn≤ppn↔−ifn≤ppn≤B
52 43 47 51 syl2anc ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→−B≤ifn≤ppn↔−ifn≤ppn≤B
53 50 52 sylibd ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→−B≤p→−ifn≤ppn≤B
54 max1 ⊢n∈ℝ∧p∈ℝ→n≤ifn≤ppn
55 54 ad2antlr ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→n≤ifn≤ppn
56 letr ⊢B∈ℝ∧n∈ℝ∧ifn≤ppn∈ℝ→B≤n∧n≤ifn≤ppn→B≤ifn≤ppn
57 43 46 47 56 syl3anc ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→B≤n∧n≤ifn≤ppn→B≤ifn≤ppn
58 55 57 mpan2d ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→B≤n→B≤ifn≤ppn
59 53 58 anim12d ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→−B≤p∧B≤n→−ifn≤ppn≤B∧B≤ifn≤ppn
60 59 ancomsd ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→B≤n∧−B≤p→−ifn≤ppn≤B∧B≤ifn≤ppn
61 43 47 absled ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→B≤ifn≤ppn↔−ifn≤ppn≤B∧B≤ifn≤ppn
62 60 61 sylibrd ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→B≤n∧−B≤p→B≤ifn≤ppn
63 62 imim2d ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ∧x∈A→c≤x→B≤n∧−B≤p→c≤x→B≤ifn≤ppn
64 63 ralimdva ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ→∀x∈Ac≤x→B≤n∧−B≤p→∀x∈Ac≤x→B≤ifn≤ppn
65 64 reximdv ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p→∃c∈ℝ∀x∈Ac≤x→B≤ifn≤ppn
66 breq2 ⊢m=ifn≤ppn→B≤m↔B≤ifn≤ppn
67 66 imbi2d ⊢m=ifn≤ppn→c≤x→B≤m↔c≤x→B≤ifn≤ppn
68 67 rexralbidv ⊢m=ifn≤ppn→∃c∈ℝ∀x∈Ac≤x→B≤m↔∃c∈ℝ∀x∈Ac≤x→B≤ifn≤ppn
69 68 rspcev ⊢ifn≤ppn∈ℝ∧∃c∈ℝ∀x∈Ac≤x→B≤ifn≤ppn→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m
70 40 65 69 syl6an ⊢φ∧A⊆ℝ∧n∈ℝ∧p∈ℝ→∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m
71 70 rexlimdvva ⊢φ∧A⊆ℝ→∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m
72 37 71 impbid ⊢φ∧A⊆ℝ→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m↔∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p
73 rexanre ⊢A⊆ℝ→∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p↔∃c∈ℝ∀x∈Ac≤x→B≤n∧∃c∈ℝ∀x∈Ac≤x→−B≤p
74 73 adantl ⊢φ∧A⊆ℝ→∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p↔∃c∈ℝ∀x∈Ac≤x→B≤n∧∃c∈ℝ∀x∈Ac≤x→−B≤p
75 74 2rexbidv ⊢φ∧A⊆ℝ→∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧−B≤p↔∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧∃c∈ℝ∀x∈Ac≤x→−B≤p
76 72 75 bitrd ⊢φ∧A⊆ℝ→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m↔∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧∃c∈ℝ∀x∈Ac≤x→−B≤p
77 reeanv ⊢∃n∈ℝ∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧∃c∈ℝ∀x∈Ac≤x→−B≤p↔∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→−B≤p
78 76 77 bitrdi ⊢φ∧A⊆ℝ→∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m↔∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→−B≤p
79 rexcom ⊢∃c∈ℝ∃m∈ℝ∀x∈Ac≤x→B≤m↔∃m∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤m
80 rexcom ⊢∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→B≤n↔∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n
81 rexcom ⊢∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→−B≤p↔∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→−B≤p
82 80 81 anbi12i ⊢∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→B≤n∧∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→−B≤p↔∃n∈ℝ∃c∈ℝ∀x∈Ac≤x→B≤n∧∃p∈ℝ∃c∈ℝ∀x∈Ac≤x→−B≤p
83 78 79 82 3bitr4g ⊢φ∧A⊆ℝ→∃c∈ℝ∃m∈ℝ∀x∈Ac≤x→B≤m↔∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→B≤n∧∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→−B≤p
84 simpr ⊢φ∧A⊆ℝ→A⊆ℝ
85 12 recnd ⊢φ∧A⊆ℝ∧x∈A→B∈ℂ
86 84 85 elo1mpt ⊢φ∧A⊆ℝ→x∈A⟼B∈𝑂⁡1↔∃c∈ℝ∃m∈ℝ∀x∈Ac≤x→B≤m
87 84 12 ello1mpt ⊢φ∧A⊆ℝ→x∈A⟼B∈≤𝑂⁡1↔∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→B≤n
88 12 renegcld ⊢φ∧A⊆ℝ∧x∈A→−B∈ℝ
89 84 88 ello1mpt ⊢φ∧A⊆ℝ→x∈A⟼−B∈≤𝑂⁡1↔∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→−B≤p
90 87 89 anbi12d ⊢φ∧A⊆ℝ→x∈A⟼B∈≤𝑂⁡1∧x∈A⟼−B∈≤𝑂⁡1↔∃c∈ℝ∃n∈ℝ∀x∈Ac≤x→B≤n∧∃c∈ℝ∃p∈ℝ∀x∈Ac≤x→−B≤p
91 83 86 90 3bitr4d ⊢φ∧A⊆ℝ→x∈A⟼B∈𝑂⁡1↔x∈A⟼B∈≤𝑂⁡1∧x∈A⟼−B∈≤𝑂⁡1
92 91 ex ⊢φ→A⊆ℝ→x∈A⟼B∈𝑂⁡1↔x∈A⟼B∈≤𝑂⁡1∧x∈A⟼−B∈≤𝑂⁡1
93 10 92 sylbid ⊢φ→dom⁡x∈A⟼B⊆ℝ→x∈A⟼B∈𝑂⁡1↔x∈A⟼B∈≤𝑂⁡1∧x∈A⟼−B∈≤𝑂⁡1
94 3 6 93 pm5.21ndd ⊢φ→x∈A⟼B∈𝑂⁡1↔x∈A⟼B∈≤𝑂⁡1∧x∈A⟼−B∈≤𝑂⁡1