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

Metamath Proof Explorer

Theorem 1nqenq

Description: The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion 1nqenq 
|- ( A e. N. -> 1Q ~Q <. A , A >. )

Proof

Step Hyp Ref Expression
1 enqer 
 |-  ~Q Er ( N. X. N. )
2 1 a1i 
 |-  ( A e. N. -> ~Q Er ( N. X. N. ) )
3 mulidpi 
 |-  ( A e. N. -> ( A .N 1o ) = A )
4 3 3 opeq12d 
 |-  ( A e. N. -> <. ( A .N 1o ) , ( A .N 1o ) >. = <. A , A >. )
5 1pi 
 |-  1o e. N.
6 mulcanenq 
 |-  ( ( A e. N. /\ 1o e. N. /\ 1o e. N. ) -> <. ( A .N 1o ) , ( A .N 1o ) >. ~Q <. 1o , 1o >. )
7 5 5 6 mp3an23 
 |-  ( A e. N. -> <. ( A .N 1o ) , ( A .N 1o ) >. ~Q <. 1o , 1o >. )
8 df-1nq 
 |-  1Q = <. 1o , 1o >.
9 7 8 breqtrrdi 
 |-  ( A e. N. -> <. ( A .N 1o ) , ( A .N 1o ) >. ~Q 1Q )
10 4 9 eqbrtrrd 
 |-  ( A e. N. -> <. A , A >. ~Q 1Q )
11 2 10 ersym 
 |-  ( A e. N. -> 1Q ~Q <. A , A >. )