Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clim1fr1 Unicode version

Theorem clim1fr1 27830
 Description: A class of sequences of fractions that converge to 1 (Contributed by Glauco Siliprandi, 29-Jun-2017.)
Hypotheses
Ref Expression
clim1fr1.1
clim1fr1.2
clim1fr1.3
clim1fr1.4
Assertion
Ref Expression
clim1fr1
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem clim1fr1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nnuz 10279 . . 3
2 1z 10069 . . . 4
32a1i 10 . . 3
4 nnex 9768 . . . . . 6
54mptex 5762 . . . . 5
65a1i 10 . . . 4
73zcnd 10134 . . . 4
8 eqidd 2297 . . . . . 6
9 eqidd 2297 . . . . . 6
10 id 19 . . . . . 6
11 ax-1cn 8811 . . . . . . 7
1211a1i 10 . . . . . 6
138, 9, 10, 12fvmptd 5622 . . . . 5
1413adantl 452 . . . 4
151, 3, 6, 7, 14climconst 12033 . . 3
16 clim1fr1.1 . . . . 5
174mptex 5762 . . . . 5
1816, 17eqeltri 2366 . . . 4
1918a1i 10 . . 3
20 clim1fr1.4 . . . . . . 7
2120adantr 451 . . . . . 6
22 clim1fr1.2 . . . . . . 7
2322adantr 451 . . . . . 6
24 nncn 9770 . . . . . . 7
2524adantl 452 . . . . . 6
26 clim1fr1.3 . . . . . . 7
2726adantr 451 . . . . . 6
28 nnne0 9794 . . . . . . 7
2928adantl 452 . . . . . 6
3021, 23, 25, 27, 29divdiv1d 9583 . . . . 5
3130mpteq2dva 4122 . . . 4
3220, 22, 26divcld 9552 . . . . 5
33 divcnv 12328 . . . . 5
3432, 33syl 15 . . . 4
3531, 34eqbrtrrd 4061 . . 3
3611a1i 10 . . . . . . 7
3736rgen 2621 . . . . . 6
38 eqid 2296 . . . . . . 7
3938fmpt 5697 . . . . . 6
4037, 39mpbi 199 . . . . 5
4140a1i 10 . . . 4
4241ffvelrnda 5681 . . 3
43 nfv 1609 . . . . . 6
4423, 25mulcld 8871 . . . . . . . 8
4523, 25, 27, 29mulne0d 9436 . . . . . . . 8
4621, 44, 45divcld 9552 . . . . . . 7
4746ex 423 . . . . . 6
4843, 47ralrimi 2637 . . . . 5
49 eqid 2296 . . . . . 6
5049fmpt 5697 . . . . 5
5148, 50sylib 188 . . . 4
5251ffvelrnda 5681 . . 3
5316a1i 10 . . . . 5
54 oveq2 5882 . . . . . . . 8
5554oveq1d 5889 . . . . . . 7
5655, 54oveq12d 5892 . . . . . 6
5756adantl 452 . . . . 5
58 simpr 447 . . . . 5
5922adantr 451 . . . . . . . 8
6058nncnd 9778 . . . . . . . 8
6159, 60mulcld 8871 . . . . . . 7
6220adantr 451 . . . . . . 7
6361, 62addcld 8870 . . . . . 6
6426adantr 451 . . . . . . 7
6558nnne0d 9806 . . . . . . 7
6659, 60, 64, 65mulne0d 9436 . . . . . 6
6763, 61, 66divcld 9552 . . . . 5
6853, 57, 58, 67fvmptd 5622 . . . 4
6961, 62, 61, 66divdird 9590 . . . . 5
7061, 66dividd 9550 . . . . . 6
7170oveq1d 5889 . . . . 5
7269, 71eqtrd 2328 . . . 4
7314eqcomd 2301 . . . . 5
74 eqidd 2297 . . . . . . 7
75 simpr 447 . . . . . . . . 9
7675oveq2d 5890 . . . . . . . 8
7776oveq2d 5890 . . . . . . 7
7862, 61, 66divcld 9552 . . . . . . 7
7974, 77, 58, 78fvmptd 5622 . . . . . 6
8079eqcomd 2301 . . . . 5
8173, 80oveq12d 5892 . . . 4
8268, 72, 813eqtrd 2332 . . 3
831, 3, 15, 19, 35, 42, 52, 82climadd 12121 . 2