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

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

Proof of Theorem 1lt2pi
StepHypRef Expression
1 1onn 6181 . . . . 5 1𝑜 ∈ ω
2 nna0 6139 . . . . 5 (1𝑜 ∈ ω → (1𝑜 +𝑜 ∅) = 1𝑜)
31, 2ax-mp 7 . . . 4 (1𝑜 +𝑜 ∅) = 1𝑜
4 0lt1o 6108 . . . . 5 ∅ ∈ 1𝑜
5 peano1 4364 . . . . . 6 ∅ ∈ ω
6 nnaord 6170 . . . . . 6 ((∅ ∈ ω ∧ 1𝑜 ∈ ω ∧ 1𝑜 ∈ ω) → (∅ ∈ 1𝑜 ↔ (1𝑜 +𝑜 ∅) ∈ (1𝑜 +𝑜 1𝑜)))
75, 1, 1, 6mp3an 1269 . . . . 5 (∅ ∈ 1𝑜 ↔ (1𝑜 +𝑜 ∅) ∈ (1𝑜 +𝑜 1𝑜))
84, 7mpbi 143 . . . 4 (1𝑜 +𝑜 ∅) ∈ (1𝑜 +𝑜 1𝑜)
93, 8eqeltrri 2156 . . 3 1𝑜 ∈ (1𝑜 +𝑜 1𝑜)
10 1pi 6603 . . . 4 1𝑜N
11 addpiord 6604 . . . 4 ((1𝑜N ∧ 1𝑜N) → (1𝑜 +N 1𝑜) = (1𝑜 +𝑜 1𝑜))
1210, 10, 11mp2an 417 . . 3 (1𝑜 +N 1𝑜) = (1𝑜 +𝑜 1𝑜)
139, 12eleqtrri 2158 . 2 1𝑜 ∈ (1𝑜 +N 1𝑜)
14 addclpi 6615 . . . 4 ((1𝑜N ∧ 1𝑜N) → (1𝑜 +N 1𝑜) ∈ N)
1510, 10, 14mp2an 417 . . 3 (1𝑜 +N 1𝑜) ∈ N
16 ltpiord 6607 . . 3 ((1𝑜N ∧ (1𝑜 +N 1𝑜) ∈ N) → (1𝑜 <N (1𝑜 +N 1𝑜) ↔ 1𝑜 ∈ (1𝑜 +N 1𝑜)))
1710, 15, 16mp2an 417 . 2 (1𝑜 <N (1𝑜 +N 1𝑜) ↔ 1𝑜 ∈ (1𝑜 +N 1𝑜))
1813, 17mpbir 144 1 1𝑜 <N (1𝑜 +N 1𝑜)
 Colors of variables: wff set class Syntax hints:   ↔ wb 103   = wceq 1285   ∈ wcel 1434  ∅c0 3268   class class class wbr 3806  ωcom 4360  (class class class)co 5564  1𝑜c1o 6079   +𝑜 coa 6083  Ncnpi 6560   +N cpli 6561
 Copyright terms: Public domain W3C validator