Metamath Proof Explorer


Theorem psercnlem1

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

Ref Expression
Hypotheses pserf.g 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) ) )
pserf.f 𝐹 = ( 𝑦𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺𝑦 ) ‘ 𝑗 ) )
pserf.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
pserf.r 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
psercn.s 𝑆 = ( abs “ ( 0 [,) 𝑅 ) )
psercn.m 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) )
Assertion psercnlem1 ( ( 𝜑𝑎𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀𝑀 < 𝑅 ) )

Proof

Step Hyp Ref Expression
1 pserf.g 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) ) )
2 pserf.f 𝐹 = ( 𝑦𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺𝑦 ) ‘ 𝑗 ) )
3 pserf.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
4 pserf.r 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
5 psercn.s 𝑆 = ( abs “ ( 0 [,) 𝑅 ) )
6 psercn.m 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) )
7 cnvimass ( abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
8 absf abs : ℂ ⟶ ℝ
9 8 fdmi dom abs = ℂ
10 7 9 sseqtri ( abs “ ( 0 [,) 𝑅 ) ) ⊆ ℂ
11 5 10 eqsstri 𝑆 ⊆ ℂ
12 11 a1i ( 𝜑𝑆 ⊆ ℂ )
13 12 sselda ( ( 𝜑𝑎𝑆 ) → 𝑎 ∈ ℂ )
14 13 abscld ( ( 𝜑𝑎𝑆 ) → ( abs ‘ 𝑎 ) ∈ ℝ )
15 readdcl ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) + 𝑅 ) ∈ ℝ )
16 14 15 sylan ( ( ( 𝜑𝑎𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) + 𝑅 ) ∈ ℝ )
17 16 rehalfcld ( ( ( 𝜑𝑎𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ∈ ℝ )
18 peano2re ( ( abs ‘ 𝑎 ) ∈ ℝ → ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ )
19 14 18 syl ( ( 𝜑𝑎𝑆 ) → ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ )
20 19 adantr ( ( ( 𝜑𝑎𝑆 ) ∧ ¬ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ )
21 17 20 ifclda ( ( 𝜑𝑎𝑆 ) → if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) ∈ ℝ )
22 6 21 eqeltrid ( ( 𝜑𝑎𝑆 ) → 𝑀 ∈ ℝ )
23 0re 0 ∈ ℝ
24 23 a1i ( ( 𝜑𝑎𝑆 ) → 0 ∈ ℝ )
25 13 absge0d ( ( 𝜑𝑎𝑆 ) → 0 ≤ ( abs ‘ 𝑎 ) )
26 breq2 ( ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ↔ ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) ) )
27 breq2 ( ( ( abs ‘ 𝑎 ) + 1 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) ↔ ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) ) )
28 simpr ( ( 𝜑𝑎𝑆 ) → 𝑎𝑆 )
29 28 5 eleqtrdi ( ( 𝜑𝑎𝑆 ) → 𝑎 ∈ ( abs “ ( 0 [,) 𝑅 ) ) )
30 ffn ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
31 elpreima ( abs Fn ℂ → ( 𝑎 ∈ ( abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) ) )
32 8 30 31 mp2b ( 𝑎 ∈ ( abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) )
33 29 32 sylib ( ( 𝜑𝑎𝑆 ) → ( 𝑎 ∈ ℂ ∧ ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ) )
34 33 simprd ( ( 𝜑𝑎𝑆 ) → ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) )
35 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
36 1 3 4 radcnvcl ( 𝜑𝑅 ∈ ( 0 [,] +∞ ) )
37 36 adantr ( ( 𝜑𝑎𝑆 ) → 𝑅 ∈ ( 0 [,] +∞ ) )
38 35 37 sselid ( ( 𝜑𝑎𝑆 ) → 𝑅 ∈ ℝ* )
39 elico2 ( ( 0 ∈ ℝ ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) ) )
40 23 38 39 sylancr ( ( 𝜑𝑎𝑆 ) → ( ( abs ‘ 𝑎 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) ) )
41 34 40 mpbid ( ( 𝜑𝑎𝑆 ) → ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑎 ) ∧ ( abs ‘ 𝑎 ) < 𝑅 ) )
42 41 simp3d ( ( 𝜑𝑎𝑆 ) → ( abs ‘ 𝑎 ) < 𝑅 )
43 42 adantr ( ( ( 𝜑𝑎𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < 𝑅 )
44 avglt1 ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ) )
45 14 44 sylan ( ( ( 𝜑𝑎𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) ) )
46 43 45 mpbid ( ( ( 𝜑𝑎𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) )
47 14 ltp1d ( ( 𝜑𝑎𝑆 ) → ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) )
48 47 adantr ( ( ( 𝜑𝑎𝑆 ) ∧ ¬ 𝑅 ∈ ℝ ) → ( abs ‘ 𝑎 ) < ( ( abs ‘ 𝑎 ) + 1 ) )
49 26 27 46 48 ifbothda ( ( 𝜑𝑎𝑆 ) → ( abs ‘ 𝑎 ) < if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) )
50 49 6 breqtrrdi ( ( 𝜑𝑎𝑆 ) → ( abs ‘ 𝑎 ) < 𝑀 )
51 24 14 22 25 50 lelttrd ( ( 𝜑𝑎𝑆 ) → 0 < 𝑀 )
52 22 51 elrpd ( ( 𝜑𝑎𝑆 ) → 𝑀 ∈ ℝ+ )
53 breq1 ( ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) < 𝑅 ↔ if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) < 𝑅 ) )
54 breq1 ( ( ( abs ‘ 𝑎 ) + 1 ) = if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) → ( ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 ↔ if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) < 𝑅 ) )
55 avglt2 ( ( ( abs ‘ 𝑎 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) < 𝑅 ) )
56 14 55 sylan ( ( ( 𝜑𝑎𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) < 𝑅 ↔ ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) < 𝑅 ) )
57 43 56 mpbid ( ( ( 𝜑𝑎𝑆 ) ∧ 𝑅 ∈ ℝ ) → ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) < 𝑅 )
58 19 rexrd ( ( 𝜑𝑎𝑆 ) → ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ* )
59 38 58 xrlenltd ( ( 𝜑𝑎𝑆 ) → ( 𝑅 ≤ ( ( abs ‘ 𝑎 ) + 1 ) ↔ ¬ ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 ) )
60 0xr 0 ∈ ℝ*
61 pnfxr +∞ ∈ ℝ*
62 elicc1 ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞ ) ) )
63 60 61 62 mp2an ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞ ) )
64 36 63 sylib ( 𝜑 → ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅𝑅 ≤ +∞ ) )
65 64 simp2d ( 𝜑 → 0 ≤ 𝑅 )
66 65 adantr ( ( 𝜑𝑎𝑆 ) → 0 ≤ 𝑅 )
67 ge0gtmnf ( ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ) → -∞ < 𝑅 )
68 38 66 67 syl2anc ( ( 𝜑𝑎𝑆 ) → -∞ < 𝑅 )
69 xrre ( ( ( 𝑅 ∈ ℝ* ∧ ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ ) ∧ ( -∞ < 𝑅𝑅 ≤ ( ( abs ‘ 𝑎 ) + 1 ) ) ) → 𝑅 ∈ ℝ )
70 69 expr ( ( ( 𝑅 ∈ ℝ* ∧ ( ( abs ‘ 𝑎 ) + 1 ) ∈ ℝ ) ∧ -∞ < 𝑅 ) → ( 𝑅 ≤ ( ( abs ‘ 𝑎 ) + 1 ) → 𝑅 ∈ ℝ ) )
71 38 19 68 70 syl21anc ( ( 𝜑𝑎𝑆 ) → ( 𝑅 ≤ ( ( abs ‘ 𝑎 ) + 1 ) → 𝑅 ∈ ℝ ) )
72 59 71 sylbird ( ( 𝜑𝑎𝑆 ) → ( ¬ ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅𝑅 ∈ ℝ ) )
73 72 con1d ( ( 𝜑𝑎𝑆 ) → ( ¬ 𝑅 ∈ ℝ → ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 ) )
74 73 imp ( ( ( 𝜑𝑎𝑆 ) ∧ ¬ 𝑅 ∈ ℝ ) → ( ( abs ‘ 𝑎 ) + 1 ) < 𝑅 )
75 53 54 57 74 ifbothda ( ( 𝜑𝑎𝑆 ) → if ( 𝑅 ∈ ℝ , ( ( ( abs ‘ 𝑎 ) + 𝑅 ) / 2 ) , ( ( abs ‘ 𝑎 ) + 1 ) ) < 𝑅 )
76 6 75 eqbrtrid ( ( 𝜑𝑎𝑆 ) → 𝑀 < 𝑅 )
77 52 50 76 3jca ( ( 𝜑𝑎𝑆 ) → ( 𝑀 ∈ ℝ+ ∧ ( abs ‘ 𝑎 ) < 𝑀𝑀 < 𝑅 ) )