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

Theorem rpnnen2lem5 12705
 Description: Lemma for rpnnen2 12712. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
Hypothesis
Ref Expression
rpnnen2.1
Assertion
Ref Expression
rpnnen2lem5
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem rpnnen2lem5
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nnuz 10414 . . . 4
2 1nn 9904 . . . . 5
32a1i 10 . . . 4
4 ssid 3283 . . . . . 6
5 rpnnen2.1 . . . . . . 7
65rpnnen2lem2 12702 . . . . . 6
74, 6mp1i 11 . . . . 5
8 ffvelrn 5770 . . . . 5
97, 8sylan 457 . . . 4
105rpnnen2lem2 12702 . . . . 5
11 ffvelrn 5770 . . . . 5
1210, 11sylan 457 . . . 4
135rpnnen2lem3 12703 . . . . 5
14 seqex 11212 . . . . . 6
15 ovex 6006 . . . . . 6
1614, 15breldm 4986 . . . . 5
1713, 16mp1i 11 . . . 4
18 elnnuz 10415 . . . . . 6
195rpnnen2lem4 12704 . . . . . . 7
204, 19mp3an2 1266 . . . . . 6
2118, 20sylan2br 462 . . . . 5
2221simpld 445 . . . 4
2321simprd 449 . . . 4
241, 3, 9, 12, 17, 22, 23cvgcmp 12482 . . 3