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

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

Proof of Theorem rpnnen2lem7
StepHypRef Expression
1 eqid 2283 . 2
2 simp3 957 . . 3
32nnzd 10116 . 2
4 eqidd 2284 . 2
5 nnuz 10263 . . . . 5
65uztrn2 10245 . . . 4
72, 6sylan 457 . . 3
8 sstr 3187 . . . . . 6
983adant3 975 . . . . 5
10 rpnnen2.1 . . . . . 6
1110rpnnen2lem2 12494 . . . . 5
129, 11syl 15 . . . 4
13 ffvelrn 5663 . . . 4
1412, 13sylan 457 . . 3
157, 14syldan 456 . 2
16 eqidd 2284 . 2
1710rpnnen2lem2 12494 . . . . 5
18173ad2ant2 977 . . . 4
19 ffvelrn 5663 . . . 4
2018, 19sylan 457 . . 3
217, 20syldan 456 . 2
2210rpnnen2lem4 12496 . . . . . 6
2322simprd 449 . . . . 5
24233expa 1151 . . . 4