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 >. )