Metamath Proof Explorer

Theorem xrge0mulc1cn

Description: The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Hypotheses xrge0mulc1cn.k ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
xrge0mulc1cn.f ⊢ F = x ∈ 0 +∞ ⟼ x ⋅ 𝑒 C
xrge0mulc1cn.c ⊢ φ → C ∈ 0 +∞
Assertion xrge0mulc1cn ⊢ φ → F ∈ J Cn J

Proof

Step Hyp Ref Expression
1 xrge0mulc1cn.k ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
2 xrge0mulc1cn.f ⊢ F = x ∈ 0 +∞ ⟼ x ⋅ 𝑒 C
3 xrge0mulc1cn.c ⊢ φ → C ∈ 0 +∞
4 letopon ⊢ ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ *
5 iccssxr ⊢ 0 +∞ ⊆ ℝ *
6 resttopon ⊢ ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ * ∧ 0 +∞ ⊆ ℝ * → ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ∈ TopOn ⁡ 0 +∞
7 4 5 6 mp2an ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ ∈ TopOn ⁡ 0 +∞
8 1 7 eqeltri ⊢ J ∈ TopOn ⁡ 0 +∞
9 8 a1i ⊢ C = 0 → J ∈ TopOn ⁡ 0 +∞
10 0e0iccpnf ⊢ 0 ∈ 0 +∞
11 10 a1i ⊢ C = 0 → 0 ∈ 0 +∞
12 simpl ⊢ C = 0 ∧ x ∈ 0 +∞ → C = 0
13 12 oveq2d ⊢ C = 0 ∧ x ∈ 0 +∞ → x ⋅ 𝑒 C = x ⋅ 𝑒 0
14 simpr ⊢ C = 0 ∧ x ∈ 0 +∞ → x ∈ 0 +∞
15 5 14 sselid ⊢ C = 0 ∧ x ∈ 0 +∞ → x ∈ ℝ *
16 xmul01 ⊢ x ∈ ℝ * → x ⋅ 𝑒 0 = 0
17 15 16 syl ⊢ C = 0 ∧ x ∈ 0 +∞ → x ⋅ 𝑒 0 = 0
18 13 17 eqtrd ⊢ C = 0 ∧ x ∈ 0 +∞ → x ⋅ 𝑒 C = 0
19 18 mpteq2dva ⊢ C = 0 → x ∈ 0 +∞ ⟼ x ⋅ 𝑒 C = x ∈ 0 +∞ ⟼ 0
20 fconstmpt ⊢ 0 +∞ × 0 = x ∈ 0 +∞ ⟼ 0
21 19 2 20 3eqtr4g ⊢ C = 0 → F = 0 +∞ × 0
22 c0ex ⊢ 0 ∈ V
23 22 fconst2 ⊢ F : 0 +∞ ⟶ 0 ↔ F = 0 +∞ × 0
24 21 23 sylibr ⊢ C = 0 → F : 0 +∞ ⟶ 0
25 cnconst ⊢ J ∈ TopOn ⁡ 0 +∞ ∧ J ∈ TopOn ⁡ 0 +∞ ∧ 0 ∈ 0 +∞ ∧ F : 0 +∞ ⟶ 0 → F ∈ J Cn J
26 9 9 11 24 25 syl22anc ⊢ C = 0 → F ∈ J Cn J
27 26 adantl ⊢ φ ∧ C = 0 → F ∈ J Cn J
28 eqid ⊢ ordTop ⁡ ≤ = ordTop ⁡ ≤
29 oveq1 ⊢ x = y → x ⋅ 𝑒 C = y ⋅ 𝑒 C
30 29 cbvmptv ⊢ x ∈ ℝ * ⟼ x ⋅ 𝑒 C = y ∈ ℝ * ⟼ y ⋅ 𝑒 C
31 id ⊢ C ∈ ℝ + → C ∈ ℝ +
32 28 30 31 xrmulc1cn ⊢ C ∈ ℝ + → x ∈ ℝ * ⟼ x ⋅ 𝑒 C ∈ ordTop ⁡ ≤ Cn ordTop ⁡ ≤
33 letopuni ⊢ ℝ * = ⋃ ordTop ⁡ ≤
34 33 cnrest ⊢ x ∈ ℝ * ⟼ x ⋅ 𝑒 C ∈ ordTop ⁡ ≤ Cn ordTop ⁡ ≤ ∧ 0 +∞ ⊆ ℝ * → x ∈ ℝ * ⟼ x ⋅ 𝑒 C ↾ 0 +∞ ∈ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ Cn ordTop ⁡ ≤
35 32 5 34 sylancl ⊢ C ∈ ℝ + → x ∈ ℝ * ⟼ x ⋅ 𝑒 C ↾ 0 +∞ ∈ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ Cn ordTop ⁡ ≤
36 resmpt ⊢ 0 +∞ ⊆ ℝ * → x ∈ ℝ * ⟼ x ⋅ 𝑒 C ↾ 0 +∞ = x ∈ 0 +∞ ⟼ x ⋅ 𝑒 C
37 5 36 ax-mp ⊢ x ∈ ℝ * ⟼ x ⋅ 𝑒 C ↾ 0 +∞ = x ∈ 0 +∞ ⟼ x ⋅ 𝑒 C
38 37 2 eqtr4i ⊢ x ∈ ℝ * ⟼ x ⋅ 𝑒 C ↾ 0 +∞ = F
39 1 eqcomi ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = J
40 39 oveq1i ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ Cn ordTop ⁡ ≤ = J Cn ordTop ⁡ ≤
41 35 38 40 3eltr3g ⊢ C ∈ ℝ + → F ∈ J Cn ordTop ⁡ ≤
42 4 a1i ⊢ C ∈ ℝ + → ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ *
43 simpr ⊢ C ∈ ℝ + ∧ x ∈ 0 +∞ → x ∈ 0 +∞
44 ioorp ⊢ 0 +∞ = ℝ +
45 ioossicc ⊢ 0 +∞ ⊆ 0 +∞
46 44 45 eqsstrri ⊢ ℝ + ⊆ 0 +∞
47 simpl ⊢ C ∈ ℝ + ∧ x ∈ 0 +∞ → C ∈ ℝ +
48 46 47 sselid ⊢ C ∈ ℝ + ∧ x ∈ 0 +∞ → C ∈ 0 +∞
49 ge0xmulcl ⊢ x ∈ 0 +∞ ∧ C ∈ 0 +∞ → x ⋅ 𝑒 C ∈ 0 +∞
50 43 48 49 syl2anc ⊢ C ∈ ℝ + ∧ x ∈ 0 +∞ → x ⋅ 𝑒 C ∈ 0 +∞
51 50 2 fmptd ⊢ C ∈ ℝ + → F : 0 +∞ ⟶ 0 +∞
52 51 frnd ⊢ C ∈ ℝ + → ran ⁡ F ⊆ 0 +∞
53 5 a1i ⊢ C ∈ ℝ + → 0 +∞ ⊆ ℝ *
54 cnrest2 ⊢ ordTop ⁡ ≤ ∈ TopOn ⁡ ℝ * ∧ ran ⁡ F ⊆ 0 +∞ ∧ 0 +∞ ⊆ ℝ * → F ∈ J Cn ordTop ⁡ ≤ ↔ F ∈ J Cn ordTop ⁡ ≤ ↾ 𝑡 0 +∞
55 42 52 53 54 syl3anc ⊢ C ∈ ℝ + → F ∈ J Cn ordTop ⁡ ≤ ↔ F ∈ J Cn ordTop ⁡ ≤ ↾ 𝑡 0 +∞
56 41 55 mpbid ⊢ C ∈ ℝ + → F ∈ J Cn ordTop ⁡ ≤ ↾ 𝑡 0 +∞
57 1 oveq2i ⊢ J Cn J = J Cn ordTop ⁡ ≤ ↾ 𝑡 0 +∞
58 56 57 eleqtrrdi ⊢ C ∈ ℝ + → F ∈ J Cn J
59 58 44 eleq2s ⊢ C ∈ 0 +∞ → F ∈ J Cn J
60 59 adantl ⊢ φ ∧ C ∈ 0 +∞ → F ∈ J Cn J
61 0xr ⊢ 0 ∈ ℝ *
62 pnfxr ⊢ +∞ ∈ ℝ *
63 0ltpnf ⊢ 0 < +∞
64 elicoelioo ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ 0 < +∞ → C ∈ 0 +∞ ↔ C = 0 ∨ C ∈ 0 +∞
65 61 62 63 64 mp3an ⊢ C ∈ 0 +∞ ↔ C = 0 ∨ C ∈ 0 +∞
66 3 65 sylib ⊢ φ → C = 0 ∨ C ∈ 0 +∞
67 27 60 66 mpjaodan ⊢ φ → F ∈ J Cn J