Step | Hyp | Ref
| Expression |
1 | | dvne0.z |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 0 ∈ ran
(ℝ D 𝐹)) |
2 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (𝑥 ∈ ran (ℝ D 𝐹) ↔ 0 ∈ ran (ℝ D 𝐹))) |
3 | 2 | notbid 307 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (¬ 𝑥 ∈ ran (ℝ D 𝐹) ↔ ¬ 0 ∈ ran
(ℝ D 𝐹))) |
4 | 1, 3 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 = 0 → ¬ 𝑥 ∈ ran (ℝ D 𝐹))) |
5 | 4 | necon2ad 2797 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ran (ℝ D 𝐹) → 𝑥 ≠ 0)) |
6 | 5 | imp 444 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ran (ℝ D 𝐹)) → 𝑥 ≠ 0) |
7 | | dvne0.f |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
8 | | cncff 22504 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
10 | | dvne0.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
11 | | dvne0.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ ℝ) |
12 | | iccssre 12126 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
13 | 10, 11, 12 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
14 | | dvfre 23520 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(𝐴[,]𝐵)⟶ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ) → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
15 | 9, 13, 14 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ) |
16 | | frn 5966 |
. . . . . . . . . . . . 13
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℝ → ran
(ℝ D 𝐹) ⊆
ℝ) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (ℝ D 𝐹) ⊆
ℝ) |
18 | 17 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ran (ℝ D 𝐹)) → 𝑥 ∈ ℝ) |
19 | | 0re 9919 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
20 | | lttri2 9999 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 0 ∈
ℝ) → (𝑥 ≠ 0
↔ (𝑥 < 0 ∨ 0
< 𝑥))) |
21 | 18, 19, 20 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ran (ℝ D 𝐹)) → (𝑥 ≠ 0 ↔ (𝑥 < 0 ∨ 0 < 𝑥))) |
22 | | 0xr 9965 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* |
23 | | elioomnf 12139 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ* → (𝑥 ∈ (-∞(,)0) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < 0))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (-∞(,)0) ↔
(𝑥 ∈ ℝ ∧
𝑥 < 0)) |
25 | 24 | baib 942 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (-∞(,)0) ↔
𝑥 < 0)) |
26 | | elrp 11710 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
↔ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
27 | 26 | baib 942 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ ℝ+
↔ 0 < 𝑥)) |
28 | 25, 27 | orbi12d 742 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ (-∞(,)0) ∨
𝑥 ∈
ℝ+) ↔ (𝑥 < 0 ∨ 0 < 𝑥))) |
29 | 18, 28 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ran (ℝ D 𝐹)) → ((𝑥 ∈ (-∞(,)0) ∨ 𝑥 ∈ ℝ+)
↔ (𝑥 < 0 ∨ 0
< 𝑥))) |
30 | 21, 29 | bitr4d 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ran (ℝ D 𝐹)) → (𝑥 ≠ 0 ↔ (𝑥 ∈ (-∞(,)0) ∨ 𝑥 ∈
ℝ+))) |
31 | 6, 30 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ran (ℝ D 𝐹)) → (𝑥 ∈ (-∞(,)0) ∨ 𝑥 ∈
ℝ+)) |
32 | | elun 3715 |
. . . . . . . 8
⊢ (𝑥 ∈ ((-∞(,)0) ∪
ℝ+) ↔ (𝑥 ∈ (-∞(,)0) ∨ 𝑥 ∈
ℝ+)) |
33 | 31, 32 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ran (ℝ D 𝐹)) → 𝑥 ∈ ((-∞(,)0) ∪
ℝ+)) |
34 | 33 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ran (ℝ D 𝐹) → 𝑥 ∈ ((-∞(,)0) ∪
ℝ+))) |
35 | 34 | ssrdv 3574 |
. . . . 5
⊢ (𝜑 → ran (ℝ D 𝐹) ⊆ ((-∞(,)0) ∪
ℝ+)) |
36 | | disjssun 3988 |
. . . . 5
⊢ ((ran
(ℝ D 𝐹) ∩
(-∞(,)0)) = ∅ → (ran (ℝ D 𝐹) ⊆ ((-∞(,)0) ∪
ℝ+) ↔ ran (ℝ D 𝐹) ⊆
ℝ+)) |
37 | 35, 36 | syl5ibcom 234 |
. . . 4
⊢ (𝜑 → ((ran (ℝ D 𝐹) ∩ (-∞(,)0)) =
∅ → ran (ℝ D 𝐹) ⊆
ℝ+)) |
38 | 37 | imp 444 |
. . 3
⊢ ((𝜑 ∧ (ran (ℝ D 𝐹) ∩ (-∞(,)0)) =
∅) → ran (ℝ D 𝐹) ⊆
ℝ+) |
39 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ran (ℝ D 𝐹) ⊆ ℝ+)
→ 𝐴 ∈
ℝ) |
40 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ran (ℝ D 𝐹) ⊆ ℝ+)
→ 𝐵 ∈
ℝ) |
41 | 7 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ran (ℝ D 𝐹) ⊆ ℝ+)
→ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
42 | | dvne0.d |
. . . . . . . . . 10
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
43 | 42 | feq2d 5944 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℝ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ)) |
44 | 15, 43 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ) |
45 | | ffn 5958 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ → (ℝ D 𝐹) Fn (𝐴(,)𝐵)) |
46 | 44, 45 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) Fn (𝐴(,)𝐵)) |
47 | 46 | anim1i 590 |
. . . . . 6
⊢ ((𝜑 ∧ ran (ℝ D 𝐹) ⊆ ℝ+)
→ ((ℝ D 𝐹) Fn
(𝐴(,)𝐵) ∧ ran (ℝ D 𝐹) ⊆
ℝ+)) |
48 | | df-f 5808 |
. . . . . 6
⊢ ((ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℝ+ ↔
((ℝ D 𝐹) Fn (𝐴(,)𝐵) ∧ ran (ℝ D 𝐹) ⊆
ℝ+)) |
49 | 47, 48 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ ran (ℝ D 𝐹) ⊆ ℝ+)
→ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℝ+) |
50 | 39, 40, 41, 49 | dvgt0 23571 |
. . . 4
⊢ ((𝜑 ∧ ran (ℝ D 𝐹) ⊆ ℝ+)
→ 𝐹 Isom < , <
((𝐴[,]𝐵), ran 𝐹)) |
51 | 50 | orcd 406 |
. . 3
⊢ ((𝜑 ∧ ran (ℝ D 𝐹) ⊆ ℝ+)
→ (𝐹 Isom < , <
((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))) |
52 | 38, 51 | syldan 486 |
. 2
⊢ ((𝜑 ∧ (ran (ℝ D 𝐹) ∩ (-∞(,)0)) =
∅) → (𝐹 Isom
< , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))) |
53 | | n0 3890 |
. . . 4
⊢ ((ran
(ℝ D 𝐹) ∩
(-∞(,)0)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (ran (ℝ D 𝐹) ∩ (-∞(,)0))) |
54 | | elin 3758 |
. . . . . 6
⊢ (𝑥 ∈ (ran (ℝ D 𝐹) ∩ (-∞(,)0)) ↔
(𝑥 ∈ ran (ℝ D
𝐹) ∧ 𝑥 ∈ (-∞(,)0))) |
55 | | fvelrnb 6153 |
. . . . . . . . 9
⊢ ((ℝ
D 𝐹) Fn (𝐴(,)𝐵) → (𝑥 ∈ ran (ℝ D 𝐹) ↔ ∃𝑦 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑦) = 𝑥)) |
56 | 46, 55 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ran (ℝ D 𝐹) ↔ ∃𝑦 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑦) = 𝑥)) |
57 | 10 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) → 𝐴 ∈
ℝ) |
58 | 11 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) → 𝐵 ∈
ℝ) |
59 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
60 | 46 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) → (ℝ D
𝐹) Fn (𝐴(,)𝐵)) |
61 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) → (ℝ D
𝐹):(𝐴(,)𝐵)⟶ℝ) |
62 | 61 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ ℝ) |
63 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ∈ ran (ℝ D
𝐹)) |
64 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → 𝑦 ∈ (𝐴(,)𝐵)) |
65 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → 𝑧 ∈ (𝐴(,)𝐵)) |
66 | | ioossicc 12130 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
67 | | rescncf 22508 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) → (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ))) |
68 | 66, 7, 67 | mpsyl 66 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
69 | 68 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → (𝐹 ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |
70 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ℝ
⊆ ℂ |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ℝ ⊆
ℂ) |
72 | | fss 5969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐹:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
73 | 9, 70, 72 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
74 | 66, 13 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
75 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
76 | 75 | tgioo2 22414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
77 | 75, 76 | dvres 23481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐴(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴(,)𝐵)))) |
78 | 71, 73, 13, 74, 77 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴(,)𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴(,)𝐵)))) |
79 | | retop 22375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(topGen‘ran (,)) ∈ Top |
80 | | iooretop 22379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
81 | | isopn3i 20696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝐴(,)𝐵) ∈ (topGen‘ran (,))) →
((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵)) |
82 | 79, 80, 81 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵)) = (𝐴(,)𝐵) |
83 | 82 | reseq2i 5314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((ℝ
D 𝐹) ↾
((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) |
84 | | fnresdm 5914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ℝ
D 𝐹) Fn (𝐴(,)𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (ℝ D 𝐹)) |
85 | 46, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (ℝ D 𝐹)) |
86 | 83, 85 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((ℝ D 𝐹) ↾
((int‘(topGen‘ran (,)))‘(𝐴(,)𝐵))) = (ℝ D 𝐹)) |
87 | 78, 86 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴(,)𝐵))) = (ℝ D 𝐹)) |
88 | 87 | dmeqd 5248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → dom (ℝ D (𝐹 ↾ (𝐴(,)𝐵))) = dom (ℝ D 𝐹)) |
89 | 88, 42 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → dom (ℝ D (𝐹 ↾ (𝐴(,)𝐵))) = (𝐴(,)𝐵)) |
90 | 89 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → dom (ℝ D (𝐹 ↾ (𝐴(,)𝐵))) = (𝐴(,)𝐵)) |
91 | 64, 65, 69, 90 | dvivth 23577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → (((ℝ D (𝐹 ↾ (𝐴(,)𝐵)))‘𝑦)[,]((ℝ D (𝐹 ↾ (𝐴(,)𝐵)))‘𝑧)) ⊆ ran (ℝ D (𝐹 ↾ (𝐴(,)𝐵)))) |
92 | 87 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → (ℝ D (𝐹 ↾ (𝐴(,)𝐵))) = (ℝ D 𝐹)) |
93 | 92 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → ((ℝ D (𝐹 ↾ (𝐴(,)𝐵)))‘𝑦) = ((ℝ D 𝐹)‘𝑦)) |
94 | 92 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → ((ℝ D (𝐹 ↾ (𝐴(,)𝐵)))‘𝑧) = ((ℝ D 𝐹)‘𝑧)) |
95 | 93, 94 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → (((ℝ D (𝐹 ↾ (𝐴(,)𝐵)))‘𝑦)[,]((ℝ D (𝐹 ↾ (𝐴(,)𝐵)))‘𝑧)) = (((ℝ D 𝐹)‘𝑦)[,]((ℝ D 𝐹)‘𝑧))) |
96 | 92 | rneqd 5274 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → ran (ℝ D (𝐹 ↾ (𝐴(,)𝐵))) = ran (ℝ D 𝐹)) |
97 | 91, 95, 96 | 3sstr3d 3610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → (((ℝ D 𝐹)‘𝑦)[,]((ℝ D 𝐹)‘𝑧)) ⊆ ran (ℝ D 𝐹)) |
98 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → 0 ∈ ℝ) |
99 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0)) |
100 | | elioomnf 12139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ∈
ℝ* → (((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0) ↔ (((ℝ D
𝐹)‘𝑦) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑦) < 0))) |
101 | 22, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0) ↔ (((ℝ D
𝐹)‘𝑦) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑦) < 0)) |
102 | 99, 101 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → (((ℝ D 𝐹)‘𝑦) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑦) < 0)) |
103 | 102 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → ((ℝ D 𝐹)‘𝑦) < 0) |
104 | 102 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → ((ℝ D 𝐹)‘𝑦) ∈ ℝ) |
105 | | ltle 10005 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((ℝ D 𝐹)‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ)
→ (((ℝ D 𝐹)‘𝑦) < 0 → ((ℝ D 𝐹)‘𝑦) ≤ 0)) |
106 | 104, 19, 105 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → (((ℝ D 𝐹)‘𝑦) < 0 → ((ℝ D 𝐹)‘𝑦) ≤ 0)) |
107 | 103, 106 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → ((ℝ D 𝐹)‘𝑦) ≤ 0) |
108 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → 0 ≤ ((ℝ D 𝐹)‘𝑧)) |
109 | 65, 62 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → ((ℝ D 𝐹)‘𝑧) ∈ ℝ) |
110 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((ℝ D 𝐹)‘𝑦) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑧) ∈ ℝ) → (0 ∈ (((ℝ
D 𝐹)‘𝑦)[,]((ℝ D 𝐹)‘𝑧)) ↔ (0 ∈ ℝ ∧ ((ℝ D
𝐹)‘𝑦) ≤ 0 ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧)))) |
111 | 104, 109,
110 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → (0 ∈ (((ℝ D 𝐹)‘𝑦)[,]((ℝ D 𝐹)‘𝑧)) ↔ (0 ∈ ℝ ∧ ((ℝ D
𝐹)‘𝑦) ≤ 0 ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧)))) |
112 | 98, 107, 108, 111 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → 0 ∈ (((ℝ D 𝐹)‘𝑦)[,]((ℝ D 𝐹)‘𝑧))) |
113 | 97, 112 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ (𝑧 ∈ (𝐴(,)𝐵) ∧ 0 ≤ ((ℝ D 𝐹)‘𝑧))) → 0 ∈ ran (ℝ D 𝐹)) |
114 | 113 | expr 641 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (0 ≤ ((ℝ D 𝐹)‘𝑧) → 0 ∈ ran (ℝ D 𝐹))) |
115 | 63, 114 | mtod 188 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ¬ 0 ≤ ((ℝ D 𝐹)‘𝑧)) |
116 | | ltnle 9996 |
. . . . . . . . . . . . . . . . . 18
⊢
((((ℝ D 𝐹)‘𝑧) ∈ ℝ ∧ 0 ∈ ℝ)
→ (((ℝ D 𝐹)‘𝑧) < 0 ↔ ¬ 0 ≤ ((ℝ D
𝐹)‘𝑧))) |
117 | 62, 19, 116 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑧) < 0 ↔ ¬ 0 ≤ ((ℝ D
𝐹)‘𝑧))) |
118 | 115, 117 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) < 0) |
119 | | elioomnf 12139 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
ℝ* → (((ℝ D 𝐹)‘𝑧) ∈ (-∞(,)0) ↔ (((ℝ D
𝐹)‘𝑧) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑧) < 0))) |
120 | 22, 119 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(((ℝ D 𝐹)‘𝑧) ∈ (-∞(,)0) ↔ (((ℝ D
𝐹)‘𝑧) ∈ ℝ ∧ ((ℝ D 𝐹)‘𝑧) < 0)) |
121 | 62, 118, 120 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ (-∞(,)0)) |
122 | 121 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) →
∀𝑧 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑧) ∈ (-∞(,)0)) |
123 | | ffnfv 6295 |
. . . . . . . . . . . . . 14
⊢ ((ℝ
D 𝐹):(𝐴(,)𝐵)⟶(-∞(,)0) ↔ ((ℝ D
𝐹) Fn (𝐴(,)𝐵) ∧ ∀𝑧 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑧) ∈ (-∞(,)0))) |
124 | 60, 122, 123 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) → (ℝ D
𝐹):(𝐴(,)𝐵)⟶(-∞(,)0)) |
125 | 57, 58, 59, 124 | dvlt0 23572 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) → 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹)) |
126 | 125 | olcd 407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴(,)𝐵) ∧ ((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0))) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))) |
127 | 126 | expr 641 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹)))) |
128 | | eleq1 2676 |
. . . . . . . . . . 11
⊢
(((ℝ D 𝐹)‘𝑦) = 𝑥 → (((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0) ↔ 𝑥 ∈
(-∞(,)0))) |
129 | 128 | imbi1d 330 |
. . . . . . . . . 10
⊢
(((ℝ D 𝐹)‘𝑦) = 𝑥 → ((((ℝ D 𝐹)‘𝑦) ∈ (-∞(,)0) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))) ↔ (𝑥 ∈ (-∞(,)0) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))))) |
130 | 127, 129 | syl5ibcom 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑦) = 𝑥 → (𝑥 ∈ (-∞(,)0) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))))) |
131 | 130 | rexlimdva 3013 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑦 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑦) = 𝑥 → (𝑥 ∈ (-∞(,)0) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))))) |
132 | 56, 131 | sylbid 229 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ran (ℝ D 𝐹) → (𝑥 ∈ (-∞(,)0) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))))) |
133 | 132 | impd 446 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ran (ℝ D 𝐹) ∧ 𝑥 ∈ (-∞(,)0)) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹)))) |
134 | 54, 133 | syl5bi 231 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (ran (ℝ D 𝐹) ∩ (-∞(,)0)) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹)))) |
135 | 134 | exlimdv 1848 |
. . . 4
⊢ (𝜑 → (∃𝑥 𝑥 ∈ (ran (ℝ D 𝐹) ∩ (-∞(,)0)) → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹)))) |
136 | 53, 135 | syl5bi 231 |
. . 3
⊢ (𝜑 → ((ran (ℝ D 𝐹) ∩ (-∞(,)0)) ≠
∅ → (𝐹 Isom <
, < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹)))) |
137 | 136 | imp 444 |
. 2
⊢ ((𝜑 ∧ (ran (ℝ D 𝐹) ∩ (-∞(,)0)) ≠
∅) → (𝐹 Isom
< , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))) |
138 | 52, 137 | pm2.61dane 2869 |
1
⊢ (𝜑 → (𝐹 Isom < , < ((𝐴[,]𝐵), ran 𝐹) ∨ 𝐹 Isom < , ◡ < ((𝐴[,]𝐵), ran 𝐹))) |