Metamath Proof Explorer

Theorem elq2

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

Ref Expression
Assertion elq2 ( 𝑄 ∈ ℚ → ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ ( 𝑄 = ( 𝑝 / 𝑞 ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑝 = ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) → ( 𝑝 / 𝑞 ) = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / 𝑞 ) )
2 1 eqeq2d ⊢ ( 𝑝 = ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) → ( 𝑄 = ( 𝑝 / 𝑞 ) ↔ 𝑄 = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / 𝑞 ) ) )
3 oveq1 ⊢ ( 𝑝 = ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) → ( 𝑝 gcd 𝑞 ) = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd 𝑞 ) )
4 3 eqeq1d ⊢ ( 𝑝 = ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) → ( ( 𝑝 gcd 𝑞 ) = 1 ↔ ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd 𝑞 ) = 1 ) )
5 2 4 anbi12d ⊢ ( 𝑝 = ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) → ( ( 𝑄 = ( 𝑝 / 𝑞 ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) ↔ ( 𝑄 = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / 𝑞 ) ∧ ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd 𝑞 ) = 1 ) ) )
6 oveq2 ⊢ ( 𝑞 = ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) → ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / 𝑞 ) = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) )
7 6 eqeq2d ⊢ ( 𝑞 = ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) → ( 𝑄 = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / 𝑞 ) ↔ 𝑄 = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) ) )
8 oveq2 ⊢ ( 𝑞 = ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) → ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd 𝑞 ) = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) )
9 8 eqeq1d ⊢ ( 𝑞 = ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) → ( ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd 𝑞 ) = 1 ↔ ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) = 1 ) )
10 7 9 anbi12d ⊢ ( 𝑞 = ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) → ( ( 𝑄 = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / 𝑞 ) ∧ ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd 𝑞 ) = 1 ) ↔ ( 𝑄 = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) ∧ ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) = 1 ) ) )
11 simpllr ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → 𝑥 ∈ ℤ )
12 simplr ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → 𝑦 ∈ ℕ )
13 12 nnzd ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → 𝑦 ∈ ℤ )
14 12 nnne0d ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → 𝑦 ≠ 0 )
15 divgcdz ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) ∈ ℤ )
16 11 13 14 15 syl3anc ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) ∈ ℤ )
17 divgcdnnr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑥 ∈ ℤ ) → ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ∈ ℕ )
18 12 11 17 syl2anc ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ∈ ℕ )
19 simpr ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → 𝑄 = ( 𝑥 / 𝑦 ) )
20 11 zcnd ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → 𝑥 ∈ ℂ )
21 12 nncnd ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → 𝑦 ∈ ℂ )
22 11 13 gcdcld ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ( 𝑥 gcd 𝑦 ) ∈ ℕ0 )
23 22 nn0cnd ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ( 𝑥 gcd 𝑦 ) ∈ ℂ )
24 14 neneqd ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ¬ 𝑦 = 0 )
25 24 intnand ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ¬ ( 𝑥 = 0 ∧ 𝑦 = 0 ) )
26 gcdeq0 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 gcd 𝑦 ) = 0 ↔ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) )
27 26 necon3abid ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 gcd 𝑦 ) ≠ 0 ↔ ¬ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) )
28 27 biimpar ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ¬ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) → ( 𝑥 gcd 𝑦 ) ≠ 0 )
29 11 13 25 28 syl21anc ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ( 𝑥 gcd 𝑦 ) ≠ 0 )
30 20 21 23 14 29 divcan7d ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) = ( 𝑥 / 𝑦 ) )
31 19 30 eqtr4d ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → 𝑄 = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) )
32 divgcdcoprm0 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑦 ≠ 0 ) → ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) = 1 )
33 11 13 14 32 syl3anc ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) = 1 )
34 31 33 jca ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ( 𝑄 = ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) / ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) ∧ ( ( 𝑥 / ( 𝑥 gcd 𝑦 ) ) gcd ( 𝑦 / ( 𝑥 gcd 𝑦 ) ) ) = 1 ) )
35 5 10 16 18 34 2rspcedvdw ⊢ ( ( ( ( 𝑄 ∈ ℚ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℕ ) ∧ 𝑄 = ( 𝑥 / 𝑦 ) ) → ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ ( 𝑄 = ( 𝑝 / 𝑞 ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) )
36 elq ⊢ ( 𝑄 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑄 = ( 𝑥 / 𝑦 ) )
37 36 biimpi ⊢ ( 𝑄 ∈ ℚ → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝑄 = ( 𝑥 / 𝑦 ) )
38 35 37 r19.29vva ⊢ ( 𝑄 ∈ ℚ → ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ ( 𝑄 = ( 𝑝 / 𝑞 ) ∧ ( 𝑝 gcd 𝑞 ) = 1 ) )