Metamath Proof Explorer


Theorem binomcxplemrat

Description: Lemma for binomcxp . As k increases, this ratio's absolute value converges to one. Part of equation "Since continuity of the absolute value..." in the Wikibooks proof (proven for the inverse ratio, which we later show is no problem). (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses binomcxp.a φA+
binomcxp.b φB
binomcxp.lt φB<A
binomcxp.c φC
Assertion binomcxplemrat φk0Ckk+11

Proof

Step Hyp Ref Expression
1 binomcxp.a φA+
2 binomcxp.b φB
3 binomcxp.lt φB<A
4 binomcxp.c φC
5 nn0uz 0=0
6 0zd φ0
7 peano2cn CC+1
8 4 7 syl φC+1
9 1zzd φ1
10 nn0ex 0V
11 10 mptex k0C+1k+1V
12 11 a1i φk0C+1k+1V
13 eqidd φx0k0C+1k+1=k0C+1k+1
14 simpr φx0k=xk=x
15 14 oveq1d φx0k=xk+1=x+1
16 15 oveq2d φx0k=xC+1k+1=C+1x+1
17 simpr φx0x0
18 ovexd φx0C+1x+1V
19 13 16 17 18 fvmptd φx0k0C+1k+1x=C+1x+1
20 5 6 8 9 12 19 divcnvshft φk0C+1k+10
21 ovexd φk0C+1k+1fk0k+1k+1V
22 nn0cn k0k
23 1cnd k01
24 22 23 addcld k0k+1
25 nn0p1nn k0k+1
26 25 nnne0d k0k+10
27 24 26 dividd k0k+1k+1=1
28 27 mpteq2ia k0k+1k+1=k01
29 fconstmpt 0×1=k01
30 28 29 eqtr4i k0k+1k+1=0×1
31 ax-1cn 1
32 0z 0
33 5 eqimss2i 00
34 33 10 climconst2 100×11
35 31 32 34 mp2an 0×11
36 30 35 eqbrtri k0k+1k+11
37 36 a1i φk0k+1k+11
38 4 adantr φx0C
39 1cnd φx01
40 38 39 addcld φx0C+1
41 17 nn0cnd φx0x
42 41 39 addcld φx0x+1
43 nn0p1nn x0x+1
44 43 nnne0d x0x+10
45 44 adantl φx0x+10
46 40 42 45 divcld φx0C+1x+1
47 19 46 eqeltrd φx0k0C+1k+1x
48 eqidd φx0k0k+1k+1=k0k+1k+1
49 15 15 oveq12d φx0k=xk+1k+1=x+1x+1
50 ovexd φx0x+1x+1V
51 48 49 17 50 fvmptd φx0k0k+1k+1x=x+1x+1
52 42 42 45 divcld φx0x+1x+1
53 51 52 eqeltrd φx0k0k+1k+1x
54 ovex C+1k+1V
55 eqid k0C+1k+1=k0C+1k+1
56 54 55 fnmpti k0C+1k+1Fn0
57 56 a1i φk0C+1k+1Fn0
58 ovex k+1k+1V
59 eqid k0k+1k+1=k0k+1k+1
60 58 59 fnmpti k0k+1k+1Fn0
61 60 a1i φk0k+1k+1Fn0
62 10 a1i φ0V
63 inidm 00=0
64 eqidd φx0k0C+1k+1x=k0C+1k+1x
65 eqidd φx0k0k+1k+1x=k0k+1k+1x
66 57 61 62 62 63 64 65 ofval φx0k0C+1k+1fk0k+1k+1x=k0C+1k+1xk0k+1k+1x
67 5 6 20 21 37 47 53 66 climsub φk0C+1k+1fk0k+1k+101
68 ovexd φk0C+1k+1V
69 ovexd φk0k+1k+1V
70 eqidd φk0C+1k+1=k0C+1k+1
71 eqidd φk0k+1k+1=k0k+1k+1
72 62 68 69 70 71 offval2 φk0C+1k+1fk0k+1k+1=k0C+1k+1k+1k+1
73 8 adantr φk0C+1
74 24 adantl φk0k+1
75 26 adantl φk0k+10
76 73 74 74 75 divsubdird φk0C+1-k+1k+1=C+1k+1k+1k+1
77 4 adantr φk0C
78 22 adantl φk0k
79 1cnd φk01
80 77 78 79 pnpcan2d φk0C+1-k+1=Ck
81 80 oveq1d φk0C+1-k+1k+1=Ckk+1
82 76 81 eqtr3d φk0C+1k+1k+1k+1=Ckk+1
83 82 mpteq2dva φk0C+1k+1k+1k+1=k0Ckk+1
84 72 83 eqtrd φk0C+1k+1fk0k+1k+1=k0Ckk+1
85 df-neg 1=01
86 85 eqcomi 01=1
87 86 a1i φ01=1
88 67 84 87 3brtr3d φk0Ckk+1-1
89 10 mptex k0Ckk+1V
90 89 a1i φk0Ckk+1V
91 eqidd φx0k0Ckk+1=k0Ckk+1
92 oveq2 k=xCk=Cx
93 oveq1 k=xk+1=x+1
94 92 93 oveq12d k=xCkk+1=Cxx+1
95 94 adantl φx0k=xCkk+1=Cxx+1
96 ovexd φx0Cxx+1V
97 91 95 17 96 fvmptd φx0k0Ckk+1x=Cxx+1
98 38 41 subcld φx0Cx
99 98 42 45 divcld φx0Cxx+1
100 97 99 eqeltrd φx0k0Ckk+1x
101 eqidd φx0k0Ckk+1=k0Ckk+1
102 94 fveq2d k=xCkk+1=Cxx+1
103 102 adantl φx0k=xCkk+1=Cxx+1
104 fvexd φx0Cxx+1V
105 101 103 17 104 fvmptd φx0k0Ckk+1x=Cxx+1
106 97 fveq2d φx0k0Ckk+1x=Cxx+1
107 105 106 eqtr4d φx0k0Ckk+1x=k0Ckk+1x
108 5 88 90 6 100 107 climabs φk0Ckk+11
109 31 absnegi 1=1
110 abs1 1=1
111 109 110 eqtri 1=1
112 108 111 breqtrdi φk0Ckk+11