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 sseldi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑅 ∈ ℝ* )
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 ‘ 𝑎 ) < 𝑀 ∧ 𝑀 < 𝑅 ) )