| Step | Hyp | Ref
| Expression |
| 1 | | xrge0mulc1cn.k |
. . . . . 6
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
| 2 | | letopon 23213 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
| 3 | | iccssxr 13470 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
| 4 | | resttopon 23169 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
(0[,]+∞) ⊆ ℝ*) → ((ordTop‘ ≤ )
↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞))) |
| 5 | 2, 3, 4 | mp2an 692 |
. . . . . 6
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞)) |
| 6 | 1, 5 | eqeltri 2837 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘(0[,]+∞)) |
| 7 | 6 | a1i 11 |
. . . 4
⊢ (𝐶 = 0 → 𝐽 ∈
(TopOn‘(0[,]+∞))) |
| 8 | | 0e0iccpnf 13499 |
. . . . 5
⊢ 0 ∈
(0[,]+∞) |
| 9 | 8 | a1i 11 |
. . . 4
⊢ (𝐶 = 0 → 0 ∈
(0[,]+∞)) |
| 10 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝐶 = 0) |
| 11 | 10 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) = (𝑥 ·e 0)) |
| 12 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈
(0[,]+∞)) |
| 13 | 3, 12 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈
ℝ*) |
| 14 | | xmul01 13309 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
→ (𝑥
·e 0) = 0) |
| 15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 0) =
0) |
| 16 | 11, 15 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) = 0) |
| 17 | 16 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝐶 = 0 → (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) = (𝑥 ∈ (0[,]+∞) ↦
0)) |
| 18 | | xrge0mulc1cn.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) |
| 19 | | fconstmpt 5747 |
. . . . . 6
⊢
((0[,]+∞) × {0}) = (𝑥 ∈ (0[,]+∞) ↦
0) |
| 20 | 17, 18, 19 | 3eqtr4g 2802 |
. . . . 5
⊢ (𝐶 = 0 → 𝐹 = ((0[,]+∞) ×
{0})) |
| 21 | | c0ex 11255 |
. . . . . 6
⊢ 0 ∈
V |
| 22 | 21 | fconst2 7225 |
. . . . 5
⊢ (𝐹:(0[,]+∞)⟶{0}
↔ 𝐹 = ((0[,]+∞)
× {0})) |
| 23 | 20, 22 | sylibr 234 |
. . . 4
⊢ (𝐶 = 0 → 𝐹:(0[,]+∞)⟶{0}) |
| 24 | | cnconst 23292 |
. . . 4
⊢ (((𝐽 ∈
(TopOn‘(0[,]+∞)) ∧ 𝐽 ∈ (TopOn‘(0[,]+∞))) ∧
(0 ∈ (0[,]+∞) ∧ 𝐹:(0[,]+∞)⟶{0})) → 𝐹 ∈ (𝐽 Cn 𝐽)) |
| 25 | 7, 7, 9, 23, 24 | syl22anc 839 |
. . 3
⊢ (𝐶 = 0 → 𝐹 ∈ (𝐽 Cn 𝐽)) |
| 26 | 25 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝐶 = 0) → 𝐹 ∈ (𝐽 Cn 𝐽)) |
| 27 | | eqid 2737 |
. . . . . . . . 9
⊢
(ordTop‘ ≤ ) = (ordTop‘ ≤ ) |
| 28 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ·e 𝐶) = (𝑦 ·e 𝐶)) |
| 29 | 28 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
↦ (𝑥
·e 𝐶)) =
(𝑦 ∈
ℝ* ↦ (𝑦 ·e 𝐶)) |
| 30 | | id 22 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℝ+) |
| 31 | 27, 29, 30 | xrmulc1cn 33929 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ+
→ (𝑥 ∈
ℝ* ↦ (𝑥 ·e 𝐶)) ∈ ((ordTop‘ ≤ ) Cn
(ordTop‘ ≤ ))) |
| 32 | | letopuni 23215 |
. . . . . . . . 9
⊢
ℝ* = ∪ (ordTop‘ ≤
) |
| 33 | 32 | cnrest 23293 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ*
↦ (𝑥
·e 𝐶))
∈ ((ordTop‘ ≤ ) Cn (ordTop‘ ≤ )) ∧ (0[,]+∞)
⊆ ℝ*) → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞))
∈ (((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn
(ordTop‘ ≤ ))) |
| 34 | 31, 3, 33 | sylancl 586 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ ((𝑥 ∈
ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) ∈
(((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn (ordTop‘
≤ ))) |
| 35 | | resmpt 6055 |
. . . . . . . . 9
⊢
((0[,]+∞) ⊆ ℝ* → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) =
(𝑥 ∈ (0[,]+∞)
↦ (𝑥
·e 𝐶))) |
| 36 | 3, 35 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ*
↦ (𝑥
·e 𝐶))
↾ (0[,]+∞)) = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) |
| 37 | 36, 18 | eqtr4i 2768 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ*
↦ (𝑥
·e 𝐶))
↾ (0[,]+∞)) = 𝐹 |
| 38 | 1 | eqcomi 2746 |
. . . . . . . 8
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) = 𝐽 |
| 39 | 38 | oveq1i 7441 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn
(ordTop‘ ≤ )) = (𝐽
Cn (ordTop‘ ≤ )) |
| 40 | 34, 37, 39 | 3eltr3g 2857 |
. . . . . 6
⊢ (𝐶 ∈ ℝ+
→ 𝐹 ∈ (𝐽 Cn (ordTop‘ ≤
))) |
| 41 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ (ordTop‘ ≤ ) ∈
(TopOn‘ℝ*)) |
| 42 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ+
∧ 𝑥 ∈
(0[,]+∞)) → 𝑥
∈ (0[,]+∞)) |
| 43 | | ioorp 13465 |
. . . . . . . . . . . 12
⊢
(0(,)+∞) = ℝ+ |
| 44 | | ioossicc 13473 |
. . . . . . . . . . . 12
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
| 45 | 43, 44 | eqsstrri 4031 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ (0[,]+∞) |
| 46 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℝ+
∧ 𝑥 ∈
(0[,]+∞)) → 𝐶
∈ ℝ+) |
| 47 | 45, 46 | sselid 3981 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℝ+
∧ 𝑥 ∈
(0[,]+∞)) → 𝐶
∈ (0[,]+∞)) |
| 48 | | ge0xmulcl 13503 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (0[,]+∞) ∧
𝐶 ∈ (0[,]+∞))
→ (𝑥
·e 𝐶)
∈ (0[,]+∞)) |
| 49 | 42, 47, 48 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ+
∧ 𝑥 ∈
(0[,]+∞)) → (𝑥
·e 𝐶)
∈ (0[,]+∞)) |
| 50 | 49, 18 | fmptd 7134 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ+
→ 𝐹:(0[,]+∞)⟶(0[,]+∞)) |
| 51 | 50 | frnd 6744 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ ran 𝐹 ⊆
(0[,]+∞)) |
| 52 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ (0[,]+∞) ⊆ ℝ*) |
| 53 | | cnrest2 23294 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
ran 𝐹 ⊆
(0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → (𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ )) ↔ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ )
↾t (0[,]+∞))))) |
| 54 | 41, 51, 52, 53 | syl3anc 1373 |
. . . . . 6
⊢ (𝐶 ∈ ℝ+
→ (𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ ))
↔ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ )
↾t (0[,]+∞))))) |
| 55 | 40, 54 | mpbid 232 |
. . . . 5
⊢ (𝐶 ∈ ℝ+
→ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ )
↾t (0[,]+∞)))) |
| 56 | 1 | oveq2i 7442 |
. . . . 5
⊢ (𝐽 Cn 𝐽) = (𝐽 Cn ((ordTop‘ ≤ )
↾t (0[,]+∞))) |
| 57 | 55, 56 | eleqtrrdi 2852 |
. . . 4
⊢ (𝐶 ∈ ℝ+
→ 𝐹 ∈ (𝐽 Cn 𝐽)) |
| 58 | 57, 43 | eleq2s 2859 |
. . 3
⊢ (𝐶 ∈ (0(,)+∞) →
𝐹 ∈ (𝐽 Cn 𝐽)) |
| 59 | 58 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ (0(,)+∞)) → 𝐹 ∈ (𝐽 Cn 𝐽)) |
| 60 | | xrge0mulc1cn.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
| 61 | | 0xr 11308 |
. . . 4
⊢ 0 ∈
ℝ* |
| 62 | | pnfxr 11315 |
. . . 4
⊢ +∞
∈ ℝ* |
| 63 | | 0ltpnf 13164 |
. . . 4
⊢ 0 <
+∞ |
| 64 | | elicoelioo 32780 |
. . . 4
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
< +∞) → (𝐶
∈ (0[,)+∞) ↔ (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞)))) |
| 65 | 61, 62, 63, 64 | mp3an 1463 |
. . 3
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 = 0 ∨ 𝐶 ∈
(0(,)+∞))) |
| 66 | 60, 65 | sylib 218 |
. 2
⊢ (𝜑 → (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞))) |
| 67 | 26, 59, 66 | mpjaodan 961 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽)) |