Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cncfiooicc Structured version   Visualization version   Unicode version

Theorem cncfiooicc 37814
Description: A continuous function  F on an open interval  ( A (,) B ) can be extended to a continuous function  G on the corresponding close interval, if it has a finite right limit  R in  A and a finite left limit  L in  B.  F can be complex valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
cncfiooicc.x  |-  F/ x ph
cncfiooicc.g  |-  G  =  ( x  e.  ( A [,] B ) 
|->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) ) )
cncfiooicc.a  |-  ( ph  ->  A  e.  RR )
cncfiooicc.b  |-  ( ph  ->  B  e.  RR )
cncfiooicc.f  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
cncfiooicc.l  |-  ( ph  ->  L  e.  ( F lim
CC  B ) )
cncfiooicc.r  |-  ( ph  ->  R  e.  ( F lim
CC  A ) )
Assertion
Ref Expression
cncfiooicc  |-  ( ph  ->  G  e.  ( ( A [,] B )
-cn-> CC ) )
Distinct variable groups:    x, A    x, B    x, F    x, L    x, R    ph, x
Allowed substitution hint:    G( x)

Proof of Theorem cncfiooicc
StepHypRef Expression
1 nfv 1765 . . 3  |-  F/ x
( ph  /\  A  < 
B )
2 cncfiooicc.g . . 3  |-  G  =  ( x  e.  ( A [,] B ) 
|->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) ) )
3 cncfiooicc.a . . . 4  |-  ( ph  ->  A  e.  RR )
43adantr 471 . . 3  |-  ( (
ph  /\  A  <  B )  ->  A  e.  RR )
5 cncfiooicc.b . . . 4  |-  ( ph  ->  B  e.  RR )
65adantr 471 . . 3  |-  ( (
ph  /\  A  <  B )  ->  B  e.  RR )
7 simpr 467 . . 3  |-  ( (
ph  /\  A  <  B )  ->  A  <  B )
8 cncfiooicc.f . . . 4  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
98adantr 471 . . 3  |-  ( (
ph  /\  A  <  B )  ->  F  e.  ( ( A (,) B ) -cn-> CC ) )
10 cncfiooicc.l . . . 4  |-  ( ph  ->  L  e.  ( F lim
CC  B ) )
1110adantr 471 . . 3  |-  ( (
ph  /\  A  <  B )  ->  L  e.  ( F lim CC  B ) )
12 cncfiooicc.r . . . 4  |-  ( ph  ->  R  e.  ( F lim
CC  A ) )
1312adantr 471 . . 3  |-  ( (
ph  /\  A  <  B )  ->  R  e.  ( F lim CC  A ) )
141, 2, 4, 6, 7, 9, 11, 13cncfiooicclem1 37813 . 2  |-  ( (
ph  /\  A  <  B )  ->  G  e.  ( ( A [,] B ) -cn-> CC ) )
15 limccl 22842 . . . . . . . . . 10  |-  ( F lim
CC  A )  C_  CC
1615, 12sseldi 3398 . . . . . . . . 9  |-  ( ph  ->  R  e.  CC )
1716snssd 4086 . . . . . . . 8  |-  ( ph  ->  { R }  C_  CC )
18 ssid 3419 . . . . . . . . 9  |-  CC  C_  CC
1918a1i 11 . . . . . . . 8  |-  ( ph  ->  CC  C_  CC )
20 cncfss 21942 . . . . . . . 8  |-  ( ( { R }  C_  CC  /\  CC  C_  CC )  ->  ( { A } -cn-> { R } ) 
C_  ( { A } -cn-> CC ) )
2117, 19, 20syl2anc 671 . . . . . . 7  |-  ( ph  ->  ( { A } -cn->
{ R } ) 
C_  ( { A } -cn-> CC ) )
2221adantr 471 . . . . . 6  |-  ( (
ph  /\  A  =  B )  ->  ( { A } -cn-> { R } )  C_  ( { A } -cn-> CC ) )
233rexrd 9677 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  RR* )
24 iccid 11671 . . . . . . . . . . . 12  |-  ( A  e.  RR*  ->  ( A [,] A )  =  { A } )
2523, 24syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( A [,] A
)  =  { A } )
26 oveq2 6284 . . . . . . . . . . 11  |-  ( A  =  B  ->  ( A [,] A )  =  ( A [,] B
) )
2725, 26sylan9req 2507 . . . . . . . . . 10  |-  ( (
ph  /\  A  =  B )  ->  { A }  =  ( A [,] B ) )
2827eqcomd 2458 . . . . . . . . 9  |-  ( (
ph  /\  A  =  B )  ->  ( A [,] B )  =  { A } )
29 simpr 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A  =  B )  /\  x  e.  ( A [,] B
) )  ->  x  e.  ( A [,] B
) )
3028adantr 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A  =  B )  /\  x  e.  ( A [,] B
) )  ->  ( A [,] B )  =  { A } )
3129, 30eleqtrd 2532 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A  =  B )  /\  x  e.  ( A [,] B
) )  ->  x  e.  { A } )
32 elsni 3961 . . . . . . . . . . 11  |-  ( x  e.  { A }  ->  x  =  A )
3331, 32syl 17 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =  B )  /\  x  e.  ( A [,] B
) )  ->  x  =  A )
3433iftrued 3857 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =  B )  /\  x  e.  ( A [,] B
) )  ->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) )  =  R )
3528, 34mpteq12dva 4452 . . . . . . . 8  |-  ( (
ph  /\  A  =  B )  ->  (
x  e.  ( A [,] B )  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `
 x ) ) ) )  =  ( x  e.  { A }  |->  R ) )
362, 35syl5eq 2498 . . . . . . 7  |-  ( (
ph  /\  A  =  B )  ->  G  =  ( x  e. 
{ A }  |->  R ) )
373recnd 9656 . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
3837adantr 471 . . . . . . . 8  |-  ( (
ph  /\  A  =  B )  ->  A  e.  CC )
3916adantr 471 . . . . . . . 8  |-  ( (
ph  /\  A  =  B )  ->  R  e.  CC )
40 cncfdmsn 37810 . . . . . . . 8  |-  ( ( A  e.  CC  /\  R  e.  CC )  ->  ( x  e.  { A }  |->  R )  e.  ( { A } -cn-> { R } ) )
4138, 39, 40syl2anc 671 . . . . . . 7  |-  ( (
ph  /\  A  =  B )  ->  (
x  e.  { A }  |->  R )  e.  ( { A } -cn->
{ R } ) )
4236, 41eqeltrd 2530 . . . . . 6  |-  ( (
ph  /\  A  =  B )  ->  G  e.  ( { A } -cn->
{ R } ) )
4322, 42sseldd 3401 . . . . 5  |-  ( (
ph  /\  A  =  B )  ->  G  e.  ( { A } -cn->
CC ) )
4427oveq1d 6291 . . . . 5  |-  ( (
ph  /\  A  =  B )  ->  ( { A } -cn-> CC )  =  ( ( A [,] B ) -cn-> CC ) )
4543, 44eleqtrd 2532 . . . 4  |-  ( (
ph  /\  A  =  B )  ->  G  e.  ( ( A [,] B ) -cn-> CC ) )
4645adantlr 726 . . 3  |-  ( ( ( ph  /\  -.  A  <  B )  /\  A  =  B )  ->  G  e.  ( ( A [,] B )
-cn-> CC ) )
47 simpll 765 . . . 4  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  ph )
48 eqcom 2459 . . . . . . . . 9  |-  ( B  =  A  <->  A  =  B )
4948biimpi 199 . . . . . . . 8  |-  ( B  =  A  ->  A  =  B )
5049con3i 142 . . . . . . 7  |-  ( -.  A  =  B  ->  -.  B  =  A
)
5150adantl 472 . . . . . 6  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  -.  B  =  A )
52 simplr 767 . . . . . 6  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  -.  A  <  B )
53 pm4.56 502 . . . . . . 7  |-  ( ( -.  B  =  A  /\  -.  A  < 
B )  <->  -.  ( B  =  A  \/  A  <  B ) )
5453biimpi 199 . . . . . 6  |-  ( ( -.  B  =  A  /\  -.  A  < 
B )  ->  -.  ( B  =  A  \/  A  <  B ) )
5551, 52, 54syl2anc 671 . . . . 5  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  -.  ( B  =  A  \/  A  <  B ) )
5647, 5syl 17 . . . . . 6  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  B  e.  RR )
5747, 3syl 17 . . . . . 6  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  A  e.  RR )
5856, 57lttrid 9760 . . . . 5  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  ( B  <  A  <->  -.  ( B  =  A  \/  A  <  B ) ) )
5955, 58mpbird 240 . . . 4  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  B  <  A )
60 0ss 3731 . . . . . . . 8  |-  (/)  C_  CC
61 eqid 2452 . . . . . . . . 9  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
6261cnfldtop 21815 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  e.  Top
63 rest0 20196 . . . . . . . . . . 11  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  (/) )  =  { (/)
} )
6462, 63ax-mp 5 . . . . . . . . . 10  |-  ( (
TopOpen ` fld )t  (/) )  =  { (/)
}
6564eqcomi 2461 . . . . . . . . 9  |-  { (/) }  =  ( ( TopOpen ` fld )t  (/) )
6661, 65, 65cncfcn 21952 . . . . . . . 8  |-  ( (
(/)  C_  CC  /\  (/)  C_  CC )  ->  ( (/) -cn-> (/) )  =  ( { (/) }  Cn  {
(/) } ) )
6760, 60, 66mp2an 683 . . . . . . 7  |-  ( (/) -cn-> (/) )  =  ( {
(/) }  Cn  { (/) } )
68 cncfss 21942 . . . . . . . 8  |-  ( (
(/)  C_  CC  /\  CC  C_  CC )  ->  ( (/)
-cn->
(/) )  C_  ( (/)
-cn-> CC ) )
6960, 18, 68mp2an 683 . . . . . . 7  |-  ( (/) -cn-> (/) )  C_  ( (/) -cn-> CC )
7067, 69eqsstr3i 3431 . . . . . 6  |-  ( {
(/) }  Cn  { (/) } )  C_  ( (/) -cn-> CC )
712a1i 11 . . . . . . . 8  |-  ( (
ph  /\  B  <  A )  ->  G  =  ( x  e.  ( A [,] B )  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `
 x ) ) ) ) )
