Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rmxnn Structured version   Unicode version

Theorem rmxnn 27007
 Description: The X-sequence is defined to range over but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
Assertion
Ref Expression
rmxnn Xrm

Proof of Theorem rmxnn
StepHypRef Expression
1 nn0z 10296 . . . . 5
2 frmx 26967 . . . . . 6 Xrm
32fovcl 6167 . . . . 5 Xrm
41, 3sylan2 461 . . . 4 Xrm
5 rmxypos 27003 . . . . 5 Xrm Yrm
65simpld 446 . . . 4 Xrm
7 elnnnn0b 10256 . . . 4 Xrm Xrm Xrm
84, 6, 7sylanbrc 646 . . 3 Xrm
10 rmxneg 26978 . . . 4 Xrm Xrm
1110adantr 452 . . 3 Xrm Xrm
12 nn0z 10296 . . . . . 6
132fovcl 6167 . . . . . 6 Xrm
1412, 13sylan2 461 . . . . 5 Xrm
15 rmxypos 27003 . . . . . 6 Xrm Yrm
1615simpld 446 . . . . 5 Xrm
17 elnnnn0b 10256 . . . . 5 Xrm Xrm Xrm
1814, 16, 17sylanbrc 646 . . . 4 Xrm
1918adantlr 696 . . 3 Xrm
2011, 19eqeltrrd 2510 . 2 Xrm
21 elznn0 10288 . . . 4
2221simprbi 451 . . 3