Metamath Proof Explorer

Theorem elpq

Description: A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022)

Ref Expression
Assertion elpq ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )

Proof

Step Hyp Ref Expression
1 elq ⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑧 / 𝑦 ) )
2 rexcom ⊢ ( ∃ 𝑧 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑧 / 𝑦 ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℤ 𝐴 = ( 𝑧 / 𝑦 ) )
3 1 2 bitri ⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℤ 𝐴 = ( 𝑧 / 𝑦 ) )
4 breq2 ⊢ ( 𝐴 = ( 𝑧 / 𝑦 ) → ( 0 < 𝐴 ↔ 0 < ( 𝑧 / 𝑦 ) ) )
5 zre ⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
6 5 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 𝑧 ∈ ℝ )
7 nnre ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
8 7 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 𝑦 ∈ ℝ )
9 nngt0 ⊢ ( 𝑦 ∈ ℕ → 0 < 𝑦 )
10 9 adantr ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → 0 < 𝑦 )
11 gt0div ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) → ( 0 < 𝑧 ↔ 0 < ( 𝑧 / 𝑦 ) ) )
12 6 8 10 11 syl3anc ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 0 < 𝑧 ↔ 0 < ( 𝑧 / 𝑦 ) ) )
13 12 bicomd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 0 < ( 𝑧 / 𝑦 ) ↔ 0 < 𝑧 ) )
14 4 13 sylan9bb ⊢ ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 0 < 𝐴 ↔ 0 < 𝑧 ) )
15 elnnz ⊢ ( 𝑧 ∈ ℕ ↔ ( 𝑧 ∈ ℤ ∧ 0 < 𝑧 ) )
16 15 simplbi2 ⊢ ( 𝑧 ∈ ℤ → ( 0 < 𝑧 → 𝑧 ∈ ℕ ) )
17 16 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 0 < 𝑧 → 𝑧 ∈ ℕ ) )
18 17 adantl ⊢ ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 0 < 𝑧 → 𝑧 ∈ ℕ ) )
19 18 imp ⊢ ( ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) ∧ 0 < 𝑧 ) → 𝑧 ∈ ℕ )
20 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 / 𝑦 ) = ( 𝑧 / 𝑦 ) )
21 20 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐴 = ( 𝑥 / 𝑦 ) ↔ 𝐴 = ( 𝑧 / 𝑦 ) ) )
22 21 adantl ⊢ ( ( ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) ∧ 0 < 𝑧 ) ∧ 𝑥 = 𝑧 ) → ( 𝐴 = ( 𝑥 / 𝑦 ) ↔ 𝐴 = ( 𝑧 / 𝑦 ) ) )
23 simpll ⊢ ( ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) ∧ 0 < 𝑧 ) → 𝐴 = ( 𝑧 / 𝑦 ) )
24 19 22 23 rspcedvd ⊢ ( ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) ∧ 0 < 𝑧 ) → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
25 24 ex ⊢ ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 0 < 𝑧 → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
26 14 25 sylbid ⊢ ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 0 < 𝐴 → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
27 26 ex ⊢ ( 𝐴 = ( 𝑧 / 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 0 < 𝐴 → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) ) )
28 27 com13 ⊢ ( 0 < 𝐴 → ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝐴 = ( 𝑧 / 𝑦 ) → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) ) )
29 28 impl ⊢ ( ( ( 0 < 𝐴 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ℤ ) → ( 𝐴 = ( 𝑧 / 𝑦 ) → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
30 29 rexlimdva ⊢ ( ( 0 < 𝐴 ∧ 𝑦 ∈ ℕ ) → ( ∃ 𝑧 ∈ ℤ 𝐴 = ( 𝑧 / 𝑦 ) → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
31 30 reximdva ⊢ ( 0 < 𝐴 → ( ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℤ 𝐴 = ( 𝑧 / 𝑦 ) → ∃ 𝑦 ∈ ℕ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
32 3 31 syl5bi ⊢ ( 0 < 𝐴 → ( 𝐴 ∈ ℚ → ∃ 𝑦 ∈ ℕ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
33 32 impcom ⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ∃ 𝑦 ∈ ℕ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
34 rexcom ⊢ ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
35 33 34 sylibr ⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )