Theorem 1lt2nq

Description: One is less than two (one plus one). (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	1lt2nq	⊢ 1Q <Q ( 1Q +Q 1Q )

Proof

Step	Hyp	Ref	Expression
1		1lt2pi	⊢ 1o <N ( 1o +N 1o )
2		1pi	⊢ 1o ∈ N
3		mulidpi	⊢ ( 1o ∈ N → ( 1o ·N 1o ) = 1o )
4	2 3	ax-mp	⊢ ( 1o ·N 1o ) = 1o
5		addclpi	⊢ ( ( 1o ∈ N ∧ 1o ∈ N ) → ( 1o +N 1o ) ∈ N )
6	2 2 5	mp2an	⊢ ( 1o +N 1o ) ∈ N
7		mulidpi	⊢ ( ( 1o +N 1o ) ∈ N → ( ( 1o +N 1o ) ·N 1o ) = ( 1o +N 1o ) )
8	6 7	ax-mp	⊢ ( ( 1o +N 1o ) ·N 1o ) = ( 1o +N 1o )
9	1 4 8	3brtr4i	⊢ ( 1o ·N 1o ) <N ( ( 1o +N 1o ) ·N 1o )
10		ordpipq	⊢ ( ⟨ 1o , 1o ⟩ <pQ ⟨ ( 1o +N 1o ) , 1o ⟩ ↔ ( 1o ·N 1o ) <N ( ( 1o +N 1o ) ·N 1o ) )
11	9 10	mpbir	⊢ ⟨ 1o , 1o ⟩ <pQ ⟨ ( 1o +N 1o ) , 1o ⟩
12		df-1nq	⊢ 1Q = ⟨ 1o , 1o ⟩
13	12 12	oveq12i	⊢ ( 1Q +pQ 1Q ) = ( ⟨ 1o , 1o ⟩ +pQ ⟨ 1o , 1o ⟩ )
14		addpipq	⊢ ( ( ( 1o ∈ N ∧ 1o ∈ N ) ∧ ( 1o ∈ N ∧ 1o ∈ N ) ) → ( ⟨ 1o , 1o ⟩ +pQ ⟨ 1o , 1o ⟩ ) = ⟨ ( ( 1o ·N 1o ) +N ( 1o ·N 1o ) ) , ( 1o ·N 1o ) ⟩ )
15	2 2 2 2 14	mp4an	⊢ ( ⟨ 1o , 1o ⟩ +pQ ⟨ 1o , 1o ⟩ ) = ⟨ ( ( 1o ·N 1o ) +N ( 1o ·N 1o ) ) , ( 1o ·N 1o ) ⟩
16	4 4	oveq12i	⊢ ( ( 1o ·N 1o ) +N ( 1o ·N 1o ) ) = ( 1o +N 1o )
17	16 4	opeq12i	⊢ ⟨ ( ( 1o ·N 1o ) +N ( 1o ·N 1o ) ) , ( 1o ·N 1o ) ⟩ = ⟨ ( 1o +N 1o ) , 1o ⟩
18	13 15 17	3eqtri	⊢ ( 1Q +pQ 1Q ) = ⟨ ( 1o +N 1o ) , 1o ⟩
19	11 12 18	3brtr4i	⊢ 1Q <pQ ( 1Q +pQ 1Q )
20		lterpq	⊢ ( 1Q <pQ ( 1Q +pQ 1Q ) ↔ ( [Q] ‘ 1Q ) <Q ( [Q] ‘ ( 1Q +pQ 1Q ) ) )
21	19 20	mpbi	⊢ ( [Q] ‘ 1Q ) <Q ( [Q] ‘ ( 1Q +pQ 1Q ) )
22		1nq	⊢ 1Q ∈ Q
23		nqerid	⊢ ( 1Q ∈ Q → ( [Q] ‘ 1Q ) = 1Q )
24	22 23	ax-mp	⊢ ( [Q] ‘ 1Q ) = 1Q
25	24	eqcomi	⊢ 1Q = ( [Q] ‘ 1Q )
26		addpqnq	⊢ ( ( 1Q ∈ Q ∧ 1Q ∈ Q ) → ( 1Q +Q 1Q ) = ( [Q] ‘ ( 1Q +pQ 1Q ) ) )
27	22 22 26	mp2an	⊢ ( 1Q +Q 1Q ) = ( [Q] ‘ ( 1Q +pQ 1Q ) )
28	21 25 27	3brtr4i	⊢ 1Q <Q ( 1Q +Q 1Q )