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

Theorem 1lt2pi 7168
 Description: One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
Assertion
Ref Expression
1lt2pi 1o <N (1o +N 1o)

Proof of Theorem 1lt2pi
StepHypRef Expression
1 1onn 6420 . . . . 5 1o ∈ ω
2 nna0 6374 . . . . 5 (1o ∈ ω → (1o +o ∅) = 1o)
31, 2ax-mp 5 . . . 4 (1o +o ∅) = 1o
4 0lt1o 6341 . . . . 5 ∅ ∈ 1o
5 peano1 4512 . . . . . 6 ∅ ∈ ω
6 nnaord 6409 . . . . . 6 ((∅ ∈ ω ∧ 1o ∈ ω ∧ 1o ∈ ω) → (∅ ∈ 1o ↔ (1o +o ∅) ∈ (1o +o 1o)))
75, 1, 1, 6mp3an 1316 . . . . 5 (∅ ∈ 1o ↔ (1o +o ∅) ∈ (1o +o 1o))
84, 7mpbi 144 . . . 4 (1o +o ∅) ∈ (1o +o 1o)
93, 8eqeltrri 2214 . . 3 1o ∈ (1o +o 1o)
10 1pi 7143 . . . 4 1oN
11 addpiord 7144 . . . 4 ((1oN ∧ 1oN) → (1o +N 1o) = (1o +o 1o))
1210, 10, 11mp2an 423 . . 3 (1o +N 1o) = (1o +o 1o)
139, 12eleqtrri 2216 . 2 1o ∈ (1o +N 1o)
14 addclpi 7155 . . . 4 ((1oN ∧ 1oN) → (1o +N 1o) ∈ N)
1510, 10, 14mp2an 423 . . 3 (1o +N 1o) ∈ N
16 ltpiord 7147 . . 3 ((1oN ∧ (1o +N 1o) ∈ N) → (1o <N (1o +N 1o) ↔ 1o ∈ (1o +N 1o)))
1710, 15, 16mp2an 423 . 2 (1o <N (1o +N 1o) ↔ 1o ∈ (1o +N 1o))
1813, 17mpbir 145 1 1o <N (1o +N 1o)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   = wceq 1332   ∈ wcel 1481  ∅c0 3364   class class class wbr 3933  ωcom 4508  (class class class)co 5778  1oc1o 6310   +o coa 6314  Ncnpi 7100   +N cpli 7101
 Copyright terms: Public domain W3C validator