72 simpr 467 . . . . . . . . . 10  |-  ( (
ph  /\  B  <  A )  ->  B  <  A )
7323adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  B  <  A )  ->  A  e.  RR* )
745rexrd 9677 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR* )
7574adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  B  <  A )  ->  B  e.  RR* )
76 icc0 11674 . . . . . . . . . . 11  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A [,] B
)  =  (/)  <->  B  <  A ) )
7773, 75, 76syl2anc 671 . . . . . . . . . 10  |-  ( (
ph  /\  B  <  A )  ->  ( ( A [,] B )  =  (/) 
<->  B  <  A ) )
7872, 77mpbird 240 . . . . . . . . 9  |-  ( (
ph  /\  B  <  A )  ->  ( A [,] B )  =  (/) )
7978mpteq1d 4456 . . . . . . . 8  |-  ( (
ph  /\  B  <  A )  ->  ( x  e.  ( A [,] B
)  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L , 
( F `  x
) ) ) )  =  ( x  e.  (/)  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L , 
( F `  x
) ) ) ) )
80 mpt0 5687 . . . . . . . . 9  |-  ( x  e.  (/)  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L , 
( F `  x
) ) ) )  =  (/)
8180a1i 11 . . . . . . . 8  |-  ( (
ph  /\  B  <  A )  ->  ( x  e.  (/)  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L , 
( F `  x
) ) ) )  =  (/) )
8271, 79, 813eqtrd 2490 . . . . . . 7  |-  ( (
ph  /\  B  <  A )  ->  G  =  (/) )
83 0cnf 37796 . . . . . . 7  |-  (/)  e.  ( { (/) }  Cn  { (/)
} )
8482, 83syl6eqel 2538 . . . . . 6  |-  ( (
ph  /\  B  <  A )  ->  G  e.  ( { (/) }  Cn  { (/)
} ) )
8570, 84sseldi 3398 . . . . 5  |-  ( (
ph  /\  B  <  A )  ->  G  e.  ( (/) -cn-> CC ) )
8678eqcomd 2458 . . . . . 6  |-  ( (
ph  /\  B  <  A )  ->  (/)  =  ( A [,] B ) )
8786oveq1d 6291 . . . . 5  |-  ( (
ph  /\  B  <  A )  ->  ( (/) -cn-> CC )  =  ( ( A [,] B ) -cn-> CC ) )
8885, 87eleqtrd 2532 . . . 4  |-  ( (
ph  /\  B  <  A )  ->  G  e.  ( ( A [,] B ) -cn-> CC ) )
8947, 59, 88syl2anc 671 . . 3  |-  ( ( ( ph  /\  -.  A  <  B )  /\  -.  A  =  B
)  ->  G  e.  ( ( A [,] B ) -cn-> CC ) )
9046, 89pm2.61dan 805 . 2  |-  ( (
ph  /\  -.  A  <  B )  ->  G  e.  ( ( A [,] B ) -cn-> CC ) )
9114, 90pm2.61dan 805 1  |-  ( ph  ->  G  e.  ( ( A [,] B )
-cn-> CC ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    = wceq 1448   F/wnf 1671    e. wcel 1891    C_ wss 3372   (/)c0 3699   ifcif 3849   {csn 3936   class class class wbr 4374    |-> cmpt 4433   ` cfv 5561  (class class class)co 6276   CCcc 9524   RRcr 9525   RR*cxr 9661    < clt 9662   (,)cioo 11625   [,]cicc 11628   ↾t crest 15330   TopOpenctopn 15331  ℂfldccnfld 18981   Topctop 19928    Cn ccn 20251   -cn->ccncf 21919   lim CC climc 22829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-rep 4487  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-cnex 9582  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602  ax-pre-mulgt0 9603  ax-pre-sup 9604
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-int 4205  df-iun 4250  df-iin 4251  df-br 4375  df-opab 4434  df-mpt 4435  df-tr 4470  df-eprel 4723  df-id 4727  df-po 4733  df-so 4734  df-fr 4771  df-we 4773  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-pred 5359  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-riota 6238  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-om 6681  df-1st 6781  df-2nd 6782  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-oadd 7173  df-er 7350  df-map 7461  df-pm 7462  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-fi 7912  df-sup 7943  df-inf 7944  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668  df-sub 9849  df-neg 9850  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-4 10659  df-5 10660  df-6 10661  df-7 10662  df-8 10663  df-9 10664  df-10 10665  df-n0 10860  df-z 10928  df-dec 11042  df-uz 11150  df-q 11255  df-rp 11293  df-xneg 11399  df-xadd 11400  df-xmul 11401  df-ioo 11629  df-ioc 11630  df-ico 11631  df-icc 11632  df-fz 11776  df-seq 12208  df-exp 12267  df-cj 13173  df-re 13174  df-im 13175  df-sqrt 13309  df-abs 13310  df-struct 15134  df-ndx 15135  df-slot 15136  df-base 15137  df-plusg 15214  df-mulr 15215  df-starv 15216  df-tset 15220  df-ple 15221  df-ds 15223  df-unif 15224  df-rest 15332  df-topn 15333  df-topgen 15353  df-psmet 18973  df-xmet 18974  df-met 18975  df-bl 18976  df-mopn 18977  df-cnfld 18982  df-top 19932  df-bases 19933  df-topon 19934  df-topsp 19935  df-cld 20045  df-ntr 20046  df-cls 20047  df-cn 20254  df-cnp 20255  df-xms 21346  df-ms 21347  df-cncf 21921  df-limc 22833
This theorem is referenced by:  cncfiooiccre  37815  cncfioobd  37817  itgioocnicc  37896  iblcncfioo  37897  fourierdlem73  38100  fourierdlem81  38108  fourierdlem82  38109
  Copyright terms: Public domain W3C validator