Step |
Hyp |
Ref |
Expression |
1 |
|
cnex |
⊢ ℂ ∈ V |
2 |
|
reex |
⊢ ℝ ∈ V |
3 |
|
elpm2r |
⊢ ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
4 |
1 2 3
|
mpanl12 |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
5 |
|
elo1 |
⊢ ( 𝐹 ∈ 𝑂(1) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) |
6 |
5
|
baib |
⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) |
7 |
4 6
|
syl |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) |
8 |
|
elin |
⊢ ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ) |
9 |
|
fdm |
⊢ ( 𝐹 : 𝐴 ⟶ ℂ → dom 𝐹 = 𝐴 ) |
10 |
9
|
ad3antrrr |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → dom 𝐹 = 𝐴 ) |
11 |
10
|
eleq2d |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴 ) ) |
12 |
11
|
anbi1d |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ) ) |
13 |
|
simpllr |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → 𝐴 ⊆ ℝ ) |
14 |
13
|
sselda |
⊢ ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ ) |
15 |
|
simpllr |
⊢ ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ ℝ ) |
16 |
|
elicopnf |
⊢ ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) ) ) |
17 |
15 16
|
syl |
⊢ ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) ) ) |
18 |
14 17
|
mpbirand |
⊢ ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ 𝑥 ≤ 𝑦 ) ) |
19 |
18
|
pm5.32da |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ) |
20 |
12 19
|
bitrd |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ dom 𝐹 ∧ 𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ) |
21 |
8 20
|
syl5bb |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ) |
22 |
21
|
imbi1d |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) |
23 |
|
impexp |
⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) |
24 |
22 23
|
bitrdi |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) ) |
25 |
24
|
ralbidv2 |
⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) |
26 |
25
|
rexbidva |
⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ↔ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) |
27 |
26
|
rexbidva |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) |
28 |
7 27
|
bitrd |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑚 ) ) ) |