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

Proof

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