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

Metamath Proof Explorer

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 )