df-denom

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdenom	⊢ denom
1		vy	⊢ 𝑦
2		cq	⊢ ℚ
3		c2nd	⊢ 2^nd
4		vx	⊢ 𝑥
5		cz	⊢ ℤ
6		cn	⊢ ℕ
7	5 6	cxp	⊢ ( ℤ × ℕ )
8		c1st	⊢ 1^st
9	4	cv	⊢ 𝑥
10	9 8	cfv	⊢ ( 1^st ‘ 𝑥 )
11		cgcd	⊢ gcd
12	9 3	cfv	⊢ ( 2^nd ‘ 𝑥 )
13	10 12 11	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	10 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	⊢ ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) )
23	1 2 22	cmpt	⊢ ( 𝑦 ∈ ℚ ↦ ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )
24	0 23	wceq	⊢ denom = ( 𝑦 ∈ ℚ ↦ ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑦 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Definition df-denom

Detailed syntax breakdown