Metamath Proof Explorer

Theorem aaliou3lem3

Description: Lemma for aaliou3 . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses aaliou3lem.a ⊢ 𝐺 = ( 𝑐 ∈ ( ℤ≥ ‘ 𝐴 ) ↦ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) )
aaliou3lem.b ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
Assertion aaliou3lem3 ( 𝐴 ∈ ℕ → ( seq 𝐴 ( + , 𝐹 ) ∈ dom ⇝ ∧ Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aaliou3lem.a ⊢ 𝐺 = ( 𝑐 ∈ ( ℤ≥ ‘ 𝐴 ) ↦ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · ( ( 1 / 2 ) ↑ ( 𝑐 − 𝐴 ) ) ) )
2 aaliou3lem.b ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑎 ) ) )
3 eqid ⊢ ( ℤ≥ ‘ 𝐴 ) = ( ℤ≥ ‘ 𝐴 )
4 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
5 uzid ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) )
6 4 5 syl ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( ℤ≥ ‘ 𝐴 ) )
7 1 aaliou3lem1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝑏 ) ∈ ℝ )
8 1 2 aaliou3lem2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ( 0 (,] ( 𝐺 ‘ 𝑏 ) ) )
9 0xr ⊢ 0 ∈ ℝ*
10 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ ( 𝐺 ‘ 𝑏 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑏 ) ∈ ( 0 (,] ( 𝐺 ‘ 𝑏 ) ) ↔ ( ( 𝐹 ‘ 𝑏 ) ∈ ℝ ∧ 0 < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ) ) )
11 9 7 10 sylancr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑏 ) ∈ ( 0 (,] ( 𝐺 ‘ 𝑏 ) ) ↔ ( ( 𝐹 ‘ 𝑏 ) ∈ ℝ ∧ 0 < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ) ) )
12 8 11 mpbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑏 ) ∈ ℝ ∧ 0 < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) ) )
13 12 simp1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℝ )
14 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
15 14 a1i ⊢ ( 𝐴 ∈ ℕ → ( 1 / 2 ) ∈ ℂ )
16 halfre ⊢ ( 1 / 2 ) ∈ ℝ
17 halfgt0 ⊢ 0 < ( 1 / 2 )
18 16 17 elrpii ⊢ ( 1 / 2 ) ∈ ℝ+
19 rprege0 ⊢ ( ( 1 / 2 ) ∈ ℝ+ → ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ) )
20 absid ⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ 0 ≤ ( 1 / 2 ) ) → ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 ) )
21 18 19 20 mp2b ⊢ ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 )
22 halflt1 ⊢ ( 1 / 2 ) < 1
23 21 22 eqbrtri ⊢ ( abs ‘ ( 1 / 2 ) ) < 1
24 23 a1i ⊢ ( 𝐴 ∈ ℕ → ( abs ‘ ( 1 / 2 ) ) < 1 )
25 2rp ⊢ 2 ∈ ℝ+
26 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
27 26 faccld ⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) ∈ ℕ )
28 27 nnzd ⊢ ( 𝐴 ∈ ℕ → ( ! ‘ 𝐴 ) ∈ ℤ )
29 28 znegcld ⊢ ( 𝐴 ∈ ℕ → - ( ! ‘ 𝐴 ) ∈ ℤ )
30 rpexpcl ⊢ ( ( 2 ∈ ℝ+ ∧ - ( ! ‘ 𝐴 ) ∈ ℤ ) → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
31 25 29 30 sylancr ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℝ+ )
32 31 rpcnd ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℂ )
33 4 15 24 32 1 geolim3 ⊢ ( 𝐴 ∈ ℕ → seq 𝐴 ( + , 𝐺 ) ⇝ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 − ( 1 / 2 ) ) ) )
34 seqex ⊢ seq 𝐴 ( + , 𝐺 ) ∈ V
35 ovex ⊢ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 − ( 1 / 2 ) ) ) ∈ V
36 34 35 breldm ⊢ ( seq 𝐴 ( + , 𝐺 ) ⇝ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 − ( 1 / 2 ) ) ) → seq 𝐴 ( + , 𝐺 ) ∈ dom ⇝ )
37 33 36 syl ⊢ ( 𝐴 ∈ ℕ → seq 𝐴 ( + , 𝐺 ) ∈ dom ⇝ )
38 12 simp2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 0 < ( 𝐹 ‘ 𝑏 ) )
39 13 38 elrpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ℝ+ )
40 39 rpge0d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 0 ≤ ( 𝐹 ‘ 𝑏 ) )
41 12 simp3d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) ≤ ( 𝐺 ‘ 𝑏 ) )
42 3 6 7 13 37 40 41 cvgcmp ⊢ ( 𝐴 ∈ ℕ → seq 𝐴 ( + , 𝐹 ) ∈ dom ⇝ )
43 eqidd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
44 3 3 6 43 39 42 isumrpcl ⊢ ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ+ )
45 eqidd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) )
46 3 4 43 13 45 7 41 42 37 isumle ⊢ ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ≤ Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐺 ‘ 𝑏 ) )
47 7 recnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐺 ‘ 𝑏 ) ∈ ℂ )
48 3 4 45 47 33 isumclim ⊢ ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐺 ‘ 𝑏 ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 − ( 1 / 2 ) ) ) )
49 1mhlfehlf ⊢ ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
50 49 oveq2i ⊢ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 − ( 1 / 2 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 / 2 ) )
51 2cn ⊢ 2 ∈ ℂ
52 mulcl ⊢ ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) ∈ ℂ )
53 32 51 52 sylancl ⊢ ( 𝐴 ∈ ℕ → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) ∈ ℂ )
54 53 div1d ⊢ ( 𝐴 ∈ ℕ → ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) / 1 ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) )
55 1rp ⊢ 1 ∈ ℝ+
56 rpcnne0 ⊢ ( 1 ∈ ℝ+ → ( 1 ∈ ℂ ∧ 1 ≠ 0 ) )
57 55 56 ax-mp ⊢ ( 1 ∈ ℂ ∧ 1 ≠ 0 )
58 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
59 divdiv2 ⊢ ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℂ ∧ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 / 2 ) ) = ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) / 1 ) )
60 57 58 59 mp3an23 ⊢ ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℂ → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 / 2 ) ) = ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) / 1 ) )
61 32 60 syl ⊢ ( 𝐴 ∈ ℕ → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 / 2 ) ) = ( ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) / 1 ) )
62 mulcom ⊢ ( ( 2 ∈ ℂ ∧ ( 2 ↑ - ( ! ‘ 𝐴 ) ) ∈ ℂ ) → ( 2 · ( 2 ↑ - ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) )
63 51 32 62 sylancr ⊢ ( 𝐴 ∈ ℕ → ( 2 · ( 2 ↑ - ( ! ‘ 𝐴 ) ) ) = ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) · 2 ) )
64 54 61 63 3eqtr4d ⊢ ( 𝐴 ∈ ℕ → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 / 2 ) ) = ( 2 · ( 2 ↑ - ( ! ‘ 𝐴 ) ) ) )
65 50 64 syl5eq ⊢ ( 𝐴 ∈ ℕ → ( ( 2 ↑ - ( ! ‘ 𝐴 ) ) / ( 1 − ( 1 / 2 ) ) ) = ( 2 · ( 2 ↑ - ( ! ‘ 𝐴 ) ) ) )
66 48 65 eqtrd ⊢ ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐺 ‘ 𝑏 ) = ( 2 · ( 2 ↑ - ( ! ‘ 𝐴 ) ) ) )
67 46 66 breqtrd ⊢ ( 𝐴 ∈ ℕ → Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ 𝐴 ) ) ) )
68 42 44 67 3jca ⊢ ( 𝐴 ∈ ℕ → ( seq 𝐴 ( + , 𝐹 ) ∈ dom ⇝ ∧ Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ∈ ℝ+ ∧ Σ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ≤ ( 2 · ( 2 ↑ - ( ! ‘ 𝐴 ) ) ) ) )