Step | Hyp | Ref
| Expression |
1 | | rlimcld2.6 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷) |
2 | 1 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐷) |
3 | 2 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐷) |
4 | | rlimcld2.2 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶) |
6 | | rlimcl 14234 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → 𝐶 ∈ ℂ) |
8 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ¬ 𝐶 ∈ 𝐷) |
9 | 7, 8 | eldifd 3585 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → 𝐶 ∈ (ℂ ∖ 𝐷)) |
10 | | rlimcld2.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ 𝐷)) → 𝑅 ∈
ℝ+) |
11 | 10 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ (ℂ ∖ 𝐷)𝑅 ∈
ℝ+) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ∀𝑦 ∈ (ℂ ∖ 𝐷)𝑅 ∈
ℝ+) |
13 | | nfcsb1v 3549 |
. . . . . 6
⊢
Ⅎ𝑦⦋𝐶 / 𝑦⦌𝑅 |
14 | 13 | nfel1 2779 |
. . . . 5
⊢
Ⅎ𝑦⦋𝐶 / 𝑦⦌𝑅 ∈ ℝ+ |
15 | | csbeq1a 3542 |
. . . . . 6
⊢ (𝑦 = 𝐶 → 𝑅 = ⦋𝐶 / 𝑦⦌𝑅) |
16 | 15 | eleq1d 2686 |
. . . . 5
⊢ (𝑦 = 𝐶 → (𝑅 ∈ ℝ+ ↔
⦋𝐶 / 𝑦⦌𝑅 ∈
ℝ+)) |
17 | 14, 16 | rspc 3303 |
. . . 4
⊢ (𝐶 ∈ (ℂ ∖ 𝐷) → (∀𝑦 ∈ (ℂ ∖ 𝐷)𝑅 ∈ ℝ+ →
⦋𝐶 / 𝑦⦌𝑅 ∈
ℝ+)) |
18 | 9, 12, 17 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ⦋𝐶 / 𝑦⦌𝑅 ∈
ℝ+) |
19 | 3, 18, 5 | rlimi 14244 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅)) |
20 | 1 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷) |
21 | 20 | adantlr 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷) |
22 | | rlimcld2.5 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (ℂ ∖ 𝐷)) ∧ 𝑧 ∈ 𝐷) → 𝑅 ≤ (abs‘(𝑧 − 𝑦))) |
23 | 22 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (ℂ ∖ 𝐷)) → ∀𝑧 ∈ 𝐷 𝑅 ≤ (abs‘(𝑧 − 𝑦))) |
24 | 23 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑦 ∈ (ℂ ∖ 𝐷)∀𝑧 ∈ 𝐷 𝑅 ≤ (abs‘(𝑧 − 𝑦))) |
25 | 24 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ∀𝑦 ∈ (ℂ ∖ 𝐷)∀𝑧 ∈ 𝐷 𝑅 ≤ (abs‘(𝑧 − 𝑦))) |
26 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝐷 |
27 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦
≤ |
28 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(abs‘(𝑧 − 𝐶)) |
29 | 13, 27, 28 | nfbr 4699 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶)) |
30 | 26, 29 | nfral 2945 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑧 ∈ 𝐷 ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶)) |
31 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐶 → (𝑧 − 𝑦) = (𝑧 − 𝐶)) |
32 | 31 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐶 → (abs‘(𝑧 − 𝑦)) = (abs‘(𝑧 − 𝐶))) |
33 | 15, 32 | breq12d 4666 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐶 → (𝑅 ≤ (abs‘(𝑧 − 𝑦)) ↔ ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶)))) |
34 | 33 | ralbidv 2986 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐶 → (∀𝑧 ∈ 𝐷 𝑅 ≤ (abs‘(𝑧 − 𝑦)) ↔ ∀𝑧 ∈ 𝐷 ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶)))) |
35 | 30, 34 | rspc 3303 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (ℂ ∖ 𝐷) → (∀𝑦 ∈ (ℂ ∖ 𝐷)∀𝑧 ∈ 𝐷 𝑅 ≤ (abs‘(𝑧 − 𝑦)) → ∀𝑧 ∈ 𝐷 ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶)))) |
36 | 9, 25, 35 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ∀𝑧 ∈ 𝐷 ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶))) |
37 | 36 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ∀𝑧 ∈ 𝐷 ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶))) |
38 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → (𝑧 − 𝐶) = (𝐵 − 𝐶)) |
39 | 38 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → (abs‘(𝑧 − 𝐶)) = (abs‘(𝐵 − 𝐶))) |
40 | 39 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶)) ↔ ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝐵 − 𝐶)))) |
41 | 40 | rspcv 3305 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝐷 → (∀𝑧 ∈ 𝐷 ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝑧 − 𝐶)) → ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝐵 − 𝐶)))) |
42 | 21, 37, 41 | sylc 65 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝐵 − 𝐶))) |
43 | 18 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ⦋𝐶 / 𝑦⦌𝑅 ∈
ℝ+) |
44 | 43 | rpred 11872 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ⦋𝐶 / 𝑦⦌𝑅 ∈ ℝ) |
45 | | rlimcld2.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ⊆ ℂ) |
46 | 45 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐷 ⊆ ℂ) |
47 | 46, 21 | sseldd 3604 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
48 | 7 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
49 | 47, 48 | subcld 10392 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (𝐵 − 𝐶) ∈ ℂ) |
50 | 49 | abscld 14175 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (abs‘(𝐵 − 𝐶)) ∈ ℝ) |
51 | 44, 50 | lenltd 10183 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → (⦋𝐶 / 𝑦⦌𝑅 ≤ (abs‘(𝐵 − 𝐶)) ↔ ¬ (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅)) |
52 | 42, 51 | mpbid 222 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ¬ (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) |
53 | | id 22 |
. . . . . . 7
⊢ ((𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) → (𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅)) |
54 | 53 | imp 445 |
. . . . . 6
⊢ (((𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) ∧ 𝑟 ≤ 𝑥) → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) |
55 | 52, 54 | nsyl 135 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) ∧ 𝑥 ∈ 𝐴) → ¬ ((𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) ∧ 𝑟 ≤ 𝑥)) |
56 | 55 | nrexdv 3001 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) → ¬ ∃𝑥 ∈ 𝐴 ((𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) ∧ 𝑟 ≤ 𝑥)) |
57 | | rlimcld2.1 |
. . . . . . . 8
⊢ (𝜑 → sup(𝐴, ℝ*, < ) =
+∞) |
58 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
59 | 58, 1 | dmmptd 6024 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
60 | | rlimss 14233 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 𝐶 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
61 | 4, 60 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ℝ) |
62 | 59, 61 | eqsstr3d 3640 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
63 | | ressxr 10083 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
64 | 62, 63 | syl6ss 3615 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
65 | | supxrunb1 12149 |
. . . . . . . . 9
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑟 ∈
ℝ ∃𝑥 ∈
𝐴 𝑟 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |
66 | 64, 65 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑟 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑟 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |
67 | 57, 66 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → ∀𝑟 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑟 ≤ 𝑥) |
68 | 67 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ∀𝑟 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑟 ≤ 𝑥) |
69 | 68 | r19.21bi 2932 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) → ∃𝑥 ∈ 𝐴 𝑟 ≤ 𝑥) |
70 | | r19.29 3072 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 (𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) ∧ ∃𝑥 ∈ 𝐴 𝑟 ≤ 𝑥) → ∃𝑥 ∈ 𝐴 ((𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) ∧ 𝑟 ≤ 𝑥)) |
71 | 70 | expcom 451 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑟 ≤ 𝑥 → (∀𝑥 ∈ 𝐴 (𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) → ∃𝑥 ∈ 𝐴 ((𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) ∧ 𝑟 ≤ 𝑥))) |
72 | 69, 71 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) → (∀𝑥 ∈ 𝐴 (𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) → ∃𝑥 ∈ 𝐴 ((𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅) ∧ 𝑟 ≤ 𝑥))) |
73 | 56, 72 | mtod 189 |
. . 3
⊢ (((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) ∧ 𝑟 ∈ ℝ) → ¬ ∀𝑥 ∈ 𝐴 (𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅)) |
74 | 73 | nrexdv 3001 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ 𝐷) → ¬ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝐴 (𝑟 ≤ 𝑥 → (abs‘(𝐵 − 𝐶)) < ⦋𝐶 / 𝑦⦌𝑅)) |
75 | 19, 74 | condan 835 |
1
⊢ (𝜑 → 𝐶 ∈ 𝐷) |