Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xrge0mulc1cn Structured version   Visualization version   GIF version

Theorem xrge0mulc1cn 29761
Description: The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.)
Hypotheses
Ref Expression
xrge0mulc1cn.k 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
xrge0mulc1cn.f 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶))
xrge0mulc1cn.c (𝜑𝐶 ∈ (0[,)+∞))
Assertion
Ref Expression
xrge0mulc1cn (𝜑𝐹 ∈ (𝐽 Cn 𝐽))
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐹(𝑥)   𝐽(𝑥)

Proof of Theorem xrge0mulc1cn
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 xrge0mulc1cn.k . . . . . 6 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))
2 letopon 20914 . . . . . . 7 (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
3 iccssxr 12195 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
4 resttopon 20870 . . . . . . 7 (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ (0[,]+∞) ⊆ ℝ*) → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ (TopOn‘(0[,]+∞)))
52, 3, 4mp2an 707 . . . . . 6 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ (TopOn‘(0[,]+∞))
61, 5eqeltri 2700 . . . . 5 𝐽 ∈ (TopOn‘(0[,]+∞))
76a1i 11 . . . 4 (𝐶 = 0 → 𝐽 ∈ (TopOn‘(0[,]+∞)))
8 0e0iccpnf 12222 . . . . 5 0 ∈ (0[,]+∞)
98a1i 11 . . . 4 (𝐶 = 0 → 0 ∈ (0[,]+∞))
10 simpl 473 . . . . . . . . 9 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝐶 = 0)
1110oveq2d 6621 . . . . . . . 8 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) = (𝑥 ·e 0))
12 simpr 477 . . . . . . . . . 10 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈ (0[,]+∞))
133, 12sseldi 3586 . . . . . . . . 9 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈ ℝ*)
14 xmul01 12037 . . . . . . . . 9 (𝑥 ∈ ℝ* → (𝑥 ·e 0) = 0)
1513, 14syl 17 . . . . . . . 8 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 0) = 0)
1611, 15eqtrd 2660 . . . . . . 7 ((𝐶 = 0 ∧ 𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) = 0)
1716mpteq2dva 4709 . . . . . 6 (𝐶 = 0 → (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)) = (𝑥 ∈ (0[,]+∞) ↦ 0))
18 xrge0mulc1cn.f . . . . . 6 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶))
19 fconstmpt 5128 . . . . . 6 ((0[,]+∞) × {0}) = (𝑥 ∈ (0[,]+∞) ↦ 0)
2017, 18, 193eqtr4g 2685 . . . . 5 (𝐶 = 0 → 𝐹 = ((0[,]+∞) × {0}))
21 c0ex 9979 . . . . . 6 0 ∈ V
2221fconst2 6425 . . . . 5 (𝐹:(0[,]+∞)⟶{0} ↔ 𝐹 = ((0[,]+∞) × {0}))
2320, 22sylibr 224 . . . 4 (𝐶 = 0 → 𝐹:(0[,]+∞)⟶{0})
24 cnconst 20993 . . . 4 (((𝐽 ∈ (TopOn‘(0[,]+∞)) ∧ 𝐽 ∈ (TopOn‘(0[,]+∞))) ∧ (0 ∈ (0[,]+∞) ∧ 𝐹:(0[,]+∞)⟶{0})) → 𝐹 ∈ (𝐽 Cn 𝐽))
257, 7, 9, 23, 24syl22anc 1324 . . 3 (𝐶 = 0 → 𝐹 ∈ (𝐽 Cn 𝐽))
2625adantl 482 . 2 ((𝜑𝐶 = 0) → 𝐹 ∈ (𝐽 Cn 𝐽))
27 eqid 2626 . . . . . . . . 9 (ordTop‘ ≤ ) = (ordTop‘ ≤ )
28 oveq1 6612 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 ·e 𝐶) = (𝑦 ·e 𝐶))
2928cbvmptv 4715 . . . . . . . . 9 (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) = (𝑦 ∈ ℝ* ↦ (𝑦 ·e 𝐶))
30 id 22 . . . . . . . . 9 (𝐶 ∈ ℝ+𝐶 ∈ ℝ+)
3127, 29, 30xrmulc1cn 29750 . . . . . . . 8 (𝐶 ∈ ℝ+ → (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ∈ ((ordTop‘ ≤ ) Cn (ordTop‘ ≤ )))
32 letopuni 20916 . . . . . . . . 9 * = (ordTop‘ ≤ )
3332cnrest 20994 . . . . . . . 8 (((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ∈ ((ordTop‘ ≤ ) Cn (ordTop‘ ≤ )) ∧ (0[,]+∞) ⊆ ℝ*) → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) ∈ (((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn (ordTop‘ ≤ )))
3431, 3, 33sylancl 693 . . . . . . 7 (𝐶 ∈ ℝ+ → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) ∈ (((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn (ordTop‘ ≤ )))
35 resmpt 5412 . . . . . . . . 9 ((0[,]+∞) ⊆ ℝ* → ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶)))
363, 35ax-mp 5 . . . . . . . 8 ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶))
3736, 18eqtr4i 2651 . . . . . . 7 ((𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶)) ↾ (0[,]+∞)) = 𝐹
381eqcomi 2635 . . . . . . . 8 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = 𝐽
3938oveq1i 6615 . . . . . . 7 (((ordTop‘ ≤ ) ↾t (0[,]+∞)) Cn (ordTop‘ ≤ )) = (𝐽 Cn (ordTop‘ ≤ ))
4034, 37, 393eltr3g 2720 . . . . . 6 (𝐶 ∈ ℝ+𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ )))
412a1i 11 . . . . . . 7 (𝐶 ∈ ℝ+ → (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*))
42 simpr 477 . . . . . . . . . 10 ((𝐶 ∈ ℝ+𝑥 ∈ (0[,]+∞)) → 𝑥 ∈ (0[,]+∞))
43 ioorp 12190 . . . . . . . . . . . 12 (0(,)+∞) = ℝ+
44 ioossicc 12198 . . . . . . . . . . . 12 (0(,)+∞) ⊆ (0[,]+∞)
4543, 44eqsstr3i 3620 . . . . . . . . . . 11 + ⊆ (0[,]+∞)
46 simpl 473 . . . . . . . . . . 11 ((𝐶 ∈ ℝ+𝑥 ∈ (0[,]+∞)) → 𝐶 ∈ ℝ+)
4745, 46sseldi 3586 . . . . . . . . . 10 ((𝐶 ∈ ℝ+𝑥 ∈ (0[,]+∞)) → 𝐶 ∈ (0[,]+∞))
48 ge0xmulcl 12226 . . . . . . . . . 10 ((𝑥 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) ∈ (0[,]+∞))
4942, 47, 48syl2anc 692 . . . . . . . . 9 ((𝐶 ∈ ℝ+𝑥 ∈ (0[,]+∞)) → (𝑥 ·e 𝐶) ∈ (0[,]+∞))
5049, 18fmptd 6341 . . . . . . . 8 (𝐶 ∈ ℝ+𝐹:(0[,]+∞)⟶(0[,]+∞))
51 frn 6012 . . . . . . . 8 (𝐹:(0[,]+∞)⟶(0[,]+∞) → ran 𝐹 ⊆ (0[,]+∞))
5250, 51syl 17 . . . . . . 7 (𝐶 ∈ ℝ+ → ran 𝐹 ⊆ (0[,]+∞))
533a1i 11 . . . . . . 7 (𝐶 ∈ ℝ+ → (0[,]+∞) ⊆ ℝ*)
54 cnrest2 20995 . . . . . . 7 (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ ran 𝐹 ⊆ (0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → (𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ )) ↔ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ ) ↾t (0[,]+∞)))))
5541, 52, 53, 54syl3anc 1323 . . . . . 6 (𝐶 ∈ ℝ+ → (𝐹 ∈ (𝐽 Cn (ordTop‘ ≤ )) ↔ 𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ ) ↾t (0[,]+∞)))))
5640, 55mpbid 222 . . . . 5 (𝐶 ∈ ℝ+𝐹 ∈ (𝐽 Cn ((ordTop‘ ≤ ) ↾t (0[,]+∞))))
571oveq2i 6616 . . . . 5 (𝐽 Cn 𝐽) = (𝐽 Cn ((ordTop‘ ≤ ) ↾t (0[,]+∞)))
5856, 57syl6eleqr 2715 . . . 4 (𝐶 ∈ ℝ+𝐹 ∈ (𝐽 Cn 𝐽))
5958, 43eleq2s 2722 . . 3 (𝐶 ∈ (0(,)+∞) → 𝐹 ∈ (𝐽 Cn 𝐽))
6059adantl 482 . 2 ((𝜑𝐶 ∈ (0(,)+∞)) → 𝐹 ∈ (𝐽 Cn 𝐽))
61 xrge0mulc1cn.c . . 3 (𝜑𝐶 ∈ (0[,)+∞))
62 0xr 10031 . . . 4 0 ∈ ℝ*
63 pnfxr 10037 . . . 4 +∞ ∈ ℝ*
64 0ltpnf 11900 . . . 4 0 < +∞
65 elicoelioo 29376 . . . 4 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → (𝐶 ∈ (0[,)+∞) ↔ (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞))))
6662, 63, 64, 65mp3an 1421 . . 3 (𝐶 ∈ (0[,)+∞) ↔ (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞)))
6761, 66sylib 208 . 2 (𝜑 → (𝐶 = 0 ∨ 𝐶 ∈ (0(,)+∞)))
6826, 60, 67mpjaodan 826 1 (𝜑𝐹 ∈ (𝐽 Cn 𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1992  wss 3560  {csn 4153   class class class wbr 4618  cmpt 4678   × cxp 5077  ran crn 5080  cres 5081  wf 5846  cfv 5850  (class class class)co 6605  0cc0 9881  +∞cpnf 10016  *cxr 10018   < clt 10019  cle 10020  +crp 11776   ·e cxmu 11889  (,)cioo 12114  [,)cico 12116  [,]cicc 12117  t crest 15997  ordTopcordt 16075  TopOnctopon 20613   Cn ccn 20933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-isom 5859  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-oadd 7510  df-er 7688  df-map 7805  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-fi 8262  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-rp 11777  df-xneg 11890  df-xmul 11892  df-ioo 12118  df-ico 12120  df-icc 12121  df-rest 15999  df-topgen 16020  df-ordt 16077  df-ps 17116  df-tsr 17117  df-top 20616  df-bases 20617  df-topon 20618  df-cn 20936  df-cnp 20937
This theorem is referenced by:  esummulc1  29916
  Copyright terms: Public domain W3C validator