Theorem ioccncflimc 45841

Description: Limit at the upper bound of a continuous function defined on a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
ioccncflimc.a	⊢ (𝜑 → 𝐴 ∈ ℝ*)
ioccncflimc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ioccncflimc.altb	⊢ (𝜑 → 𝐴 < 𝐵)
ioccncflimc.f	⊢ (𝜑 → 𝐹 ∈ ((𝐴(,]𝐵)–cn→ℂ))

Assertion

Ref	Expression
ioccncflimc	⊢ (𝜑 → (𝐹‘𝐵) ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵))

Proof of Theorem ioccncflimc

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ioccncflimc.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,]𝐵)–cn→ℂ))
2		ioccncflimc.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
3		ioccncflimc.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	3	rexrd 11309	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		ioccncflimc.altb	. . . 4 ⊢ (𝜑 → 𝐴 < 𝐵)
6	3	leidd 11827	. . . 4 ⊢ (𝜑 → 𝐵 ≤ 𝐵)
7	2, 4, 4, 5, 6	eliocd 45460	. . 3 ⊢ (𝜑 → 𝐵 ∈ (𝐴(,]𝐵))
8	1, 7	cnlimci 25939	. 2 ⊢ (𝜑 → (𝐹‘𝐵) ∈ (𝐹 limℂ 𝐵))
9		cncfrss 24931	. . . . . . . 8 ⊢ (𝐹 ∈ ((𝐴(,]𝐵)–cn→ℂ) → (𝐴(,]𝐵) ⊆ ℂ)
10	1, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℂ)
11		ssid 4018	. . . . . . 7 ⊢ ℂ ⊆ ℂ
12		eqid 2735	. . . . . . . 8 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
13		eqid 2735	. . . . . . . 8 ⊢ ((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) = ((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵))
14		eqid 2735	. . . . . . . 8 ⊢ ((TopOpen‘ℂfld) ↾t ℂ) = ((TopOpen‘ℂfld) ↾t ℂ)
15	12, 13, 14	cncfcn 24950	. . . . . . 7 ⊢ (((𝐴(,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴(,]𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
16	10, 11, 15	sylancl 586	. . . . . 6 ⊢ (𝜑 → ((𝐴(,]𝐵)–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
17	1, 16	eleqtrd 2841	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t ℂ)))
18	12	cnfldtopon 24819	. . . . . . 7 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
19		resttopon 23185	. . . . . . 7 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝐴(,]𝐵) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) ∈ (TopOn‘(𝐴(,]𝐵)))
20	18, 10, 19	sylancr 587	. . . . . 6 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) ∈ (TopOn‘(𝐴(,]𝐵)))
21	12	cnfldtop 24820	. . . . . . . 8 ⊢ (TopOpen‘ℂfld) ∈ Top
22		unicntop 24822	. . . . . . . . 9 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
23	22	restid 17480	. . . . . . . 8 ⊢ ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
24	21, 23	ax-mp 5	. . . . . . 7 ⊢ ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
25	24	cnfldtopon 24819	. . . . . 6 ⊢ ((TopOpen‘ℂfld) ↾t ℂ) ∈ (TopOn‘ℂ)
26		cncnp 23304	. . . . . 6 ⊢ ((((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) ∈ (TopOn‘(𝐴(,]𝐵)) ∧ ((TopOpen‘ℂfld) ↾t ℂ) ∈ (TopOn‘ℂ)) → (𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t ℂ)) ↔ (𝐹:(𝐴(,]𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,]𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) CnP ((TopOpen‘ℂfld) ↾t ℂ))‘𝑥))))
27	20, 25, 26	sylancl 586	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ (((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) Cn ((TopOpen‘ℂfld) ↾t ℂ)) ↔ (𝐹:(𝐴(,]𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,]𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) CnP ((TopOpen‘ℂfld) ↾t ℂ))‘𝑥))))
28	17, 27	mpbid 232	. . . 4 ⊢ (𝜑 → (𝐹:(𝐴(,]𝐵)⟶ℂ ∧ ∀𝑥 ∈ (𝐴(,]𝐵)𝐹 ∈ ((((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) CnP ((TopOpen‘ℂfld) ↾t ℂ))‘𝑥)))
29	28	simpld 494	. . 3 ⊢ (𝜑 → 𝐹:(𝐴(,]𝐵)⟶ℂ)
30		ioossioc 45445	. . . 4 ⊢ (𝐴(,)𝐵) ⊆ (𝐴(,]𝐵)
31	30	a1i 11	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,]𝐵))
32		eqid 2735	. . 3 ⊢ ((TopOpen‘ℂfld) ↾t ((𝐴(,]𝐵) ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t ((𝐴(,]𝐵) ∪ {𝐵}))
33	3	recnd 11287	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℂ)
34	22	ntrtop 23094	. . . . . . . . 9 ⊢ ((TopOpen‘ℂfld) ∈ Top → ((int‘(TopOpen‘ℂfld))‘ℂ) = ℂ)
35	21, 34	ax-mp 5	. . . . . . . 8 ⊢ ((int‘(TopOpen‘ℂfld))‘ℂ) = ℂ
36		undif 4488	. . . . . . . . . . 11 ⊢ ((𝐴(,]𝐵) ⊆ ℂ ↔ ((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵))) = ℂ)
37	10, 36	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵))) = ℂ)
38	37	eqcomd 2741	. . . . . . . . 9 ⊢ (𝜑 → ℂ = ((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵))))
39	38	fveq2d 6911	. . . . . . . 8 ⊢ (𝜑 → ((int‘(TopOpen‘ℂfld))‘ℂ) = ((int‘(TopOpen‘ℂfld))‘((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵)))))
40	35, 39	eqtr3id 2789	. . . . . . 7 ⊢ (𝜑 → ℂ = ((int‘(TopOpen‘ℂfld))‘((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵)))))
41	33, 40	eleqtrd 2841	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ((int‘(TopOpen‘ℂfld))‘((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵)))))
42	41, 7	elind 4210	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (((int‘(TopOpen‘ℂfld))‘((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵)))) ∩ (𝐴(,]𝐵)))
43	21	a1i 11	. . . . . 6 ⊢ (𝜑 → (TopOpen‘ℂfld) ∈ Top)
44		ssid 4018	. . . . . . 7 ⊢ (𝐴(,]𝐵) ⊆ (𝐴(,]𝐵)
45	44	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ (𝐴(,]𝐵))
46	22, 13	restntr 23206	. . . . . 6 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ (𝐴(,]𝐵) ⊆ ℂ ∧ (𝐴(,]𝐵) ⊆ (𝐴(,]𝐵)) → ((int‘((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)))‘(𝐴(,]𝐵)) = (((int‘(TopOpen‘ℂfld))‘((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵)))) ∩ (𝐴(,]𝐵)))
47	43, 10, 45, 46	syl3anc 1370	. . . . 5 ⊢ (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)))‘(𝐴(,]𝐵)) = (((int‘(TopOpen‘ℂfld))‘((𝐴(,]𝐵) ∪ (ℂ ∖ (𝐴(,]𝐵)))) ∩ (𝐴(,]𝐵)))
48	42, 47	eleqtrrd 2842	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)))‘(𝐴(,]𝐵)))
49	7	snssd 4814	. . . . . . . . 9 ⊢ (𝜑 → {𝐵} ⊆ (𝐴(,]𝐵))
50		ssequn2 4199	. . . . . . . . 9 ⊢ ({𝐵} ⊆ (𝐴(,]𝐵) ↔ ((𝐴(,]𝐵) ∪ {𝐵}) = (𝐴(,]𝐵))
51	49, 50	sylib 218	. . . . . . . 8 ⊢ (𝜑 → ((𝐴(,]𝐵) ∪ {𝐵}) = (𝐴(,]𝐵))
52	51	eqcomd 2741	. . . . . . 7 ⊢ (𝜑 → (𝐴(,]𝐵) = ((𝐴(,]𝐵) ∪ {𝐵}))
53	52	oveq2d 7447	. . . . . 6 ⊢ (𝜑 → ((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)) = ((TopOpen‘ℂfld) ↾t ((𝐴(,]𝐵) ∪ {𝐵})))
54	53	fveq2d 6911	. . . . 5 ⊢ (𝜑 → (int‘((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵))) = (int‘((TopOpen‘ℂfld) ↾t ((𝐴(,]𝐵) ∪ {𝐵}))))
55		ioounsn 13514	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵))
56	2, 4, 5, 55	syl3anc 1370	. . . . . 6 ⊢ (𝜑 → ((𝐴(,)𝐵) ∪ {𝐵}) = (𝐴(,]𝐵))
57	56	eqcomd 2741	. . . . 5 ⊢ (𝜑 → (𝐴(,]𝐵) = ((𝐴(,)𝐵) ∪ {𝐵}))
58	54, 57	fveq12d 6914	. . . 4 ⊢ (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t (𝐴(,]𝐵)))‘(𝐴(,]𝐵)) = ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,]𝐵) ∪ {𝐵})))‘((𝐴(,)𝐵) ∪ {𝐵})))
59	48, 58	eleqtrd 2841	. . 3 ⊢ (𝜑 → 𝐵 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((𝐴(,]𝐵) ∪ {𝐵})))‘((𝐴(,)𝐵) ∪ {𝐵})))
60	29, 31, 10, 12, 32, 59	limcres 25936	. 2 ⊢ (𝜑 → ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵) = (𝐹 limℂ 𝐵))
61	8, 60	eleqtrrd 2842	1 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ((𝐹 ↾ (𝐴(,)𝐵)) limℂ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059   ∖ cdif 3960   ∪ cun 3961   ∩ cin 3962   ⊆ wss 3963  {csn 4631   class class class wbr 5148   ↾ cres 5691  ⟶wf 6559  ‘cfv 6563  (class class class)co 7431  ℂcc 11151  ℝcr 11152  ℝ^*cxr 11292   < clt 11293  (,)cioo 13384  (,]cioc 13385   ↾_t crest 17467  TopOpenctopn 17468  ℂ_fldccnfld 21382  Topctop 22915  TopOnctopon 22932  intcnt 23041   Cn ccn 23248   CnP ccnp 23249  –cn→ccncf 24916   lim_ℂ climc 25912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-map 8867  df-pm 8868  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fi 9449  df-sup 9480  df-inf 9481  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ioo 13388  df-ioc 13389  df-icc 13391  df-fz 13545  df-seq 14040  df-exp 14100  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-struct 17181  df-slot 17216  df-ndx 17228  df-base 17246  df-plusg 17311  df-mulr 17312  df-starv 17313  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-rest 17469  df-topn 17470  df-topgen 17490  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-cnfld 21383  df-top 22916  df-topon 22933  df-topsp 22955  df-bases 22969  df-ntr 23044  df-cn 23251  df-cnp 23252  df-xms 24346  df-ms 24347  df-cncf 24918  df-limc 25916

This theorem is referenced by:  fourierdlem46  46108