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∈JCnJ

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∈JCnJ
26 9 9 11 24 25 syl22anc ⊢C=0→F∈JCnJ
27 26 adantl ⊢φ∧C=0→F∈JCnJ
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⁡≤CnordTop⁡≤
33 letopuni ⊢ℝ*=⋃ordTop⁡≤
34 33 cnrest ⊢x∈ℝ*⟼x⋅𝑒C∈ordTop⁡≤CnordTop⁡≤∧0+∞⊆ℝ*→x∈ℝ*⟼x⋅𝑒C↾0+∞∈ordTop⁡≤↾𝑡0+∞CnordTop⁡≤
35 32 5 34 sylancl ⊢C∈ℝ+→x∈ℝ*⟼x⋅𝑒C↾0+∞∈ordTop⁡≤↾𝑡0+∞CnordTop⁡≤
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+∞CnordTop⁡≤=JCnordTop⁡≤
41 35 38 40 3eltr3g ⊢C∈ℝ+→F∈JCnordTop⁡≤
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∈JCnordTop⁡≤↔F∈JCnordTop⁡≤↾𝑡0+∞
55 42 52 53 54 syl3anc ⊢C∈ℝ+→F∈JCnordTop⁡≤↔F∈JCnordTop⁡≤↾𝑡0+∞
56 41 55 mpbid ⊢C∈ℝ+→F∈JCnordTop⁡≤↾𝑡0+∞
57 1 oveq2i ⊢JCnJ=JCnordTop⁡≤↾𝑡0+∞
58 56 57 eleqtrrdi ⊢C∈ℝ+→F∈JCnJ
59 58 44 eleq2s ⊢C∈0+∞→F∈JCnJ
60 59 adantl ⊢φ∧C∈0+∞→F∈JCnJ
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∈JCnJ