Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  climrlim2 Structured version   Unicode version

Theorem climrlim2 12331
 Description: Produce a real limit from an integer limit, where the real function is only dependent on the integer part of . (Contributed by Mario Carneiro, 2-May-2016.)
Hypotheses
Ref Expression
climrlim2.1
climrlim2.2
climrlim2.3
climrlim2.4
climrlim2.5
climrlim2.6
climrlim2.7
Assertion
Ref Expression
climrlim2
Distinct variable groups:   ,   ,   ,   ,   ,,   ,,
Allowed substitution hints:   ()   ()   ()   ()   (,)

Proof of Theorem climrlim2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 climrlim2.5 . 2
2 eluzelz 10486 . . . . . . . . . . . . . . . 16
3 climrlim2.1 . . . . . . . . . . . . . . . 16
42, 3eleq2s 2527 . . . . . . . . . . . . . . 15
54ad2antlr 708 . . . . . . . . . . . . . 14
6 climrlim2.3 . . . . . . . . . . . . . . . . . 18
76sselda 3340 . . . . . . . . . . . . . . . . 17
87flcld 11197 . . . . . . . . . . . . . . . 16
98adantlr 696 . . . . . . . . . . . . . . 15
109ad2ant2r 728 . . . . . . . . . . . . . 14
11 simprr 734 . . . . . . . . . . . . . . 15
127adantlr 696 . . . . . . . . . . . . . . . . 17
1312ad2ant2r 728 . . . . . . . . . . . . . . . 16
14 flge 11204 . . . . . . . . . . . . . . . 16
1513, 5, 14syl2anc 643 . . . . . . . . . . . . . . 15
1611, 15mpbid 202 . . . . . . . . . . . . . 14
17 eluz2 10484 . . . . . . . . . . . . . 14
185, 10, 16, 17syl3anbrc 1138 . . . . . . . . . . . . 13
19 simpr 448 . . . . . . . . . . . . . 14
2019ralimi 2773 . . . . . . . . . . . . 13
21 fveq2 5720 . . . . . . . . . . . . . . . . 17
2221oveq1d 6088 . . . . . . . . . . . . . . . 16
2322fveq2d 5724 . . . . . . . . . . . . . . 15
2423breq1d 4214 . . . . . . . . . . . . . 14
2524rspcv 3040 . . . . . . . . . . . . 13
2618, 20, 25syl2im 36 . . . . . . . . . . . 12
27 climrlim2.4 . . . . . . . . . . . . . . . . . . . . 21
2827adantr 452 . . . . . . . . . . . . . . . . . . . 20
29 climrlim2.7 . . . . . . . . . . . . . . . . . . . . 21
30 flge 11204 . . . . . . . . . . . . . . . . . . . . . 22
317, 28, 30syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
3229, 31mpbid 202 . . . . . . . . . . . . . . . . . . . 20
33 eluz2 10484 . . . . . . . . . . . . . . . . . . . 20
3428, 8, 32, 33syl3anbrc 1138 . . . . . . . . . . . . . . . . . . 19
3534, 3syl6eleqr 2526 . . . . . . . . . . . . . . . . . 18
36 climrlim2.6 . . . . . . . . . . . . . . . . . . . . 21
3736ralrimiva 2781 . . . . . . . . . . . . . . . . . . . 20
3837adantr 452 . . . . . . . . . . . . . . . . . . 19
39 climrlim2.2 . . . . . . . . . . . . . . . . . . . . 21
4039eleq1d 2501 . . . . . . . . . . . . . . . . . . . 20
4140rspcv 3040 . . . . . . . . . . . . . . . . . . 19
4235, 38, 41sylc 58 . . . . . . . . . . . . . . . . . 18
43 eqid 2435 . . . . . . . . . . . . . . . . . . 19
4439, 43fvmptg 5796 . . . . . . . . . . . . . . . . . 18
4535, 42, 44syl2anc 643 . . . . . . . . . . . . . . . . 17
4645adantlr 696 . . . . . . . . . . . . . . . 16
4746ad2ant2r 728 . . . . . . . . . . . . . . 15
4847oveq1d 6088 . . . . . . . . . . . . . 14
4948fveq2d 5724 . . . . . . . . . . . . 13
5049breq1d 4214 . . . . . . . . . . . 12
5126, 50sylibd 206 . . . . . . . . . . 11
5251expr 599 . . . . . . . . . 10
5352com23 74 . . . . . . . . 9
5453ralrimdva 2788 . . . . . . . 8
55 eluzelre 10487 . . . . . . . . . 10
5655, 3eleq2s 2527 . . . . . . . . 9
5756adantl 453 . . . . . . . 8
5854, 57jctild 528 . . . . . . 7
5958expimpd 587 . . . . . 6
6059reximdv2 2807 . . . . 5
6160ralimdva 2776 . . . 4