Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  1lt2pi Structured version   Visualization version   GIF version

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

Proof of Theorem 1lt2pi
StepHypRef Expression
1 1onn 7871 . . . . 5 1𝑜 ∈ ω
2 nna0 7836 . . . . 5 (1𝑜 ∈ ω → (1𝑜 +𝑜 ∅) = 1𝑜)
31, 2ax-mp 5 . . . 4 (1𝑜 +𝑜 ∅) = 1𝑜
4 0lt1o 7736 . . . . 5 ∅ ∈ 1𝑜
5 peano1 7230 . . . . . 6 ∅ ∈ ω
6 nnaord 7851 . . . . . 6 ((∅ ∈ ω ∧ 1𝑜 ∈ ω ∧ 1𝑜 ∈ ω) → (∅ ∈ 1𝑜 ↔ (1𝑜 +𝑜 ∅) ∈ (1𝑜 +𝑜 1𝑜)))
75, 1, 1, 6mp3an 1570 . . . . 5 (∅ ∈ 1𝑜 ↔ (1𝑜 +𝑜 ∅) ∈ (1𝑜 +𝑜 1𝑜))
84, 7mpbi 220 . . . 4 (1𝑜 +𝑜 ∅) ∈ (1𝑜 +𝑜 1𝑜)
93, 8eqeltrri 2845 . . 3 1𝑜 ∈ (1𝑜 +𝑜 1𝑜)
10 1pi 9905 . . . 4 1𝑜N
11 addpiord 9906 . . . 4 ((1𝑜N ∧ 1𝑜N) → (1𝑜 +N 1𝑜) = (1𝑜 +𝑜 1𝑜))
1210, 10, 11mp2an 707 . . 3 (1𝑜 +N 1𝑜) = (1𝑜 +𝑜 1𝑜)
139, 12eleqtrri 2847 . 2 1𝑜 ∈ (1𝑜 +N 1𝑜)
14 addclpi 9914 . . . 4 ((1𝑜N ∧ 1𝑜N) → (1𝑜 +N 1𝑜) ∈ N)
1510, 10, 14mp2an 707 . . 3 (1𝑜 +N 1𝑜) ∈ N
16 ltpiord 9909 . . 3 ((1𝑜N ∧ (1𝑜 +N 1𝑜) ∈ N) → (1𝑜 <N (1𝑜 +N 1𝑜) ↔ 1𝑜 ∈ (1𝑜 +N 1𝑜)))
1710, 15, 16mp2an 707 . 2 (1𝑜 <N (1𝑜 +N 1𝑜) ↔ 1𝑜 ∈ (1𝑜 +N 1𝑜))
1813, 17mpbir 221 1 1𝑜 <N (1𝑜 +N 1𝑜)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   = wceq 1629   ∈ wcel 2143  ∅c0 4060   class class class wbr 4783  (class class class)co 6791  ωcom 7210  1𝑜c1o 7704   +𝑜 coa 7708  Ncnpi 9866   +N cpli 9867
 Copyright terms: Public domain W3C validator