Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  zq GIF version

Theorem zq 9468
 Description: An integer is a rational number. (Contributed by NM, 9-Jan-2002.)
Assertion
Ref Expression
zq (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)

Proof of Theorem zq
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqcom 2142 . . . . 5 (𝑥 = 𝐴𝐴 = 𝑥)
2 zcn 9106 . . . . . . 7 (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
32div1d 8587 . . . . . 6 (𝑥 ∈ ℤ → (𝑥 / 1) = 𝑥)
43eqeq2d 2152 . . . . 5 (𝑥 ∈ ℤ → (𝐴 = (𝑥 / 1) ↔ 𝐴 = 𝑥))
51, 4bitr4id 198 . . . 4 (𝑥 ∈ ℤ → (𝑥 = 𝐴𝐴 = (𝑥 / 1)))
6 1nn 8778 . . . . 5 1 ∈ ℕ
7 oveq2 5792 . . . . . . 7 (𝑦 = 1 → (𝑥 / 𝑦) = (𝑥 / 1))
87eqeq2d 2152 . . . . . 6 (𝑦 = 1 → (𝐴 = (𝑥 / 𝑦) ↔ 𝐴 = (𝑥 / 1)))
98rspcev 2794 . . . . 5 ((1 ∈ ℕ ∧ 𝐴 = (𝑥 / 1)) → ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
106, 9mpan 421 . . . 4 (𝐴 = (𝑥 / 1) → ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
115, 10syl6bi 162 . . 3 (𝑥 ∈ ℤ → (𝑥 = 𝐴 → ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦)))
1211reximia 2531 . 2 (∃𝑥 ∈ ℤ 𝑥 = 𝐴 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
13 risset 2467 . 2 (𝐴 ∈ ℤ ↔ ∃𝑥 ∈ ℤ 𝑥 = 𝐴)
14 elq 9464 . 2 (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
1512, 13, 143imtr4i 200 1 (𝐴 ∈ ℤ → 𝐴 ∈ ℚ)