Metamath Proof Explorer


Theorem pserdvlem1

Description: Lemma for pserdv . (Contributed by Mario Carneiro, 7-May-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 pserdvlem1 φ a S a + M 2 + a < a + M 2 a + M 2 < 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 1 2 3 4 5 6 psercnlem1 φ a S M + a < M M < R
16 15 simp1d φ a S M +
17 16 rpred φ a S M
18 14 17 readdcld φ a S a + M
19 0red φ a S 0
20 13 absge0d φ a S 0 a
21 14 16 ltaddrpd φ a S a < a + M
22 19 14 18 20 21 lelttrd φ a S 0 < a + M
23 18 22 elrpd φ a S a + M +
24 23 rphalfcld φ a S a + M 2 +
25 15 simp2d φ a S a < M
26 avglt1 a M a < M a < a + M 2
27 14 17 26 syl2anc φ a S a < M a < a + M 2
28 25 27 mpbid φ a S a < a + M 2
29 18 rehalfcld φ a S a + M 2
30 29 rexrd φ a S a + M 2 *
31 17 rexrd φ a S M *
32 iccssxr 0 +∞ *
33 1 3 4 radcnvcl φ R 0 +∞
34 32 33 sseldi φ R *
35 34 adantr φ a S R *
36 avglt2 a M a < M a + M 2 < M
37 14 17 36 syl2anc φ a S a < M a + M 2 < M
38 25 37 mpbid φ a S a + M 2 < M
39 15 simp3d φ a S M < R
40 30 31 35 38 39 xrlttrd φ a S a + M 2 < R
41 24 28 40 3jca φ a S a + M 2 + a < a + M 2 a + M 2 < R