df-numer

Description: The canonical numerator of a rational is the numerator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014)

		Ref	Expression
	Assertion	df-numer	⊢ numer = ( 𝑦 ∈ ℚ ↦ ( 1^st ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnumer	⊢ numer
1		vy	⊢ 𝑦
2		cq	⊢ ℚ
3		c1st	⊢ 1^st
4		vx	⊢ 𝑥
5		cz	⊢ ℤ
6		cn	⊢ ℕ
7	5 6	cxp	⊢ ( ℤ × ℕ )
8	4	cv	⊢ 𝑥
9	8 3	cfv	⊢ ( 1^st ‘ 𝑥 )
10		cgcd	⊢ gcd
11		c2nd	⊢ 2^nd
12	8 11	cfv	⊢ ( 2^nd ‘ 𝑥 )
13	9 12 10	co	⊢ ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) )
14		c1	⊢ 1
15	13 14	wceq	⊢ ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1
16	1	cv	⊢ 𝑦
17		cdiv	⊢ /
18	9 12 17	co	⊢ ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) )
19	16 18	wceq	⊢ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) )
20	15 19	wa	⊢ ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) )
21	20 4 7	crio	⊢ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) )
22	21 3	cfv	⊢ ( 1^st ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) )
23	1 2 22	cmpt	⊢ ( 𝑦 ∈ ℚ ↦ ( 1^st ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )
24	0 23	wceq	⊢ numer = ( 𝑦 ∈ ℚ ↦ ( 1^st ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Definition df-numer

Detailed syntax breakdown