Metamath Proof Explorer


Theorem logtayllem

Description: Lemma for logtayl . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion logtayllem
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
2 1nn0
 |-  1 e. NN0
3 2 a1i
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. NN0 )
4 oveq2
 |-  ( n = k -> ( ( abs ` A ) ^ n ) = ( ( abs ` A ) ^ k ) )
5 eqid
 |-  ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) = ( n e. NN0 |-> ( ( abs ` A ) ^ n ) )
6 ovex
 |-  ( ( abs ` A ) ^ k ) e. _V
7 4 5 6 fvmpt
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) )
8 7 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) )
9 abscl
 |-  ( A e. CC -> ( abs ` A ) e. RR )
10 9 adantr
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. RR )
11 reexpcl
 |-  ( ( ( abs ` A ) e. RR /\ k e. NN0 ) -> ( ( abs ` A ) ^ k ) e. RR )
12 10 11 sylan
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( abs ` A ) ^ k ) e. RR )
13 8 12 eqeltrd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) e. RR )
14 eqeq1
 |-  ( n = k -> ( n = 0 <-> k = 0 ) )
15 oveq2
 |-  ( n = k -> ( 1 / n ) = ( 1 / k ) )
16 14 15 ifbieq2d
 |-  ( n = k -> if ( n = 0 , 0 , ( 1 / n ) ) = if ( k = 0 , 0 , ( 1 / k ) ) )
17 oveq2
 |-  ( n = k -> ( A ^ n ) = ( A ^ k ) )
18 16 17 oveq12d
 |-  ( n = k -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) = ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) )
19 eqid
 |-  ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) = ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) )
20 ovex
 |-  ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) e. _V
21 18 19 20 fvmpt
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) = ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) )
22 21 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) = ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) )
23 0cnd
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ k = 0 ) -> 0 e. CC )
24 nn0cn
 |-  ( k e. NN0 -> k e. CC )
25 24 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> k e. CC )
26 neqne
 |-  ( -. k = 0 -> k =/= 0 )
27 reccl
 |-  ( ( k e. CC /\ k =/= 0 ) -> ( 1 / k ) e. CC )
28 25 26 27 syl2an
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ -. k = 0 ) -> ( 1 / k ) e. CC )
29 23 28 ifclda
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> if ( k = 0 , 0 , ( 1 / k ) ) e. CC )
30 expcl
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
31 30 adantlr
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( A ^ k ) e. CC )
32 29 31 mulcld
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) e. CC )
33 22 32 eqeltrd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) e. CC )
34 10 recnd
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. CC )
35 absidm
 |-  ( A e. CC -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )
36 35 adantr
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( abs ` A ) ) = ( abs ` A ) )
37 simpr
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
38 36 37 eqbrtrd
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( abs ` A ) ) < 1 )
39 34 38 8 geolim
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) ~~> ( 1 / ( 1 - ( abs ` A ) ) ) )
40 seqex
 |-  seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) e. _V
41 ovex
 |-  ( 1 / ( 1 - ( abs ` A ) ) ) e. _V
42 40 41 breldm
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) ~~> ( 1 / ( 1 - ( abs ` A ) ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) e. dom ~~> )
43 39 42 syl
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) e. dom ~~> )
44 1red
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. RR )
45 elnnuz
 |-  ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
46 nnrecre
 |-  ( k e. NN -> ( 1 / k ) e. RR )
47 46 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) e. RR )
48 47 recnd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) e. CC )
49 nnnn0
 |-  ( k e. NN -> k e. NN0 )
50 49 31 sylan2
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( A ^ k ) e. CC )
51 48 50 absmuld
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( 1 / k ) x. ( A ^ k ) ) ) = ( ( abs ` ( 1 / k ) ) x. ( abs ` ( A ^ k ) ) ) )
52 nnrp
 |-  ( k e. NN -> k e. RR+ )
53 52 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k e. RR+ )
54 53 rpreccld
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) e. RR+ )
55 54 rpge0d
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 <_ ( 1 / k ) )
56 47 55 absidd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( 1 / k ) ) = ( 1 / k ) )
57 simpl
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
58 absexp
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) )
59 57 49 58 syl2an
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) )
60 56 59 oveq12d
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( abs ` ( 1 / k ) ) x. ( abs ` ( A ^ k ) ) ) = ( ( 1 / k ) x. ( ( abs ` A ) ^ k ) ) )
61 51 60 eqtrd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( 1 / k ) x. ( A ^ k ) ) ) = ( ( 1 / k ) x. ( ( abs ` A ) ^ k ) ) )
62 1red
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 1 e. RR )
63 49 12 sylan2
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( abs ` A ) ^ k ) e. RR )
64 50 absge0d
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 <_ ( abs ` ( A ^ k ) ) )
65 64 59 breqtrd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 <_ ( ( abs ` A ) ^ k ) )
66 nnge1
 |-  ( k e. NN -> 1 <_ k )
67 66 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 1 <_ k )
68 0lt1
 |-  0 < 1
69 68 a1i
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 < 1 )
70 nnre
 |-  ( k e. NN -> k e. RR )
71 70 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k e. RR )
72 nngt0
 |-  ( k e. NN -> 0 < k )
73 72 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 < k )
74 lerec
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( k e. RR /\ 0 < k ) ) -> ( 1 <_ k <-> ( 1 / k ) <_ ( 1 / 1 ) ) )
75 62 69 71 73 74 syl22anc
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 <_ k <-> ( 1 / k ) <_ ( 1 / 1 ) ) )
76 67 75 mpbid
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) <_ ( 1 / 1 ) )
77 1div1e1
 |-  ( 1 / 1 ) = 1
78 76 77 breqtrdi
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) <_ 1 )
79 47 62 63 65 78 lemul1ad
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( 1 / k ) x. ( ( abs ` A ) ^ k ) ) <_ ( 1 x. ( ( abs ` A ) ^ k ) ) )
80 61 79 eqbrtrd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( 1 / k ) x. ( A ^ k ) ) ) <_ ( 1 x. ( ( abs ` A ) ^ k ) ) )
81 49 22 sylan2
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) = ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) )
82 nnne0
 |-  ( k e. NN -> k =/= 0 )
83 82 adantl
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k =/= 0 )
84 83 neneqd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> -. k = 0 )
85 84 iffalsed
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> if ( k = 0 , 0 , ( 1 / k ) ) = ( 1 / k ) )
86 85 oveq1d
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( ( 1 / k ) x. ( A ^ k ) ) )
87 81 86 eqtrd
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) = ( ( 1 / k ) x. ( A ^ k ) ) )
88 87 fveq2d
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) ) = ( abs ` ( ( 1 / k ) x. ( A ^ k ) ) ) )
89 49 8 sylan2
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) )
90 89 oveq2d
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 x. ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) ) = ( 1 x. ( ( abs ` A ) ^ k ) ) )
91 80 88 90 3brtr4d
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) ) <_ ( 1 x. ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) ) )
92 45 91 sylan2br
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) ) <_ ( 1 x. ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) ) )
93 1 3 13 33 43 44 92 cvgcmpce
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ) e. dom ~~> )