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 ~~> )