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 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 / 𝑦 ) = ( 𝑧 / 𝑦 ) )
16 15 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐴 = ( 𝑥 / 𝑦 ) ↔ 𝐴 = ( 𝑧 / 𝑦 ) ) )
17 elnnz ⊢ ( 𝑧 ∈ ℕ ↔ ( 𝑧 ∈ ℤ ∧ 0 < 𝑧 ) )
18 17 simplbi2 ⊢ ( 𝑧 ∈ ℤ → ( 0 < 𝑧 → 𝑧 ∈ ℕ ) )
19 18 adantl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 0 < 𝑧 → 𝑧 ∈ ℕ ) )
20 19 adantl ⊢ ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 0 < 𝑧 → 𝑧 ∈ ℕ ) )
21 20 imp ⊢ ( ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) ∧ 0 < 𝑧 ) → 𝑧 ∈ ℕ )
22 simpll ⊢ ( ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) ∧ 0 < 𝑧 ) → 𝐴 = ( 𝑧 / 𝑦 ) )
23 16 21 22 rspcedvdw ⊢ ( ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) ∧ 0 < 𝑧 ) → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
24 23 ex ⊢ ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 0 < 𝑧 → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
25 14 24 sylbid ⊢ ( ( 𝐴 = ( 𝑧 / 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) ) → ( 0 < 𝐴 → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
26 25 ex ⊢ ( 𝐴 = ( 𝑧 / 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 0 < 𝐴 → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) ) )
27 26 com13 ⊢ ( 0 < 𝐴 → ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ ) → ( 𝐴 = ( 𝑧 / 𝑦 ) → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) ) )
28 27 impl ⊢ ( ( ( 0 < 𝐴 ∧ 𝑦 ∈ ℕ ) ∧ 𝑧 ∈ ℤ ) → ( 𝐴 = ( 𝑧 / 𝑦 ) → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
29 28 rexlimdva ⊢ ( ( 0 < 𝐴 ∧ 𝑦 ∈ ℕ ) → ( ∃ 𝑧 ∈ ℤ 𝐴 = ( 𝑧 / 𝑦 ) → ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
30 29 reximdva ⊢ ( 0 < 𝐴 → ( ∃ 𝑦 ∈ ℕ ∃ 𝑧 ∈ ℤ 𝐴 = ( 𝑧 / 𝑦 ) → ∃ 𝑦 ∈ ℕ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
31 3 30 biimtrid ⊢ ( 0 < 𝐴 → ( 𝐴 ∈ ℚ → ∃ 𝑦 ∈ ℕ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) )
32 31 impcom ⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ∃ 𝑦 ∈ ℕ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
33 rexcom ⊢ ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ↔ ∃ 𝑦 ∈ ℕ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
34 32 33 sylibr ⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )