This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1lt2pi

Description: One is less than two (one plus one). (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion 1lt2pi 1o <N ( 1o +N 1o )

Proof

Step Hyp Ref Expression
1 1onn ⊢ 1o ∈ ω
2 nna0 ⊢ ( 1o ∈ ω → ( 1o +o ∅ ) = 1o )
3 1 2 ax-mp ⊢ ( 1o +o ∅ ) = 1o
4 0lt1o ⊢ ∅ ∈ 1o
5 peano1 ⊢ ∅ ∈ ω
6 nnaord ⊢ ( ( ∅ ∈ ω ∧ 1o ∈ ω ∧ 1o ∈ ω ) → ( ∅ ∈ 1o ↔ ( 1o +o ∅ ) ∈ ( 1o +o 1o ) ) )
7 5 1 1 6 mp3an ⊢ ( ∅ ∈ 1o ↔ ( 1o +o ∅ ) ∈ ( 1o +o 1o ) )
8 4 7 mpbi ⊢ ( 1o +o ∅ ) ∈ ( 1o +o 1o )
9 3 8 eqeltrri ⊢ 1o ∈ ( 1o +o 1o )
10 1pi ⊢ 1o ∈ N
11 addpiord ⊢ ( ( 1o ∈ N ∧ 1o ∈ N ) → ( 1o +N 1o ) = ( 1o +o 1o ) )
12 10 10 11 mp2an ⊢ ( 1o +N 1o ) = ( 1o +o 1o )
13 9 12 eleqtrri ⊢ 1o ∈ ( 1o +N 1o )
14 addclpi ⊢ ( ( 1o ∈ N ∧ 1o ∈ N ) → ( 1o +N 1o ) ∈ N )
15 10 10 14 mp2an ⊢ ( 1o +N 1o ) ∈ N
16 ltpiord ⊢ ( ( 1o ∈ N ∧ ( 1o +N 1o ) ∈ N ) → ( 1o <N ( 1o +N 1o ) ↔ 1o ∈ ( 1o +N 1o ) ) )
17 10 15 16 mp2an ⊢ ( 1o <N ( 1o +N 1o ) ↔ 1o ∈ ( 1o +N 1o ) )
18 13 17 mpbir ⊢ 1o <N ( 1o +N 1o )