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

Theorem rpnnen2lem7 12822
 Description: Lemma for rpnnen2 12827. (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 2438 . 2
2 simp3 960 . . 3
32nnzd 10376 . 2
4 eqidd 2439 . 2
5 nnuz 10523 . . . . 5
65uztrn2 10505 . . . 4
72, 6sylan 459 . . 3
8 sstr 3358 . . . . . 6
983adant3 978 . . . . 5
10 rpnnen2.1 . . . . . 6
1110rpnnen2lem2 12817 . . . . 5
129, 11syl 16 . . . 4
1312ffvelrnda 5872 . . 3
147, 13syldan 458 . 2
15 eqidd 2439 . 2
1610rpnnen2lem2 12817 . . . . 5
17163ad2ant2 980 . . . 4
1817ffvelrnda 5872 . . 3
197, 18syldan 458 . 2
2010rpnnen2lem4 12819 . . . . . 6
2120simprd 451 . . . . 5
22213expa 1154 . . . 4