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 )