Metamath Proof Explorer


Theorem psercnlem1

Description: Lemma for psercn . (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses pserf.g G = x n 0 A n x n
pserf.f F = y S j 0 G y j
pserf.a φ A : 0
pserf.r R = sup r | seq 0 + G r dom * <
psercn.s S = abs -1 0 R
psercn.m M = if R a + R 2 a + 1
Assertion psercnlem1 φ a S M + a < M M < R

Proof

Step Hyp Ref Expression
1 pserf.g G = x n 0 A n x n
2 pserf.f F = y S j 0 G y j
3 pserf.a φ A : 0
4 pserf.r R = sup r | seq 0 + G r dom * <
5 psercn.s S = abs -1 0 R
6 psercn.m M = if R a + R 2 a + 1
7 cnvimass abs -1 0 R dom abs
8 absf abs :
9 8 fdmi dom abs =
10 7 9 sseqtri abs -1 0 R
11 5 10 eqsstri S
12 11 a1i φ S
13 12 sselda φ a S a
14 13 abscld φ a S a
15 readdcl a R a + R
16 14 15 sylan φ a S R a + R
17 16 rehalfcld φ a S R a + R 2
18 peano2re a a + 1
19 14 18 syl φ a S a + 1
20 19 adantr φ a S ¬ R a + 1
21 17 20 ifclda φ a S if R a + R 2 a + 1
22 6 21 eqeltrid φ a S M
23 0re 0
24 23 a1i φ a S 0
25 13 absge0d φ a S 0 a
26 breq2 a + R 2 = if R a + R 2 a + 1 a < a + R 2 a < if R a + R 2 a + 1
27 breq2 a + 1 = if R a + R 2 a + 1 a < a + 1 a < if R a + R 2 a + 1
28 simpr φ a S a S
29 28 5 eleqtrdi φ a S a abs -1 0 R
30 ffn abs : abs Fn
31 elpreima abs Fn a abs -1 0 R a a 0 R
32 8 30 31 mp2b a abs -1 0 R a a 0 R
33 29 32 sylib φ a S a a 0 R
34 33 simprd φ a S a 0 R
35 iccssxr 0 +∞ *
36 1 3 4 radcnvcl φ R 0 +∞
37 36 adantr φ a S R 0 +∞
38 35 37 sselid φ a S R *
39 elico2 0 R * a 0 R a 0 a a < R
40 23 38 39 sylancr φ a S a 0 R a 0 a a < R
41 34 40 mpbid φ a S a 0 a a < R
42 41 simp3d φ a S a < R
43 42 adantr φ a S R a < R
44 avglt1 a R a < R a < a + R 2
45 14 44 sylan φ a S R a < R a < a + R 2
46 43 45 mpbid φ a S R a < a + R 2
47 14 ltp1d φ a S a < a + 1
48 47 adantr φ a S ¬ R a < a + 1
49 26 27 46 48 ifbothda φ a S a < if R a + R 2 a + 1
50 49 6 breqtrrdi φ a S a < M
51 24 14 22 25 50 lelttrd φ a S 0 < M
52 22 51 elrpd φ a S M +
53 breq1 a + R 2 = if R a + R 2 a + 1 a + R 2 < R if R a + R 2 a + 1 < R
54 breq1 a + 1 = if R a + R 2 a + 1 a + 1 < R if R a + R 2 a + 1 < R
55 avglt2 a R a < R a + R 2 < R
56 14 55 sylan φ a S R a < R a + R 2 < R
57 43 56 mpbid φ a S R a + R 2 < R
58 19 rexrd φ a S a + 1 *
59 38 58 xrlenltd φ a S R a + 1 ¬ a + 1 < R
60 0xr 0 *
61 pnfxr +∞ *
62 elicc1 0 * +∞ * R 0 +∞ R * 0 R R +∞
63 60 61 62 mp2an R 0 +∞ R * 0 R R +∞
64 36 63 sylib φ R * 0 R R +∞
65 64 simp2d φ 0 R
66 65 adantr φ a S 0 R
67 ge0gtmnf R * 0 R −∞ < R
68 38 66 67 syl2anc φ a S −∞ < R
69 xrre R * a + 1 −∞ < R R a + 1 R
70 69 expr R * a + 1 −∞ < R R a + 1 R
71 38 19 68 70 syl21anc φ a S R a + 1 R
72 59 71 sylbird φ a S ¬ a + 1 < R R
73 72 con1d φ a S ¬ R a + 1 < R
74 73 imp φ a S ¬ R a + 1 < R
75 53 54 57 74 ifbothda φ a S if R a + R 2 a + 1 < R
76 6 75 eqbrtrid φ a S M < R
77 52 50 76 3jca φ a S M + a < M M < R