Theorem znumd

Description: Numerator of an integer. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypothesis	znumd.1	⊢ ( 𝜑 → 𝑍 ∈ ℤ )
Assertion	znumd	⊢ ( 𝜑 → ( numer ‘ 𝑍 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		znumd.1	⊢ ( 𝜑 → 𝑍 ∈ ℤ )
2		zq	⊢ ( 𝑍 ∈ ℤ → 𝑍 ∈ ℚ )
3	1 2	syl	⊢ ( 𝜑 → 𝑍 ∈ ℚ )
4		1nn	⊢ 1 ∈ ℕ
5	4	a1i	⊢ ( 𝜑 → 1 ∈ ℕ )
6		gcd1	⊢ ( 𝑍 ∈ ℤ → ( 𝑍 gcd 1 ) = 1 )
7	1 6	syl	⊢ ( 𝜑 → ( 𝑍 gcd 1 ) = 1 )
8	1	zcnd	⊢ ( 𝜑 → 𝑍 ∈ ℂ )
9	8	div1d	⊢ ( 𝜑 → ( 𝑍 / 1 ) = 𝑍 )
10	9	eqcomd	⊢ ( 𝜑 → 𝑍 = ( 𝑍 / 1 ) )
11		qnumdenbi	⊢ ( ( 𝑍 ∈ ℚ ∧ 𝑍 ∈ ℤ ∧ 1 ∈ ℕ ) → ( ( ( 𝑍 gcd 1 ) = 1 ∧ 𝑍 = ( 𝑍 / 1 ) ) ↔ ( ( numer ‘ 𝑍 ) = 𝑍 ∧ ( denom ‘ 𝑍 ) = 1 ) ) )
12	11	biimpa	⊢ ( ( ( 𝑍 ∈ ℚ ∧ 𝑍 ∈ ℤ ∧ 1 ∈ ℕ ) ∧ ( ( 𝑍 gcd 1 ) = 1 ∧ 𝑍 = ( 𝑍 / 1 ) ) ) → ( ( numer ‘ 𝑍 ) = 𝑍 ∧ ( denom ‘ 𝑍 ) = 1 ) )
13	3 1 5 7 10 12	syl32anc	⊢ ( 𝜑 → ( ( numer ‘ 𝑍 ) = 𝑍 ∧ ( denom ‘ 𝑍 ) = 1 ) )
14	13	simpld	⊢ ( 𝜑 → ( numer ‘ 𝑍 ) = 𝑍 )