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	⊢ ( 𝐴 ∈ N → 1Q ~Q ⟨ 𝐴 , 𝐴 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		enqer	⊢ ~Q Er ( N × N )
2	1	a1i	⊢ ( 𝐴 ∈ N → ~Q Er ( N × N ) )
3		mulidpi	⊢ ( 𝐴 ∈ N → ( 𝐴 ·N 1o ) = 𝐴 )
4	3 3	opeq12d	⊢ ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 1o ) , ( 𝐴 ·N 1o ) ⟩ = ⟨ 𝐴 , 𝐴 ⟩ )
5		1pi	⊢ 1o ∈ N
6		mulcanenq	⊢ ( ( 𝐴 ∈ N ∧ 1o ∈ N ∧ 1o ∈ N ) → ⟨ ( 𝐴 ·N 1o ) , ( 𝐴 ·N 1o ) ⟩ ~Q ⟨ 1o , 1o ⟩ )
7	5 5 6	mp3an23	⊢ ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 1o ) , ( 𝐴 ·N 1o ) ⟩ ~Q ⟨ 1o , 1o ⟩ )
8		df-1nq	⊢ 1Q = ⟨ 1o , 1o ⟩
9	7 8	breqtrrdi	⊢ ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 1o ) , ( 𝐴 ·N 1o ) ⟩ ~Q 1Q )
10	4 9	eqbrtrrd	⊢ ( 𝐴 ∈ N → ⟨ 𝐴 , 𝐴 ⟩ ~Q 1Q )
11	2 10	ersym	⊢ ( 𝐴 ∈ N → 1Q ~Q ⟨ 𝐴 , 𝐴 ⟩ )