enqeq

Description: Corollary of nqereu : if two fractions are both reduced and equivalent, then they are equal. (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	enqeq	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		3simpa	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) )
2		elpqn	⊢ ( 𝐵 ∈ Q → 𝐵 ∈ ( N × N ) )
3	2	3ad2ant2	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → 𝐵 ∈ ( N × N ) )
4		nqereu	⊢ ( 𝐵 ∈ ( N × N ) → ∃! 𝑥 ∈ Q 𝑥 ~_Q 𝐵 )
5		reurmo	⊢ ( ∃! 𝑥 ∈ Q 𝑥 ~_Q 𝐵 → ∃* 𝑥 ∈ Q 𝑥 ~_Q 𝐵 )
6	3 4 5	3syl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → ∃* 𝑥 ∈ Q 𝑥 ~_Q 𝐵 )
7		df-rmo	⊢ ( ∃* 𝑥 ∈ Q 𝑥 ~_Q 𝐵 ↔ ∃* 𝑥 ( 𝑥 ∈ Q ∧ 𝑥 ~_Q 𝐵 ) )
8	6 7	sylib	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → ∃* 𝑥 ( 𝑥 ∈ Q ∧ 𝑥 ~_Q 𝐵 ) )
9		3simpb	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → ( 𝐴 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) )
10		simp2	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → 𝐵 ∈ Q )
11		enqer	⊢ ~_Q Er ( N × N )
12	11	a1i	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → ~_Q Er ( N × N ) )
13	12 3	erref	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → 𝐵 ~_Q 𝐵 )
14	10 13	jca	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → ( 𝐵 ∈ Q ∧ 𝐵 ~_Q 𝐵 ) )
15		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ Q ↔ 𝐴 ∈ Q ) )
16		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ~_Q 𝐵 ↔ 𝐴 ~_Q 𝐵 ) )
17	15 16	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ Q ∧ 𝑥 ~_Q 𝐵 ) ↔ ( 𝐴 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) ) )
18		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ Q ↔ 𝐵 ∈ Q ) )
19		breq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ~_Q 𝐵 ↔ 𝐵 ~_Q 𝐵 ) )
20	18 19	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ Q ∧ 𝑥 ~_Q 𝐵 ) ↔ ( 𝐵 ∈ Q ∧ 𝐵 ~_Q 𝐵 ) ) )
21	17 20	moi	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ ∃* 𝑥 ( 𝑥 ∈ Q ∧ 𝑥 ~_Q 𝐵 ) ∧ ( ( 𝐴 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) ∧ ( 𝐵 ∈ Q ∧ 𝐵 ~_Q 𝐵 ) ) ) → 𝐴 = 𝐵 )
22	1 8 9 14 21	syl112anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~_Q 𝐵 ) → 𝐴 = 𝐵 )

Metamath Proof Explorer

Theorem enqeq

Proof