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

Proof

Step Hyp Ref Expression
1 1lt2pi 
 |-  1o
2 1pi 
 |-  1o e. N.
3 mulidpi 
 |-  ( 1o e. N. -> ( 1o .N 1o ) = 1o )
4 2 3 ax-mp 
 |-  ( 1o .N 1o ) = 1o
5 addclpi 
 |-  ( ( 1o e. N. /\ 1o e. N. ) -> ( 1o +N 1o ) e. N. )
6 2 2 5 mp2an 
 |-  ( 1o +N 1o ) e. N.
7 mulidpi 
 |-  ( ( 1o +N 1o ) e. 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 )
10 ordpipq 
 |-  ( <. 1o , 1o >. . <-> ( 1o .N 1o )
11 9 10 mpbir 
 |-  <. 1o , 1o >. .
12 df-1nq 
 |-  1Q = <. 1o , 1o >.
13 12 12 oveq12i 
 |-  ( 1Q +pQ 1Q ) = ( <. 1o , 1o >. +pQ <. 1o , 1o >. )
14 addpipq 
 |-  ( ( ( 1o e. N. /\ 1o e. N. ) /\ ( 1o e. N. /\ 1o e. 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
20 lterpq 
 |-  ( 1Q  ( /Q ` 1Q )
21 19 20 mpbi 
 |-  ( /Q ` 1Q )
22 1nq 
 |-  1Q e. Q.
23 nqerid 
 |-  ( 1Q e. Q. -> ( /Q ` 1Q ) = 1Q )
24 22 23 ax-mp 
 |-  ( /Q ` 1Q ) = 1Q
25 24 eqcomi 
 |-  1Q = ( /Q ` 1Q )
26 addpqnq 
 |-  ( ( 1Q e. Q. /\ 1Q e. 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