MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  psercnlem1 Structured version   Unicode version

Theorem psercnlem1 23366
Description: Lemma for psercn 23367. (Contributed by Mario Carneiro, 18-Mar-2015.)
Hypotheses
Ref Expression
pserf.g  |-  G  =  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
pserf.f  |-  F  =  ( y  e.  S  |-> 
sum_ j  e.  NN0  ( ( G `  y ) `  j
) )
pserf.a  |-  ( ph  ->  A : NN0 --> CC )
pserf.r  |-  R  =  sup ( { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
psercn.s  |-  S  =  ( `' abs " (
0 [,) R ) )
psercn.m  |-  M  =  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )
Assertion
Ref Expression
psercnlem1  |-  ( (
ph  /\  a  e.  S )  ->  ( M  e.  RR+  /\  ( abs `  a )  < 
M  /\  M  <  R ) )
Distinct variable groups:    j, a, n, r, x, y, A   
j, M, y    j, G, r, y    S, a, j, y    F, a    ph, a, j, y
Allowed substitution hints:    ph( x, n, r)    R( x, y, j, n, r, a)    S( x, n, r)    F( x, y, j, n, r)    G( x, n, a)    M( x, n, r, a)

Proof of Theorem psercnlem1
StepHypRef Expression
1 psercn.m . . . 4  |-  M  =  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )
2 psercn.s . . . . . . . . . . 11  |-  S  =  ( `' abs " (
0 [,) R ) )
3 cnvimass 5203 . . . . . . . . . . . 12  |-  ( `' abs " ( 0 [,) R ) ) 
C_  dom  abs
4 absf 13388 . . . . . . . . . . . . 13  |-  abs : CC
--> RR
54fdmi 5747 . . . . . . . . . . . 12  |-  dom  abs  =  CC
63, 5sseqtri 3496 . . . . . . . . . . 11  |-  ( `' abs " ( 0 [,) R ) ) 
C_  CC
72, 6eqsstri 3494 . . . . . . . . . 10  |-  S  C_  CC
87a1i 11 . . . . . . . . 9  |-  ( ph  ->  S  C_  CC )
98sselda 3464 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  a  e.  CC )
109abscld 13485 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  e.  RR )
11 readdcl 9622 . . . . . . 7  |-  ( ( ( abs `  a
)  e.  RR  /\  R  e.  RR )  ->  ( ( abs `  a
)  +  R )  e.  RR )
1210, 11sylan 473 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  R  e.  RR )  ->  (
( abs `  a
)  +  R )  e.  RR )
1312rehalfcld 10859 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  R  e.  RR )  ->  (
( ( abs `  a
)  +  R )  /  2 )  e.  RR )
14 peano2re 9806 . . . . . . 7  |-  ( ( abs `  a )  e.  RR  ->  (
( abs `  a
)  +  1 )  e.  RR )
1510, 14syl 17 . . . . . 6  |-  ( (
ph  /\  a  e.  S )  ->  (
( abs `  a
)  +  1 )  e.  RR )
1615adantr 466 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  -.  R  e.  RR )  ->  ( ( abs `  a
)  +  1 )  e.  RR )
1713, 16ifclda 3941 . . . 4  |-  ( (
ph  /\  a  e.  S )  ->  if ( R  e.  RR ,  ( ( ( abs `  a )  +  R )  / 
2 ) ,  ( ( abs `  a
)  +  1 ) )  e.  RR )
181, 17syl5eqel 2514 . . 3  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  RR )
19 0re 9643 . . . . 5  |-  0  e.  RR
2019a1i 11 . . . 4  |-  ( (
ph  /\  a  e.  S )  ->  0  e.  RR )
219absge0d 13493 . . . 4  |-  ( (
ph  /\  a  e.  S )  ->  0  <_  ( abs `  a
) )
22 breq2 4424 . . . . . 6  |-  ( ( ( ( abs `  a
)  +  R )  /  2 )  =  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )  ->  ( ( abs `  a )  < 
( ( ( abs `  a )  +  R
)  /  2 )  <-> 
( abs `  a
)  <  if ( R  e.  RR , 
( ( ( abs `  a )  +  R
)  /  2 ) ,  ( ( abs `  a )  +  1 ) ) ) )
23 breq2 4424 . . . . . 6  |-  ( ( ( abs `  a
)  +  1 )  =  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )  ->  ( ( abs `  a )  < 
( ( abs `  a
)  +  1 )  <-> 
( abs `  a
)  <  if ( R  e.  RR , 
( ( ( abs `  a )  +  R
)  /  2 ) ,  ( ( abs `  a )  +  1 ) ) ) )
24 simpr 462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  a  e.  S )  ->  a  e.  S )
2524, 2syl6eleq 2520 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  a  e.  ( `' abs " (
0 [,) R ) ) )
26 ffn 5742 . . . . . . . . . . . . 13  |-  ( abs
: CC --> RR  ->  abs 
Fn  CC )
27 elpreima 6013 . . . . . . . . . . . . 13  |-  ( abs 
Fn  CC  ->  ( a  e.  ( `' abs " ( 0 [,) R
) )  <->  ( a  e.  CC  /\  ( abs `  a )  e.  ( 0 [,) R ) ) ) )
284, 26, 27mp2b 10 . . . . . . . . . . . 12  |-  ( a  e.  ( `' abs " ( 0 [,) R
) )  <->  ( a  e.  CC  /\  ( abs `  a )  e.  ( 0 [,) R ) ) )
2925, 28sylib 199 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  (
a  e.  CC  /\  ( abs `  a )  e.  ( 0 [,) R ) ) )
3029simprd 464 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  e.  ( 0 [,) R
) )
31 iccssxr 11717 . . . . . . . . . . . 12  |-  ( 0 [,] +oo )  C_  RR*
32 pserf.g . . . . . . . . . . . . . 14  |-  G  =  ( x  e.  CC  |->  ( n  e.  NN0  |->  ( ( A `  n )  x.  (
x ^ n ) ) ) )
33 pserf.a . . . . . . . . . . . . . 14  |-  ( ph  ->  A : NN0 --> CC )
34 pserf.r . . . . . . . . . . . . . 14  |-  R  =  sup ( { r  e.  RR  |  seq 0 (  +  , 
( G `  r
) )  e.  dom  ~~>  } ,  RR* ,  <  )
3532, 33, 34radcnvcl 23358 . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  ( 0 [,] +oo ) )
3635adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  a  e.  S )  ->  R  e.  ( 0 [,] +oo ) )
3731, 36sseldi 3462 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  S )  ->  R  e.  RR* )
38 elico2 11698 . . . . . . . . . . 11  |-  ( ( 0  e.  RR  /\  R  e.  RR* )  -> 
( ( abs `  a
)  e.  ( 0 [,) R )  <->  ( ( abs `  a )  e.  RR  /\  0  <_ 
( abs `  a
)  /\  ( abs `  a )  <  R
) ) )
3919, 37, 38sylancr 667 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  S )  ->  (
( abs `  a
)  e.  ( 0 [,) R )  <->  ( ( abs `  a )  e.  RR  /\  0  <_ 
( abs `  a
)  /\  ( abs `  a )  <  R
) ) )
4030, 39mpbid 213 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  S )  ->  (
( abs `  a
)  e.  RR  /\  0  <_  ( abs `  a
)  /\  ( abs `  a )  <  R
) )
4140simp3d 1019 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  < 
R )
4241adantr 466 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  R  e.  RR )  ->  ( abs `  a )  < 
R )
43 avglt1 10850 . . . . . . . 8  |-  ( ( ( abs `  a
)  e.  RR  /\  R  e.  RR )  ->  ( ( abs `  a
)  <  R  <->  ( abs `  a )  <  (
( ( abs `  a
)  +  R )  /  2 ) ) )
4410, 43sylan 473 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  S )  /\  R  e.  RR )  ->  (
( abs `  a
)  <  R  <->  ( abs `  a )  <  (
( ( abs `  a
)  +  R )  /  2 ) ) )
4542, 44mpbid 213 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  R  e.  RR )  ->  ( abs `  a )  < 
( ( ( abs `  a )  +  R
)  /  2 ) )
4610ltp1d 10537 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  < 
( ( abs `  a
)  +  1 ) )
4746adantr 466 . . . . . 6  |-  ( ( ( ph  /\  a  e.  S )  /\  -.  R  e.  RR )  ->  ( abs `  a
)  <  ( ( abs `  a )  +  1 ) )
4822, 23, 45, 47ifbothda 3944 . . . . 5  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  < 
if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) ) )
4948, 1syl6breqr 4461 . . . 4  |-  ( (
ph  /\  a  e.  S )  ->  ( abs `  a )  < 
M )
5020, 10, 18, 21, 49lelttrd 9793 . . 3  |-  ( (
ph  /\  a  e.  S )  ->  0  <  M )
5118, 50elrpd 11338 . 2  |-  ( (
ph  /\  a  e.  S )  ->  M  e.  RR+ )
52 breq1 4423 . . . 4  |-  ( ( ( ( abs `  a
)  +  R )  /  2 )  =  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )  ->  ( (
( ( abs `  a
)  +  R )  /  2 )  < 
R  <->  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )  <  R ) )
53 breq1 4423 . . . 4  |-  ( ( ( abs `  a
)  +  1 )  =  if ( R  e.  RR ,  ( ( ( abs `  a
)  +  R )  /  2 ) ,  ( ( abs `  a
)  +  1 ) )  ->  ( (
( abs `  a
)  +  1 )  <  R  <->  if ( R  e.  RR , 
( ( ( abs `  a )  +  R
)  /  2 ) ,  ( ( abs `  a )  +  1 ) )  <  R
) )
54 avglt2 10851 . . . . . 6  |-  ( ( ( abs `  a
)  e.  RR  /\  R  e.  RR )  ->  ( ( abs `  a
)  <  R  <->  ( (
( abs `  a
)  +  R )  /  2 )  < 
R ) )
5510, 54sylan 473 . . . . 5  |-  ( ( ( ph  /\  a  e.  S )  /\  R  e.  RR )  ->  (
( abs `  a
)  <  R  <->  ( (
( abs `  a
)  +  R )  /  2 )  < 
R ) )
5642, 55mpbid 213 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  R  e.  RR )  ->  (
( ( abs `  a
)  +  R )  /  2 )  < 
R )
5715rexrd 9690 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  ->  (
( abs `  a
)  +  1 )  e.  RR* )
58 xrlenlt 9699 . . . . . . . 8  |-  ( ( R  e.  RR*  /\  (
( abs `  a
)  +  1 )  e.  RR* )  ->  ( R  <_  ( ( abs `  a )  +  1 )  <->  -.  ( ( abs `  a )  +  1 )  <  R
) )
5937, 57, 58syl2anc 665 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  ( R  <_  ( ( abs `  a )  +  1 )  <->  -.  ( ( abs `  a )  +  1 )  <  R
) )
60 0xr 9687 . . . . . . . . . . . . 13  |-  0  e.  RR*
61 pnfxr 11412 . . . . . . . . . . . . 13  |- +oo  e.  RR*
62 elicc1 11680 . . . . . . . . . . . . 13  |-  ( ( 0  e.  RR*  /\ +oo  e.  RR* )  ->  ( R  e.  ( 0 [,] +oo )  <->  ( R  e.  RR*  /\  0  <_  R  /\  R  <_ +oo )
) )
6360, 61, 62mp2an 676 . . . . . . . . . . . 12  |-  ( R  e.  ( 0 [,] +oo )  <->  ( R  e. 
RR*  /\  0  <_  R  /\  R  <_ +oo )
)
6435, 63sylib 199 . . . . . . . . . . 11  |-  ( ph  ->  ( R  e.  RR*  /\  0  <_  R  /\  R  <_ +oo ) )
6564simp2d 1018 . . . . . . . . . 10  |-  ( ph  ->  0  <_  R )
6665adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  S )  ->  0  <_  R )
67 ge0gtmnf 11467 . . . . . . . . 9  |-  ( ( R  e.  RR*  /\  0  <_  R )  -> -oo  <  R )
6837, 66, 67syl2anc 665 . . . . . . . 8  |-  ( (
ph  /\  a  e.  S )  -> -oo  <  R )
69 xrre 11464 . . . . . . . . 9  |-  ( ( ( R  e.  RR*  /\  ( ( abs `  a
)  +  1 )  e.  RR )  /\  ( -oo  <  R  /\  R  <_  ( ( abs `  a )  +  1 ) ) )  ->  R  e.  RR )
7069expr 618 . . . . . . . 8  |-  ( ( ( R  e.  RR*  /\  ( ( abs `  a
)  +  1 )  e.  RR )  /\ -oo 
<  R )  ->  ( R  <_  ( ( abs `  a )  +  1 )  ->  R  e.  RR ) )
7137, 15, 68, 70syl21anc 1263 . . . . . . 7  |-  ( (
ph  /\  a  e.  S )  ->  ( R  <_  ( ( abs `  a )  +  1 )  ->  R  e.  RR ) )
7259, 71sylbird 238 . . . . . 6  |-  ( (
ph  /\  a  e.  S )  ->  ( -.  ( ( abs `  a
)  +  1 )  <  R  ->  R  e.  RR ) )
7372con1d 127 . . . . 5  |-  ( (
ph  /\  a  e.  S )  ->  ( -.  R  e.  RR  ->  ( ( abs `  a
)  +  1 )  <  R ) )
7473imp 430 . . . 4  |-  ( ( ( ph  /\  a  e.  S )  /\  -.  R  e.  RR )  ->  ( ( abs `  a
)  +  1 )  <  R )
7552, 53, 56, 74ifbothda 3944 . . 3  |-  ( (
ph  /\  a  e.  S )  ->  if ( R  e.  RR ,  ( ( ( abs `  a )  +  R )  / 
2 ) ,  ( ( abs `  a
)  +  1 ) )  <  R )
761, 75syl5eqbr 4454 . 2  |-  ( (
ph  /\  a  e.  S )  ->  M  <  R )
7751, 49, 763jca 1185 1  |-  ( (
ph  /\  a  e.  S )  ->  ( M  e.  RR+  /\  ( abs `  a )  < 
M  /\  M  <  R ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1868   {crab 2779    C_ wss 3436   ifcif 3909   class class class wbr 4420    |-> cmpt 4479   `'ccnv 4848   dom cdm 4849   "cima 4852    Fn wfn 5592   -->wf 5593   ` cfv 5597  (class class class)co 6301   supcsup 7956   CCcc 9537   RRcr 9538   0cc0 9539   1c1 9540    + caddc 9542    x. cmul 9544   +oocpnf 9672   -oocmnf 9673   RR*cxr 9674    < clt 9675    <_ cle 9676    / cdiv 10269   2c2 10659   NN0cn0 10869   RR+crp 11302   [,)cico 11637   [,]cicc 11638    seqcseq 12212   ^cexp 12271   abscabs 13285    ~~> cli 13535   sum_csu 13739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-inf2 8148  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-pred 5395  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-om 6703  df-1st 6803  df-2nd 6804  df-wrecs 7032  df-recs 7094  df-rdg 7132  df-1o 7186  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-fin 7577  df-sup 7958  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-ico 11641  df-icc 11642  df-fz 11785  df-seq 12213  df-exp 12272  df-cj 13150  df-re 13151  df-im 13152  df-sqrt 13286  df-abs 13287  df-clim 13539
This theorem is referenced by:  psercn  23367  pserdvlem1  23368  pserdvlem2  23369  pserdv  23370
  Copyright terms: Public domain W3C validator