Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axlowdim1 Structured version   Unicode version

Theorem axlowdim1 25891
 Description: The lower dimensional axiom for one dimension. In any dimension, there are at least two distinct points. Theorem 3.13 of [Schwabhauser] p. 32, where it is derived from axlowdim2 25892. (Contributed by Scott Fenton, 22-Apr-2013.)
Assertion
Ref Expression
axlowdim1
Distinct variable group:   ,,

Proof of Theorem axlowdim1
StepHypRef Expression
1 1re 9083 . . . 4
21fconst6 5626 . . 3
3 elee 25826 . . 3
42, 3mpbiri 225 . 2
5 0re 9084 . . . 4
65fconst6 5626 . . 3
7 elee 25826 . . 3
86, 7mpbiri 225 . 2
9 ax-1ne0 9052 . . . . . . 7
10 df-ne 2601 . . . . . . 7
119, 10mpbi 200 . . . . . 6
12 1ex 9079 . . . . . . 7
1312sneqr 3959 . . . . . 6
1411, 13mto 169 . . . . 5
15 elnnuz 10515 . . . . . . . . 9
16 eluzfz1 11057 . . . . . . . . 9
1715, 16sylbi 188 . . . . . . . 8
18 ne0i 3627 . . . . . . . 8
1917, 18syl 16 . . . . . . 7
20 rnxp 5292 . . . . . . 7
2119, 20syl 16 . . . . . 6
22 rnxp 5292 . . . . . . 7
2319, 22syl 16 . . . . . 6
2421, 23eqeq12d 2450 . . . . 5
2514, 24mtbiri 295 . . . 4
26 rneq 5088 . . . 4
2725, 26nsyl 115 . . 3