Step | Hyp | Ref
| Expression |
1 | | xrge0mulc1cn.k |
. . . . . 6
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
2 | | letopon 20819 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
3 | | iccssxr 12127 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
4 | | resttopon 20775 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
(0[,]+∞) ⊆ ℝ*) → ((ordTop‘ ≤ )
↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞))) |
5 | 2, 3, 4 | mp2an 704 |
. . . . . 6
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞)) |
6 | 1, 5 | eqeltri 2684 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘(0[,]+∞)) |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝐶 = 0 → 𝐽 ∈
(TopOn‘(0[,]+∞))) |
8 | | 0e0iccpnf 12154 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝐶 = 0 → 0 ∈
(0[,]+∞)) |
10 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝐶 = 0) |
11 | 10 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) = (𝑥 ·e 0)) |
12 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈
(0[,]+∞)) |
13 | 3, 12 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈
ℝ*) |
14 | | xmul01 11969 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
→ (𝑥
·e 0) = 0) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 0) =
0) |
16 | 11, 15 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) = 0) |
17 | 16 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝐶 = 0 → (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) = (𝑥 ∈ (0[,]+∞) ↦
0)) |
18 | | xrge0mulc1cn.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) |
19 | | fconstmpt 5085 |
. . . . . 6
⊢
((0[,]+∞) × {0}) = (𝑥 ∈ (0[,]+∞) ↦
0) |
20 | 17, 18, 19 | 3eqtr4g 2669 |
. . . . 5
⊢ (𝐶 = 0 → 𝐹 = ((0[,]+∞) ×
{0})) |
21 | | c0ex 9913 |
. . . . . 6
⊢ 0 ∈
V |
22 | 21 | fconst2 6375 |
. . . . 5
⊢ (𝐹:(0[,]+∞)⟶{0}
↔ 𝐹 = ((0[,]+∞)
× {0})) |
23 | 20, 22 | sylibr 223 |
. . . 4
⊢ (𝐶 = 0 → 𝐹:(0[,]+∞)⟶{0}) |
24 | | cnconst 20898 |
. . . 4
⊢ (((𝐽 ∈
(TopOn‘(0[,]+∞)) ∧ 𝐽 ∈ (TopOn‘(0[,]+∞))) ∧
(0 ∈ (0[,]+∞) ∧ 𝐹:(0[,]+∞)⟶{0})) → 𝐹 ∈ (𝐽 Cn 𝐽)) |
25 | 7, 7, 9, 23, 24 | syl22anc 1319 |
. . 3
⊢ (𝐶 = 0 → 𝐹 ∈ (𝐽 Cn 𝐽)) |
26 | 25 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝐶 = 0) → 𝐹 ∈ (𝐽 Cn 𝐽)) |
27 | | eqid 2610 |
. . . . . . . . 9
⊢
(ordTop‘ ≤ ) = (ordTop‘ ≤ ) |
28 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ·e 𝐶) = (𝑦 ·e 𝐶)) |
29 | 28 | cbvmptv 4678 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
↦ (𝑥
·e 𝐶)) =
(𝑦 ∈
ℝ* ↦ (𝑦 ·e 𝐶)) |
30 | | id 22 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℝ+) |
31 | 27, 29, 30 | xrmulc1cn 29304 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ+
→ (𝑥 ∈
ℝ* ↦ (𝑥 ·e 𝐶)) ∈ ((ordTop‘ ≤ ) Cn
(ordTop‘ ≤ ))) |
32 | | letopuni 20821 |
. . . . . . . . 9
⊢
ℝ* = ∪ (ordTop‘ ≤
) |
33 | 32 | cnrest 20899 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ*
↦ (𝑥
·e 𝐶))
∈ ((ordTop‘ ≤ ) Cn (ordTop‘ ≤ )) ∧ (0[,]+∞)
⊆ ℝ*) → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞))
∈ (((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn
(ordTop‘ ≤ ))) |
34 | 31, 3, 33 | sylancl 693 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ ((𝑥 ∈
ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) ∈
(((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn (ordTop‘
≤ ))) |
35 | | resmpt 5369 |
. . . . . . . . 9
⊢
((0[,]+∞) ⊆ ℝ* → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) =
(𝑥 ∈ (0[,]+∞)
↦ (𝑥
·e 𝐶))) |
36 | 3, 35 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
↦ (𝑥
·e 𝐶))
↾ (0[,]+∞)) = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) |
37 | 36, 18 | eqtr4i 2635 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
↦ (𝑥
·e 𝐶))
↾ (0[,]+∞)) = 𝐹 |
38 | 1 | eqcomi 2619 |
. . . . . . . 8
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) = 𝐽 |
39 | 38 | oveq1i 6559 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn
(ordTop‘ ≤ )) = (𝐽
Cn (ordTop‘ ≤ )) |
40 | 34, 37, 39 | 3eltr3g 2704 |
. . . . . 6
⊢ (𝐶 ∈ ℝ+
→ 𝐹 ∈ (𝐽 Cn (ordTop‘ ≤
))) |
41 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ (ordTop‘ ≤ ) ∈
(TopOn‘ℝ*)) |
42 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ+
∧ 𝑥 ∈
(0[,]+∞)) → 𝑥
∈ (0[,]+∞)) |
43 | | ioorp 12122 |
. . . . . . . . . . . 12
⊢
(0(,)+∞) = ℝ+ |
44 | | ioossicc 12130 |
. . . . . . . . . . . 12
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
45 | 43, 44 | eqsstr3i 3599 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ (0[,]+∞) |
46 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℝ+
∧ 𝑥 ∈
(0[,]+∞)) → 𝐶
∈ ℝ+) |
47 | 45, 46 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ+
∧ 𝑥 ∈
(0[,]+∞)) → 𝐶
∈ (0[,]+∞)) |
48 | | ge0xmulcl 12158 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (0[,]+∞) ∧
𝐶 ∈ (0[,]+∞))
→ (𝑥
·e 𝐶)
∈ (0[,]+∞)) |
49 | 42, 47, 48 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ+
∧ 𝑥 ∈
(0[,]+∞)) → (𝑥
·e 𝐶)
∈ (0[,]+∞)) |
50 | 49, 18 | fmptd 6292 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ+
→ 𝐹:(0[,]+∞)⟶(0[,]+∞)) |
51 | | frn 5966 |
. . . . . . . 8
⊢ (𝐹:(0[,]+∞)⟶(0[,]+∞) →
ran 𝐹 ⊆
(0[,]+∞)) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ ran 𝐹 ⊆
(0[,]+∞)) |
53 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ (0[,]+∞) ⊆ ℝ*) |
54 | | cnrest2 20900 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
ran 𝐹 ⊆
(0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → (𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ )) ↔ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ )
↾t (0[,]+∞))))) |
55 | 41, 52, 53, 54 | syl3anc 1318 |
. . . . . 6
⊢ (𝐶 ∈ ℝ+
→ (𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ ))
↔ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ )
↾t (0[,]+∞))))) |
56 | 40, 55 | mpbid 221 |
. . . . 5
⊢ (𝐶 ∈ ℝ+
→ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ )
↾t (0[,]+∞)))) |
57 | 1 | oveq2i 6560 |
. . . . 5
⊢ (𝐽 Cn 𝐽) = (𝐽 Cn ((ordTop‘ ≤ )
↾t (0[,]+∞))) |
58 | 56, 57 | syl6eleqr 2699 |
. . . 4
⊢ (𝐶 ∈ ℝ+
→ 𝐹 ∈ (𝐽 Cn 𝐽)) |
59 | 58, 43 | eleq2s 2706 |
. . 3
⊢ (𝐶 ∈ (0(,)+∞) →
𝐹 ∈ (𝐽 Cn 𝐽)) |
60 | 59 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ (0(,)+∞)) → 𝐹 ∈ (𝐽 Cn 𝐽)) |
61 | | xrge0mulc1cn.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
62 | | 0xr 9965 |
. . . 4
⊢ 0 ∈
ℝ* |
63 | | pnfxr 9971 |
. . . 4
⊢ +∞
∈ ℝ* |
64 | | 0ltpnf 11832 |
. . . 4
⊢ 0 <
+∞ |
65 | | elicoelioo 28930 |
. . . 4
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
< +∞) → (𝐶
∈ (0[,)+∞) ↔ (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞)))) |
66 | 62, 63, 64, 65 | mp3an 1416 |
. . 3
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 = 0 ∨ 𝐶 ∈
(0(,)+∞))) |
67 | 61, 66 | sylib 207 |
. 2
⊢ (𝜑 → (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞))) |
68 | 26, 60, 67 | mpjaodan 823 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽)) |