Step | Hyp | Ref
| Expression |
1 | | fal 1482 |
. . . 4
⊢ ¬
⊥ |
2 | | rlimno1.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
3 | | rlimno1.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0) |
4 | 2, 3 | reccld 10673 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (1 / 𝐵) ∈ ℂ) |
5 | 4 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (1 / 𝐵) ∈ ℂ) |
6 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑥 ∈ 𝐴 (1 / 𝐵) ∈ ℂ) |
7 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
8 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
9 | | ifcl 4080 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 1 ∈
ℝ) → if(1 ≤ 𝑦, 𝑦, 1) ∈ ℝ) |
10 | 7, 8, 9 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(1 ≤ 𝑦, 𝑦, 1) ∈ ℝ) |
11 | | 1rp 11712 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℝ+) |
13 | | max1 11890 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ 𝑦
∈ ℝ) → 1 ≤ if(1 ≤ 𝑦, 𝑦, 1)) |
14 | 8, 7, 13 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ≤ if(1 ≤
𝑦, 𝑦, 1)) |
15 | 10, 12, 14 | rpgecld 11787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → if(1 ≤ 𝑦, 𝑦, 1) ∈
ℝ+) |
16 | 15 | rpreccld 11758 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∈
ℝ+) |
17 | | rlimno1.2 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⇝𝑟
0) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⇝𝑟
0) |
19 | 6, 16, 18 | rlimi 14092 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)))) |
20 | | dmmptg 5549 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 (1 / 𝐵) ∈ ℂ → dom (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) = 𝐴) |
21 | 5, 20 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) = 𝐴) |
22 | | rlimss 14081 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⇝𝑟 0 → dom
(𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⊆ ℝ) |
23 | 17, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ (1 / 𝐵)) ⊆ ℝ) |
24 | 21, 23 | eqsstr3d 3603 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐴 ⊆ ℝ) |
26 | | rexanre 13934 |
. . . . . . 7
⊢ (𝐴 ⊆ ℝ →
(∃𝑐 ∈ ℝ
∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) ↔ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)))) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) ↔ (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)))) |
28 | | rlimno1.1 |
. . . . . . . . 9
⊢ (𝜑 → sup(𝐴, ℝ*, < ) =
+∞) |
29 | | ressxr 9962 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℝ* |
30 | 24, 29 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
31 | | supxrunb1 12021 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑐 ∈
ℝ ∃𝑥 ∈
𝐴 𝑐 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |
33 | 28, 32 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥) |
34 | 33 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥) |
35 | | r19.29 3054 |
. . . . . . . 8
⊢
((∀𝑐 ∈
ℝ ∃𝑥 ∈
𝐴 𝑐 ≤ 𝑥 ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ∃𝑐 ∈ ℝ (∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)))) |
36 | | r19.29r 3055 |
. . . . . . . . . 10
⊢
((∃𝑥 ∈
𝐴 𝑐 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ∃𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 ∧ (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)))) |
37 | 2 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
38 | 3 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0) |
39 | 37, 38 | absrpcld 14035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (abs‘𝐵) ∈
ℝ+) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘𝐵) ∈
ℝ+) |
41 | 15 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → if(1 ≤ 𝑦, 𝑦, 1) ∈
ℝ+) |
42 | 8 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 1 ∈ ℝ) |
43 | | 0le1 10430 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ≤
1 |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 0 ≤ 1) |
45 | 40 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘𝐵) ∈ ℝ) |
46 | 7 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 𝑦 ∈ ℝ) |
47 | 10 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → if(1 ≤ 𝑦, 𝑦, 1) ∈ ℝ) |
48 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘𝐵) ≤ 𝑦) |
49 | | max2 11892 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ 𝑦
∈ ℝ) → 𝑦
≤ if(1 ≤ 𝑦, 𝑦, 1)) |
50 | 8, 46, 49 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 𝑦 ≤ if(1 ≤ 𝑦, 𝑦, 1)) |
51 | 45, 46, 47, 48, 50 | letrd 10073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘𝐵) ≤ if(1 ≤ 𝑦, 𝑦, 1)) |
52 | 40, 41, 42, 44, 51 | lediv2ad 11770 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (1 / if(1 ≤ 𝑦, 𝑦, 1)) ≤ (1 / (abs‘𝐵))) |
53 | 41 | rprecred 11759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∈ ℝ) |
54 | 40 | rprecred 11759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (1 / (abs‘𝐵)) ∈ ℝ) |
55 | 53, 54 | lenltd 10062 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((1 / if(1 ≤ 𝑦, 𝑦, 1)) ≤ (1 / (abs‘𝐵)) ↔ ¬ (1 / (abs‘𝐵)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)))) |
56 | 52, 55 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ¬ (1 / (abs‘𝐵)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) |
57 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 𝐵 ∈ ℂ) |
58 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 𝐵 ≠ 0) |
59 | 57, 58 | reccld 10673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (1 / 𝐵) ∈ ℂ) |
60 | 59 | subid1d 10260 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((1 / 𝐵) − 0) = (1 / 𝐵)) |
61 | 60 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘((1 / 𝐵) − 0)) = (abs‘(1 / 𝐵))) |
62 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → 1 ∈ ℂ) |
63 | 62, 57, 58 | absdivd 14042 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘(1 / 𝐵)) = ((abs‘1) / (abs‘𝐵))) |
64 | 42, 44 | absidd 14009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘1) = 1) |
65 | 64 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((abs‘1) / (abs‘𝐵)) = (1 / (abs‘𝐵))) |
66 | 61, 63, 65 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → (abs‘((1 / 𝐵) − 0)) = (1 / (abs‘𝐵))) |
67 | 66 | breq1d 4593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ↔ (1 / (abs‘𝐵)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)))) |
68 | 56, 67 | mtbird 314 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ¬ (abs‘((1 / 𝐵) − 0)) < (1 / if(1
≤ 𝑦, 𝑦, 1))) |
69 | 68 | pm2.21d 117 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) ∧ (abs‘𝐵) ≤ 𝑦) → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) → ⊥)) |
70 | 69 | expimpd 627 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (((abs‘𝐵) ≤ 𝑦 ∧ (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) → ⊥)) |
71 | 70 | ancomsd 469 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (((abs‘((1 / 𝐵) − 0)) < (1 / if(1
≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦) → ⊥)) |
72 | 71 | imim2d 55 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) → (𝑐 ≤ 𝑥 → ⊥))) |
73 | 72 | com23 84 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝑐 ≤ 𝑥 → ((𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) → ⊥))) |
74 | 73 | impd 446 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ((𝑐 ≤ 𝑥 ∧ (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥)) |
75 | 74 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 ∧ (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥)) |
76 | 36, 75 | syl5 33 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥)) |
77 | 76 | rexlimdvw 3016 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑐 ∈ ℝ (∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥)) |
78 | 35, 77 | syl5 33 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((∀𝑐 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑐 ≤ 𝑥 ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦))) → ⊥)) |
79 | 34, 78 | mpand 707 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → ((abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1)) ∧ (abs‘𝐵) ≤ 𝑦)) → ⊥)) |
80 | 27, 79 | sylbird 249 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ((∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘((1 / 𝐵) − 0)) < (1 / if(1 ≤ 𝑦, 𝑦, 1))) ∧ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)) → ⊥)) |
81 | 19, 80 | mpand 707 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦) → ⊥)) |
82 | 1, 81 | mtoi 189 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → ¬ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)) |
83 | 82 | nrexdv 2984 |
. 2
⊢ (𝜑 → ¬ ∃𝑦 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)) |
84 | 24, 2 | elo1mpt 14113 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ ∃𝑐 ∈ ℝ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦))) |
85 | | rexcom 3080 |
. . 3
⊢
(∃𝑐 ∈
ℝ ∃𝑦 ∈
ℝ ∀𝑥 ∈
𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦) ↔ ∃𝑦 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦)) |
86 | 84, 85 | syl6bb 275 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1) ↔ ∃𝑦 ∈ ℝ ∃𝑐 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑐 ≤ 𝑥 → (abs‘𝐵) ≤ 𝑦))) |
87 | 83, 86 | mtbird 314 |
1
⊢ (𝜑 → ¬ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1)) |