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 → 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 1oN
6 mulcanenq ( ( 𝐴N ∧ 1oN ∧ 1oN ) → ⟨ ( 𝐴 ·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𝐴 , 𝐴 ⟩ )