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

Theorem psercnlem1 25018
 Description: Lemma for psercn 25019. (Contributed by Mario Carneiro, 18-Mar-2015.)
Hypotheses
Ref Expression
pserf.g 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
pserf.f 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
pserf.a (𝜑𝐴:ℕ0⟶ℂ)
pserf.r 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
psercn.s 𝑆 = (abs “ (0[,)𝑅))
psercn.m 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))
Assertion
Ref Expression
psercnlem1 ((𝜑𝑎𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀𝑀 < 𝑅))
Distinct variable groups:   𝑗,𝑎,𝑛,𝑟,𝑥,𝑦,𝐴   𝑗,𝑀,𝑦   𝑗,𝐺,𝑟,𝑦   𝑆,𝑎,𝑗,𝑦   𝐹,𝑎   𝜑,𝑎,𝑗,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑛,𝑟)   𝑅(𝑥,𝑦,𝑗,𝑛,𝑟,𝑎)   𝑆(𝑥,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑗,𝑛,𝑟)   𝐺(𝑥,𝑛,𝑎)   𝑀(𝑥,𝑛,𝑟,𝑎)

Proof of Theorem psercnlem1
StepHypRef Expression
1 psercn.m . . . 4 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))
2 psercn.s . . . . . . . . . . 11 𝑆 = (abs “ (0[,)𝑅))
3 cnvimass 5927 . . . . . . . . . . . 12 (abs “ (0[,)𝑅)) ⊆ dom abs
4 absf 14688 . . . . . . . . . . . . 13 abs:ℂ⟶ℝ
54fdmi 6505 . . . . . . . . . . . 12 dom abs = ℂ
63, 5sseqtri 3978 . . . . . . . . . . 11 (abs “ (0[,)𝑅)) ⊆ ℂ
72, 6eqsstri 3976 . . . . . . . . . 10 𝑆 ⊆ ℂ
87a1i 11 . . . . . . . . 9 (𝜑𝑆 ⊆ ℂ)
98sselda 3942 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝑎 ∈ ℂ)
109abscld 14787 . . . . . . 7 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ ℝ)
11 readdcl 10609 . . . . . . 7 (((abs‘𝑎) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 𝑅) ∈ ℝ)
1210, 11sylan 583 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 𝑅) ∈ ℝ)
1312rehalfcld 11872 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → (((abs‘𝑎) + 𝑅) / 2) ∈ ℝ)
14 peano2re 10802 . . . . . . 7 ((abs‘𝑎) ∈ ℝ → ((abs‘𝑎) + 1) ∈ ℝ)
1510, 14syl 17 . . . . . 6 ((𝜑𝑎𝑆) → ((abs‘𝑎) + 1) ∈ ℝ)
1615adantr 484 . . . . 5 (((𝜑𝑎𝑆) ∧ ¬ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 1) ∈ ℝ)
1713, 16ifclda 4473 . . . 4 ((𝜑𝑎𝑆) → if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ∈ ℝ)
181, 17eqeltrid 2918 . . 3 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ)
19 0re 10632 . . . . 5 0 ∈ ℝ
2019a1i 11 . . . 4 ((𝜑𝑎𝑆) → 0 ∈ ℝ)
219absge0d 14795 . . . 4 ((𝜑𝑎𝑆) → 0 ≤ (abs‘𝑎))
22 breq2 5046 . . . . . 6 ((((abs‘𝑎) + 𝑅) / 2) = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))))
23 breq2 5046 . . . . . 6 (((abs‘𝑎) + 1) = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < ((abs‘𝑎) + 1) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))))
24 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 𝑎𝑆)
2524, 2eleqtrdi 2924 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑎 ∈ (abs “ (0[,)𝑅)))
26 ffn 6494 . . . . . . . . . . . . 13 (abs:ℂ⟶ℝ → abs Fn ℂ)
27 elpreima 6810 . . . . . . . . . . . . 13 (abs Fn ℂ → (𝑎 ∈ (abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅))))
284, 26, 27mp2b 10 . . . . . . . . . . . 12 (𝑎 ∈ (abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅)))
2925, 28sylib 221 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅)))
3029simprd 499 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ (0[,)𝑅))
31 iccssxr 12808 . . . . . . . . . . . 12 (0[,]+∞) ⊆ ℝ*
32 pserf.g . . . . . . . . . . . . . 14 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
33 pserf.a . . . . . . . . . . . . . 14 (𝜑𝐴:ℕ0⟶ℂ)
34 pserf.r . . . . . . . . . . . . . 14 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
3532, 33, 34radcnvcl 25010 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ (0[,]+∞))
3635adantr 484 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → 𝑅 ∈ (0[,]+∞))
3731, 36sseldi 3940 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑅 ∈ ℝ*)
38 elico2 12789 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 𝑅 ∈ ℝ*) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤ (abs‘𝑎) ∧ (abs‘𝑎) < 𝑅)))
3919, 37, 38sylancr 590 . . . . . . . . . 10 ((𝜑𝑎𝑆) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤ (abs‘𝑎) ∧ (abs‘𝑎) < 𝑅)))
4030, 39mpbid 235 . . . . . . . . 9 ((𝜑𝑎𝑆) → ((abs‘𝑎) ∈ ℝ ∧ 0 ≤ (abs‘𝑎) ∧ (abs‘𝑎) < 𝑅))
4140simp3d 1141 . . . . . . . 8 ((𝜑𝑎𝑆) → (abs‘𝑎) < 𝑅)
4241adantr 484 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < 𝑅)
43 avglt1 11863 . . . . . . . 8 (((abs‘𝑎) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2)))
4410, 43sylan 583 . . . . . . 7 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2)))
4542, 44mpbid 235 . . . . . 6 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))
4610ltp1d 11559 . . . . . . 7 ((𝜑𝑎𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 1))
4746adantr 484 . . . . . 6 (((𝜑𝑎𝑆) ∧ ¬ 𝑅 ∈ ℝ) → (abs‘𝑎) < ((abs‘𝑎) + 1))
4822, 23, 45, 47ifbothda 4476 . . . . 5 ((𝜑𝑎𝑆) → (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))
4948, 1breqtrrdi 5084 . . . 4 ((𝜑𝑎𝑆) → (abs‘𝑎) < 𝑀)
5020, 10, 18, 21, 49lelttrd 10787 . . 3 ((𝜑𝑎𝑆) → 0 < 𝑀)
5118, 50elrpd 12416 . 2 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ+)
52 breq1 5045 . . . 4 ((((abs‘𝑎) + 𝑅) / 2) = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((((abs‘𝑎) + 𝑅) / 2) < 𝑅 ↔ if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅))
53 breq1 5045 . . . 4 (((abs‘𝑎) + 1) = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → (((abs‘𝑎) + 1) < 𝑅 ↔ if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅))
54 avglt2 11864 . . . . . 6 (((abs‘𝑎) ∈ ℝ ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (((abs‘𝑎) + 𝑅) / 2) < 𝑅))
5510, 54sylan 583 . . . . 5 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (((abs‘𝑎) + 𝑅) / 2) < 𝑅))
5642, 55mpbid 235 . . . 4 (((𝜑𝑎𝑆) ∧ 𝑅 ∈ ℝ) → (((abs‘𝑎) + 𝑅) / 2) < 𝑅)
5715rexrd 10680 . . . . . . . 8 ((𝜑𝑎𝑆) → ((abs‘𝑎) + 1) ∈ ℝ*)
5837, 57xrlenltd 10696 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑅 ≤ ((abs‘𝑎) + 1) ↔ ¬ ((abs‘𝑎) + 1) < 𝑅))
59 0xr 10677 . . . . . . . . . . . . 13 0 ∈ ℝ*
60 pnfxr 10684 . . . . . . . . . . . . 13 +∞ ∈ ℝ*
61 elicc1 12770 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑅 ∈ (0[,]+∞) ↔ (𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞)))
6259, 60, 61mp2an 691 . . . . . . . . . . . 12 (𝑅 ∈ (0[,]+∞) ↔ (𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞))
6335, 62sylib 221 . . . . . . . . . . 11 (𝜑 → (𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞))
6463simp2d 1140 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑅)
6564adantr 484 . . . . . . . . 9 ((𝜑𝑎𝑆) → 0 ≤ 𝑅)
66 ge0gtmnf 12553 . . . . . . . . 9 ((𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅) → -∞ < 𝑅)
6737, 65, 66syl2anc 587 . . . . . . . 8 ((𝜑𝑎𝑆) → -∞ < 𝑅)
68 xrre 12550 . . . . . . . . 9 (((𝑅 ∈ ℝ* ∧ ((abs‘𝑎) + 1) ∈ ℝ) ∧ (-∞ < 𝑅𝑅 ≤ ((abs‘𝑎) + 1))) → 𝑅 ∈ ℝ)
6968expr 460 . . . . . . . 8 (((𝑅 ∈ ℝ* ∧ ((abs‘𝑎) + 1) ∈ ℝ) ∧ -∞ < 𝑅) → (𝑅 ≤ ((abs‘𝑎) + 1) → 𝑅 ∈ ℝ))
7037, 15, 67, 69syl21anc 836 . . . . . . 7 ((𝜑𝑎𝑆) → (𝑅 ≤ ((abs‘𝑎) + 1) → 𝑅 ∈ ℝ))
7158, 70sylbird 263 . . . . . 6 ((𝜑𝑎𝑆) → (¬ ((abs‘𝑎) + 1) < 𝑅𝑅 ∈ ℝ))
7271con1d 147 . . . . 5 ((𝜑𝑎𝑆) → (¬ 𝑅 ∈ ℝ → ((abs‘𝑎) + 1) < 𝑅))
7372imp 410 . . . 4 (((𝜑𝑎𝑆) ∧ ¬ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 1) < 𝑅)
7452, 53, 56, 73ifbothda 4476 . . 3 ((𝜑𝑎𝑆) → if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅)
751, 74eqbrtrid 5077 . 2 ((𝜑𝑎𝑆) → 𝑀 < 𝑅)
7651, 49, 753jca 1125 1 ((𝜑𝑎𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀𝑀 < 𝑅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2114  {crab 3134   ⊆ wss 3908  ifcif 4439   class class class wbr 5042   ↦ cmpt 5122  ◡ccnv 5531  dom cdm 5532   “ cima 5535   Fn wfn 6329  ⟶wf 6330  ‘cfv 6334  (class class class)co 7140  supcsup 8892  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  +∞cpnf 10661  -∞cmnf 10662  ℝ*cxr 10663   < clt 10664   ≤ cle 10665   / cdiv 11286  2c2 11680  ℕ0cn0 11885  ℝ+crp 12377  [,)cico 12728  [,]cicc 12729  seqcseq 13364  ↑cexp 13425  abscabs 14584   ⇝ cli 14832  Σcsu 15033 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-sup 8894  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-ico 12732  df-icc 12733  df-fz 12886  df-seq 13365  df-exp 13426  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-clim 14836 This theorem is referenced by:  psercn  25019  pserdvlem1  25020  pserdvlem2  25021  pserdv  25022
 Copyright terms: Public domain W3C validator