Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax0lt1 GIF version

Theorem ax0lt1 7707
 Description: 0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 7749. The version of this axiom in the Metamath Proof Explorer reads 1 ≠ 0; here we change it to 0 <ℝ 1. The proof of 0 <ℝ 1 from 1 ≠ 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
Assertion
Ref Expression
ax0lt1 0 < 1

Proof of Theorem ax0lt1
StepHypRef Expression
1 0lt1sr 7596 . . 3 0R <R 1R
2 ltresr 7670 . . 3 (⟨0R, 0R⟩ < ⟨1R, 0R⟩ ↔ 0R <R 1R)
31, 2mpbir 145 . 2 ⟨0R, 0R⟩ < ⟨1R, 0R
4 df-0 7650 . 2 0 = ⟨0R, 0R
5 df-1 7651 . 2 1 = ⟨1R, 0R
63, 4, 53brtr4i 3965 1 0 < 1
 Colors of variables: wff set class Syntax hints:  ⟨cop 3534   class class class wbr 3936  0Rc0r 7129  1Rc1r 7130
 Copyright terms: Public domain W3C validator