elq2

Description: Elementhood in the rational numbers, providing the canonical representation. (Contributed by Thierry Arnoux, 9-Nov-2025)

		Ref	Expression
	Assertion	elq2	$⊢ Q \in ℚ \to \exists p \in ℤ \exists q \in ℕ (Q = \frac{p}{q} \land p \gcd q = 1)$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ p = \frac{x}{x \gcd y} \to \frac{p}{q} = \frac{\frac{x}{x \gcd y}}{q}$
2	1	eqeq2d	$⊢ p = \frac{x}{x \gcd y} \to (Q = \frac{p}{q} \leftrightarrow Q = \frac{\frac{x}{x \gcd y}}{q})$
3		oveq1	$⊢ p = \frac{x}{x \gcd y} \to p \gcd q = (\frac{x}{x \gcd y}) \gcd q$
4	3	eqeq1d	$⊢ p = \frac{x}{x \gcd y} \to (p \gcd q = 1 \leftrightarrow (\frac{x}{x \gcd y}) \gcd q = 1)$
5	2 4	anbi12d	$⊢ p = \frac{x}{x \gcd y} \to ((Q = \frac{p}{q} \land p \gcd q = 1) \leftrightarrow (Q = \frac{\frac{x}{x \gcd y}}{q} \land (\frac{x}{x \gcd y}) \gcd q = 1))$
6		oveq2	$⊢ q = \frac{y}{x \gcd y} \to \frac{\frac{x}{x \gcd y}}{q} = \frac{\frac{x}{x \gcd y}}{\frac{y}{x \gcd y}}$
7	6	eqeq2d	$⊢ q = \frac{y}{x \gcd y} \to (Q = \frac{\frac{x}{x \gcd y}}{q} \leftrightarrow Q = \frac{\frac{x}{x \gcd y}}{\frac{y}{x \gcd y}})$
8		oveq2	$⊢ q = \frac{y}{x \gcd y} \to (\frac{x}{x \gcd y}) \gcd q = (\frac{x}{x \gcd y}) \gcd (\frac{y}{x \gcd y})$
9	8	eqeq1d	$⊢ q = \frac{y}{x \gcd y} \to ((\frac{x}{x \gcd y}) \gcd q = 1 \leftrightarrow (\frac{x}{x \gcd y}) \gcd (\frac{y}{x \gcd y}) = 1)$
10	7 9	anbi12d	$⊢ q = \frac{y}{x \gcd y} \to ((Q = \frac{\frac{x}{x \gcd y}}{q} \land (\frac{x}{x \gcd y}) \gcd q = 1) \leftrightarrow (Q = \frac{\frac{x}{x \gcd y}}{\frac{y}{x \gcd y}} \land (\frac{x}{x \gcd y}) \gcd (\frac{y}{x \gcd y}) = 1))$
11		simpllr	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to x \in ℤ$
12		simplr	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to y \in ℕ$
13	12	nnzd	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to y \in ℤ$
14	12	nnne0d	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to y \neq 0$
15		divgcdz	$⊢ (x \in ℤ \land y \in ℤ \land y \neq 0) \to \frac{x}{x \gcd y} \in ℤ$
16	11 13 14 15	syl3anc	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to \frac{x}{x \gcd y} \in ℤ$
17		divgcdnnr	$⊢ (y \in ℕ \land x \in ℤ) \to \frac{y}{x \gcd y} \in ℕ$
18	12 11 17	syl2anc	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to \frac{y}{x \gcd y} \in ℕ$
19		simpr	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to Q = \frac{x}{y}$
20	11	zcnd	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to x \in ℂ$
21	12	nncnd	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to y \in ℂ$
22	11 13	gcdcld	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to x \gcd y \in ℕ_{0}$
23	22	nn0cnd	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to x \gcd y \in ℂ$
24	14	neneqd	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to \neg y = 0$
25	24	intnand	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to \neg (x = 0 \land y = 0)$
26		gcdeq0	$⊢ (x \in ℤ \land y \in ℤ) \to (x \gcd y = 0 \leftrightarrow (x = 0 \land y = 0))$
27	26	necon3abid	$⊢ (x \in ℤ \land y \in ℤ) \to (x \gcd y \neq 0 \leftrightarrow \neg (x = 0 \land y = 0))$
28	27	biimpar	$⊢ ((x \in ℤ \land y \in ℤ) \land \neg (x = 0 \land y = 0)) \to x \gcd y \neq 0$
29	11 13 25 28	syl21anc	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to x \gcd y \neq 0$
30	20 21 23 14 29	divcan7d	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to \frac{\frac{x}{x \gcd y}}{\frac{y}{x \gcd y}} = \frac{x}{y}$
31	19 30	eqtr4d	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to Q = \frac{\frac{x}{x \gcd y}}{\frac{y}{x \gcd y}}$
32		divgcdcoprm0	$⊢ (x \in ℤ \land y \in ℤ \land y \neq 0) \to (\frac{x}{x \gcd y}) \gcd (\frac{y}{x \gcd y}) = 1$
33	11 13 14 32	syl3anc	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to (\frac{x}{x \gcd y}) \gcd (\frac{y}{x \gcd y}) = 1$
34	31 33	jca	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to (Q = \frac{\frac{x}{x \gcd y}}{\frac{y}{x \gcd y}} \land (\frac{x}{x \gcd y}) \gcd (\frac{y}{x \gcd y}) = 1)$
35	5 10 16 18 34	2rspcedvdw	$⊢ (((Q \in ℚ \land x \in ℤ) \land y \in ℕ) \land Q = \frac{x}{y}) \to \exists p \in ℤ \exists q \in ℕ (Q = \frac{p}{q} \land p \gcd q = 1)$
36		elq	$⊢ Q \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ Q = \frac{x}{y}$
37	36	biimpi	$⊢ Q \in ℚ \to \exists x \in ℤ \exists y \in ℕ Q = \frac{x}{y}$
38	35 37	r19.29vva	$⊢ Q \in ℚ \to \exists p \in ℤ \exists q \in ℕ (Q = \frac{p}{q} \land p \gcd q = 1)$

Metamath Proof Explorer

Theorem elq2

Proof