Step | Hyp | Ref
| Expression |
1 | | bndth.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
2 | | bndth.2 |
. . . . 5
⊢ 𝐾 = (topGen‘ran
(,)) |
3 | | bndth.3 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Comp) |
4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
𝐽 ∈
Comp) |
5 | | cmptop 21008 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
𝐽 ∈
Top) |
7 | 1 | toptopon 20548 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
8 | 6, 7 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
𝐽 ∈ (TopOn‘𝑋)) |
9 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
10 | 9 | cnfldtopon 22396 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
12 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → 1
∈ ℂ) |
13 | 8, 11, 12 | cnmptc 21275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ 1) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
14 | | bndth.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
15 | | uniretop 22376 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ =
∪ (topGen‘ran (,)) |
16 | 2 | unieqi 4381 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ 𝐾 =
∪ (topGen‘ran (,)) |
17 | 15, 16 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ =
∪ 𝐾 |
18 | 1, 17 | cnf 20860 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ) |
19 | 14, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
20 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
22 | | fdm 5964 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑋⟶ℝ → dom 𝐹 = 𝑋) |
23 | 19, 22 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝑋) |
24 | | evth.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ≠ ∅) |
25 | 23, 24 | eqnetrd 2849 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐹 ≠ ∅) |
26 | | dm0rn0 5263 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝐹 = ∅ ↔ ran
𝐹 =
∅) |
27 | 26 | necon3bii 2834 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐹 ≠ ∅ ↔ ran
𝐹 ≠
∅) |
28 | 25, 27 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐹 ≠ ∅) |
29 | 1, 2, 3, 14 | bndth 22565 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥) |
30 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑋⟶ℝ → 𝐹 Fn 𝑋) |
31 | 19, 30 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 Fn 𝑋) |
32 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐹‘𝑦) → (𝑧 ≤ 𝑥 ↔ (𝐹‘𝑦) ≤ 𝑥)) |
33 | 32 | ralrn 6270 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
34 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
35 | 34 | rexbidv 3034 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
36 | 29, 35 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥) |
37 | 21, 28, 36 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥)) |
38 | | suprcl 10862 |
. . . . . . . . . . . . . 14
⊢ ((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
40 | 39 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℂ) |
41 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
sup(ran 𝐹, ℝ, < )
∈ ℂ) |
42 | 8, 11, 41 | cnmptc 21275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ sup(ran 𝐹, ℝ, < )) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
43 | 19 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 = (𝑧 ∈ 𝑋 ↦ (𝐹‘𝑧))) |
44 | 9 | cnfldtop 22397 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈ Top |
45 | | cnrest2r 20901 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ∈ Top → (𝐽 Cn
((TopOpen‘ℂfld) ↾t ℝ)) ⊆
(𝐽 Cn
(TopOpen‘ℂfld))) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐽 Cn
((TopOpen‘ℂfld) ↾t ℝ)) ⊆
(𝐽 Cn
(TopOpen‘ℂfld)) |
47 | 9 | tgioo2 22414 |
. . . . . . . . . . . . . . . 16
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
48 | 2, 47 | eqtri 2632 |
. . . . . . . . . . . . . . 15
⊢ 𝐾 =
((TopOpen‘ℂfld) ↾t
ℝ) |
49 | 48 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)) |
50 | 14, 49 | syl6eleq 2698 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
51 | 46, 50 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
52 | 43, 51 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ 𝑋 ↦ (𝐹‘𝑧)) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
53 | 52 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (𝐹‘𝑧)) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
54 | 9 | subcn 22477 |
. . . . . . . . . . 11
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
55 | 54 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
− ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
56 | 8, 42, 53, 55 | cnmpt12f 21279 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
57 | 39 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
58 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
59 | 58 | adantll 746 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
60 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑧) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ≠ sup(ran 𝐹, ℝ, < ))) |
61 | 59, 60 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ≠ sup(ran 𝐹, ℝ, < ))) |
62 | 61 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℝ) |
63 | 57, 62 | resubcld 10337 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) ∈ ℝ) |
64 | 63 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) ∈ ℂ) |
65 | 57 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → sup(ran 𝐹, ℝ, < ) ∈
ℂ) |
66 | 62 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ∈ ℂ) |
67 | 61 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (𝐹‘𝑧) ≠ sup(ran 𝐹, ℝ, < )) |
68 | 67 | necomd 2837 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → sup(ran 𝐹, ℝ, < ) ≠ (𝐹‘𝑧)) |
69 | 65, 66, 68 | subne0d 10280 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) ≠ 0) |
70 | | eldifsn 4260 |
. . . . . . . . . . . . 13
⊢ ((sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑧)) ∈ (ℂ ∖ {0}) ↔
((sup(ran 𝐹, ℝ, <
) − (𝐹‘𝑧)) ∈ ℂ ∧ (sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑧)) ≠ 0)) |
71 | 64, 69, 70 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) ∈ (ℂ ∖
{0})) |
72 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) = (𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) |
73 | 71, 72 | fmptd 6292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))):𝑋⟶(ℂ ∖
{0})) |
74 | | frn 5966 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))):𝑋⟶(ℂ ∖ {0}) → ran
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ⊆ (ℂ ∖
{0})) |
75 | 73, 74 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ran
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ⊆ (ℂ ∖
{0})) |
76 | | difssd 3700 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(ℂ ∖ {0}) ⊆ ℂ) |
77 | | cnrest2 20900 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ⊆ (ℂ ∖ {0}) ∧
(ℂ ∖ {0}) ⊆ ℂ) → ((𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ {0}))))) |
78 | 11, 75, 76, 77 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
((𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ {0}))))) |
79 | 56, 78 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t (ℂ ∖ {0})))) |
80 | | eqid 2610 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t (ℂ
∖ {0})) = ((TopOpen‘ℂfld) ↾t
(ℂ ∖ {0})) |
81 | 9, 80 | divcn 22479 |
. . . . . . . . 9
⊢ / ∈
(((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) Cn (TopOpen‘ℂfld)) |
82 | 81 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → /
∈ (((TopOpen‘ℂfld) ×t
((TopOpen‘ℂfld) ↾t (ℂ ∖
{0}))) Cn (TopOpen‘ℂfld))) |
83 | 8, 13, 79, 82 | cnmpt12f 21279 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn
(TopOpen‘ℂfld))) |
84 | 63, 69 | rereccld 10731 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑧 ∈ 𝑋) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) ∈ ℝ) |
85 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) = (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) |
86 | 84, 85 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))):𝑋⟶ℝ) |
87 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))):𝑋⟶ℝ → ran (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ⊆ ℝ) |
88 | 86, 87 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) → ran
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ⊆ ℝ) |
89 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
90 | 89 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
ℝ ⊆ ℂ) |
91 | | cnrest2 20900 |
. . . . . . . 8
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ⊆ ℝ ∧ ℝ ⊆
ℂ) → ((𝑧 ∈
𝑋 ↦ (1 / (sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
92 | 11, 88, 90, 91 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn (TopOpen‘ℂfld))
↔ (𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ)))) |
93 | 83, 92 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn ((TopOpen‘ℂfld)
↾t ℝ))) |
94 | 93, 49 | syl6eleqr 2699 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
(𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)))) ∈ (𝐽 Cn 𝐾)) |
95 | 1, 2, 4, 94 | bndth 22565 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
∃𝑥 ∈ ℝ
∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥) |
96 | 39 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → sup(ran
𝐹, ℝ, < ) ∈
ℝ) |
97 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈
ℝ) |
98 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
99 | | ifcl 4080 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 1 ∈
ℝ) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ) |
100 | 97, 98, 99 | sylancl 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → if(1
≤ 𝑥, 𝑥, 1) ∈ ℝ) |
101 | | 0red 9920 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 ∈
ℝ) |
102 | 98 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℝ) |
103 | | 0lt1 10429 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
104 | 103 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 <
1) |
105 | | max1 11890 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℝ ∧ 𝑥
∈ ℝ) → 1 ≤ if(1 ≤ 𝑥, 𝑥, 1)) |
106 | 98, 97, 105 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 1 ≤
if(1 ≤ 𝑥, 𝑥, 1)) |
107 | 101, 102,
100, 104, 106 | ltletrd 10076 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 <
if(1 ≤ 𝑥, 𝑥, 1)) |
108 | 107 | gt0ne0d 10471 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → if(1
≤ 𝑥, 𝑥, 1) ≠ 0) |
109 | 100, 108 | rereccld 10731 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (1 /
if(1 ≤ 𝑥, 𝑥, 1)) ∈
ℝ) |
110 | 100, 107 | recgt0d 10837 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 0 <
(1 / if(1 ≤ 𝑥, 𝑥, 1))) |
111 | 109, 110 | elrpd 11745 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (1 /
if(1 ≤ 𝑥, 𝑥, 1)) ∈
ℝ+) |
112 | 96, 111 | ltsubrpd 11780 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran
𝐹, ℝ, < ) −
(1 / if(1 ≤ 𝑥, 𝑥, 1))) < sup(ran 𝐹, ℝ, <
)) |
113 | 96, 109 | resubcld 10337 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran
𝐹, ℝ, < ) −
(1 / if(1 ≤ 𝑥, 𝑥, 1))) ∈
ℝ) |
114 | 113, 96 | ltnled 10063 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) →
((sup(ran 𝐹, ℝ, <
) − (1 / if(1 ≤ 𝑥,
𝑥, 1))) < sup(ran 𝐹, ℝ, < ) ↔ ¬
sup(ran 𝐹, ℝ, < )
≤ (sup(ran 𝐹, ℝ,
< ) − (1 / if(1 ≤ 𝑥, 𝑥, 1))))) |
115 | 112, 114 | mpbid 221 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ¬
sup(ran 𝐹, ℝ, < )
≤ (sup(ran 𝐹, ℝ,
< ) − (1 / if(1 ≤ 𝑥, 𝑥, 1)))) |
116 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 𝑥 ∈ ℝ) |
117 | | max2 11892 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑥
∈ ℝ) → 𝑥
≤ if(1 ≤ 𝑥, 𝑥, 1)) |
118 | 98, 116, 117 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) |
119 | 39 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
120 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
121 | 120 | ad2ant2l 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
122 | | eldifsn 4260 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑦) ≠ sup(ran 𝐹, ℝ, < ))) |
123 | 121, 122 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((𝐹‘𝑦) ∈ ℝ ∧ (𝐹‘𝑦) ≠ sup(ran 𝐹, ℝ, < ))) |
124 | 123 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ∈ ℝ) |
125 | 119, 124 | resubcld 10337 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ∈ ℝ) |
126 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (ran 𝐹 ⊆ ℝ ∧ ran 𝐹 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥)) |
127 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 Fn 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ ran 𝐹) |
128 | 31, 127 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ∈ ran 𝐹) |
129 | | suprub 10863 |
. . . . . . . . . . . . . . . . . 18
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥) ∧ (𝐹‘𝑦) ∈ ran 𝐹) → (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < )) |
130 | 126, 128,
129 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < )) |
131 | 130 | ad2ant2rl 781 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < )) |
132 | 123 | simprd 478 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) ≠ sup(ran 𝐹, ℝ, < )) |
133 | 132 | necomd 2837 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → sup(ran 𝐹, ℝ, < ) ≠ (𝐹‘𝑦)) |
134 | 124, 119 | ltlend 10061 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((𝐹‘𝑦) < sup(ran 𝐹, ℝ, < ) ↔ ((𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < ) ∧ sup(ran 𝐹, ℝ, < ) ≠ (𝐹‘𝑦)))) |
135 | 131, 133,
134 | mpbir2and 959 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (𝐹‘𝑦) < sup(ran 𝐹, ℝ, < )) |
136 | 124, 119 | posdifd 10493 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((𝐹‘𝑦) < sup(ran 𝐹, ℝ, < ) ↔ 0 < (sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑦)))) |
137 | 135, 136 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 0 < (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) |
138 | 137 | gt0ne0d 10471 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ≠ 0) |
139 | 125, 138 | rereccld 10731 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ∈ ℝ) |
140 | 116, 98, 99 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℝ) |
141 | | letr 10010 |
. . . . . . . . . . . 12
⊢ (((1 /
(sup(ran 𝐹, ℝ, < )
− (𝐹‘𝑦))) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ if(1 ≤
𝑥, 𝑥, 1) ∈ ℝ) → (((1 / (sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑦))) ≤ 𝑥 ∧ 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
142 | 139, 116,
140, 141 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ 𝑥 ∧ 𝑥 ≤ if(1 ≤ 𝑥, 𝑥, 1)) → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
143 | 118, 142 | mpan2d 706 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ 𝑥 → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
144 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
145 | 144 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧)) = (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) |
146 | 145 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))) = (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)))) |
147 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (1 /
(sup(ran 𝐹, ℝ, < )
− (𝐹‘𝑦))) ∈ V |
148 | 146, 85, 147 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) = (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)))) |
149 | 148 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑋 → (((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ 𝑥)) |
150 | 149 | ad2antll 761 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ 𝑥)) |
151 | 109 | adantrr 749 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (1 / if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ) |
152 | 107 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 0 < if(1 ≤ 𝑥, 𝑥, 1)) |
153 | 140, 152 | recgt0d 10837 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → 0 < (1 / if(1 ≤ 𝑥, 𝑥, 1))) |
154 | | lerec 10785 |
. . . . . . . . . . . 12
⊢ ((((1 /
if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ ∧ 0
< (1 / if(1 ≤ 𝑥,
𝑥, 1))) ∧ ((sup(ran
𝐹, ℝ, < ) −
(𝐹‘𝑦)) ∈ ℝ ∧ 0 < (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)))) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))))) |
155 | 151, 153,
125, 137, 154 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))))) |
156 | | lesub 10386 |
. . . . . . . . . . . 12
⊢ (((1 /
if(1 ≤ 𝑥, 𝑥, 1)) ∈ ℝ ∧
sup(ran 𝐹, ℝ, < )
∈ ℝ ∧ (𝐹‘𝑦) ∈ ℝ) → ((1 / if(1 ≤
𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ↔ (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
157 | 151, 119,
124, 156 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((1 / if(1 ≤ 𝑥, 𝑥, 1)) ≤ (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦)) ↔ (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
158 | 140 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ∈ ℂ) |
159 | 108 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → if(1 ≤ 𝑥, 𝑥, 1) ≠ 0) |
160 | 158, 159 | recrecd 10677 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))) = if(1 ≤ 𝑥, 𝑥, 1)) |
161 | 160 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ (1 / (1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
162 | 155, 157,
161 | 3bitr3d 297 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → ((𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ↔ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑦))) ≤ if(1 ≤ 𝑥, 𝑥, 1))) |
163 | 143, 150,
162 | 3imtr4d 282 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧
(𝑥 ∈ ℝ ∧
𝑦 ∈ 𝑋)) → (((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 → (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
164 | 163 | anassrs 678 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 → (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
165 | 164 | ralimdva 2945 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 → ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
166 | 37 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥)) |
167 | | suprleub 10866 |
. . . . . . . . 9
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥) ∧ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ∈ ℝ) → (sup(ran 𝐹, ℝ, < ) ≤ (sup(ran
𝐹, ℝ, < ) −
(1 / if(1 ≤ 𝑥, 𝑥, 1))) ↔ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
168 | 166, 113,
167 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran
𝐹, ℝ, < ) ≤
(sup(ran 𝐹, ℝ, < )
− (1 / if(1 ≤ 𝑥,
𝑥, 1))) ↔
∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
169 | 31 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn 𝑋) |
170 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘𝑦) → (𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ↔ (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
171 | 170 | ralrn 6270 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
172 | 169, 171 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) →
(∀𝑧 ∈ ran 𝐹 𝑧 ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))) ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
173 | 168, 172 | bitrd 267 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → (sup(ran
𝐹, ℝ, < ) ≤
(sup(ran 𝐹, ℝ, < )
− (1 / if(1 ≤ 𝑥,
𝑥, 1))) ↔
∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (sup(ran 𝐹, ℝ, < ) − (1 / if(1 ≤
𝑥, 𝑥, 1))))) |
174 | 165, 173 | sylibrd 248 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) →
(∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥 → sup(ran 𝐹, ℝ, < ) ≤ (sup(ran 𝐹, ℝ, < ) − (1 /
if(1 ≤ 𝑥, 𝑥, 1))))) |
175 | 115, 174 | mtod 188 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) ∧ 𝑥 ∈ ℝ) → ¬
∀𝑦 ∈ 𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥) |
176 | 175 | nrexdv 2984 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )})) →
¬ ∃𝑥 ∈
ℝ ∀𝑦 ∈
𝑋 ((𝑧 ∈ 𝑋 ↦ (1 / (sup(ran 𝐹, ℝ, < ) − (𝐹‘𝑧))))‘𝑦) ≤ 𝑥) |
177 | 95, 176 | pm2.65da 598 |
. . 3
⊢ (𝜑 → ¬ 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, <
)})) |
178 | 130 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < )) |
179 | | breq2 4587 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑥) = sup(ran 𝐹, ℝ, < ) → ((𝐹‘𝑦) ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < ))) |
180 | 179 | ralbidv 2969 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) = sup(ran 𝐹, ℝ, < ) → (∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ sup(ran 𝐹, ℝ, < ))) |
181 | 178, 180 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝑥) = sup(ran 𝐹, ℝ, < ) → ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥))) |
182 | 181 | necon3bd 2796 |
. . . . . . 7
⊢ (𝜑 → (¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → (𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
183 | 182 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → (𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
184 | 19 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ ℝ) |
185 | | eldifsn 4260 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
186 | 185 | baib 942 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ ℝ → ((𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
(𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
187 | 184, 186 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
(𝐹‘𝑥) ≠ sup(ran 𝐹, ℝ, < ))) |
188 | 183, 187 | sylibrd 248 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
189 | 188 | ralimdva 2945 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
190 | | ffnfv 6295 |
. . . . . 6
⊢ (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
(𝐹 Fn 𝑋 ∧ ∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
191 | 190 | baib 942 |
. . . . 5
⊢ (𝐹 Fn 𝑋 → (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
192 | 31, 191 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, < )}) ↔
∀𝑥 ∈ 𝑋 (𝐹‘𝑥) ∈ (ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
193 | 189, 192 | sylibrd 248 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) → 𝐹:𝑋⟶(ℝ ∖ {sup(ran 𝐹, ℝ, <
)}))) |
194 | 177, 193 | mtod 188 |
. 2
⊢ (𝜑 → ¬ ∀𝑥 ∈ 𝑋 ¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) |
195 | | dfrex2 2979 |
. 2
⊢
(∃𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥) ↔ ¬ ∀𝑥 ∈ 𝑋 ¬ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) |
196 | 194, 195 | sylibr 223 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) |