Mathbox for Steve Rodriguez < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  binomcxplemfrat Structured version   Visualization version   Unicode version

Theorem binomcxplemfrat 36770
 Description: Lemma for binomcxp 36776. binomcxplemrat 36769 implies that when is not a nonnegative integer, the absolute value of the ratio converges to one. The rest of equation "Since continuity of the absolute value..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
Hypotheses
Ref Expression
binomcxp.a
binomcxp.b
binomcxp.lt
binomcxp.c
binomcxplem.f C𝑐
Assertion
Ref Expression
binomcxplemfrat
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem binomcxplemfrat
StepHypRef Expression
1 binomcxp.c . . . . . . . . . 10
21adantr 472 . . . . . . . . 9
3 simpr 468 . . . . . . . . 9
42, 3bccp1k 36760 . . . . . . . 8 C𝑐 C𝑐
5 binomcxplem.f . . . . . . . . . 10 C𝑐
65a1i 11 . . . . . . . . 9 C𝑐
7 simpr 468 . . . . . . . . . 10
87oveq2d 6324 . . . . . . . . 9 C𝑐 C𝑐
9 1nn0 10909 . . . . . . . . . . 11
109a1i 11 . . . . . . . . . 10
113, 10nn0addcld 10953 . . . . . . . . 9
12 ovex 6336 . . . . . . . . . 10 C𝑐
1312a1i 11 . . . . . . . . 9 C𝑐
146, 8, 11, 13fvmptd 5969 . . . . . . . 8 C𝑐
15 simpr 468 . . . . . . . . . . 11
1615oveq2d 6324 . . . . . . . . . 10 C𝑐 C𝑐
17 ovex 6336 . . . . . . . . . . 11 C𝑐
1817a1i 11 . . . . . . . . . 10 C𝑐
196, 16, 3, 18fvmptd 5969 . . . . . . . . 9 C𝑐
2019oveq1d 6323 . . . . . . . 8 C𝑐
214, 14, 203eqtr4d 2515 . . . . . . 7
2221adantlr 729 . . . . . 6
2322eqcomd 2477 . . . . 5
242, 3bcccl 36758 . . . . . . . . . 10 C𝑐
2519, 24eqeltrd 2549 . . . . . . . . 9
2625adantlr 729 . . . . . . . 8
272adantlr 729 . . . . . . . . . 10
28 simpr 468 . . . . . . . . . . 11
2928nn0cnd 10951 . . . . . . . . . 10
3027, 29subcld 10005 . . . . . . . . 9
31 1cnd 9677 . . . . . . . . . 10
3229, 31addcld 9680 . . . . . . . . 9
33 nn0p1nn 10933 . . . . . . . . . . 11
3433nnne0d 10676 . . . . . . . . . 10
3534adantl 473 . . . . . . . . 9
3630, 32, 35divcld 10405 . . . . . . . 8
3726, 36mulcld 9681 . . . . . . 7
3822, 37eqeltrd 2549 . . . . . 6
3919adantlr 729 . . . . . . 7 C𝑐
40 elfznn0 11913 . . . . . . . . . 10
4140con3i 142 . . . . . . . . 9
4241ad2antlr 741 . . . . . . . 8
4327, 28bcc0 36759 . . . . . . . . 9 C𝑐
4443necon3abid 2679 . . . . . . . 8 C𝑐
4542, 44mpbird 240 . . . . . . 7 C𝑐
4639, 45eqnetrd 2710 . . . . . 6
4738, 26, 36, 46divmuld 10427 . . . . 5
4823, 47mpbird 240 . . . 4
4948fveq2d 5883 . . 3
5049mpteq2dva 4482 . 2
51 binomcxp.a . . . 4
52 binomcxp.b . . . 4
53 binomcxp.lt . . . 4
5451, 52, 53, 1binomcxplemrat 36769 . . 3