| Step | Hyp | Ref
| Expression |
| 1 | | elq 12992 |
. . 3
⊢ (𝐴 ∈ ℚ ↔
∃𝑥 ∈ ℤ
∃𝑦 ∈ ℕ
𝐴 = (𝑥 / 𝑦)) |
| 2 | | nnne0 12300 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0) |
| 3 | 2 | ancli 548 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ ∧ 𝑦 ≠ 0)) |
| 4 | | neeq1 3003 |
. . . . . . . . . 10
⊢ (𝐴 = (𝑥 / 𝑦) → (𝐴 ≠ 0 ↔ (𝑥 / 𝑦) ≠ 0)) |
| 5 | | zcn 12618 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 6 | | nncn 12274 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
| 7 | 5, 6 | anim12i 613 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑥 ∈ ℂ ∧ 𝑦 ∈
ℂ)) |
| 8 | | divne0b 11933 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 ≠ 0 ↔ (𝑥 / 𝑦) ≠ 0)) |
| 9 | 8 | 3expa 1119 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑦 ≠ 0) → (𝑥 ≠ 0 ↔ (𝑥 / 𝑦) ≠ 0)) |
| 10 | 7, 9 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) → (𝑥 ≠ 0 ↔ (𝑥 / 𝑦) ≠ 0)) |
| 11 | 10 | bicomd 223 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) → ((𝑥 / 𝑦) ≠ 0 ↔ 𝑥 ≠ 0)) |
| 12 | 4, 11 | sylan9bbr 510 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 ≠ 0 ↔ 𝑥 ≠ 0)) |
| 13 | | nnz 12634 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 14 | | zmulcl 12666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ) |
| 15 | 13, 14 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑥 · 𝑦) ∈ ℤ) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (𝑥 · 𝑦) ∈ ℤ) |
| 17 | | msqznn 12700 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → (𝑥 · 𝑥) ∈ ℕ) |
| 18 | 17 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → (𝑥 · 𝑥) ∈ ℕ) |
| 19 | 16, 18 | jca 511 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
| 20 | 19 | adantlr 715 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
| 21 | 20 | adantlr 715 |
. . . . . . . . . . 11
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → ((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ)) |
| 22 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝐴 = (𝑥 / 𝑦) → (1 / 𝐴) = (1 / (𝑥 / 𝑦))) |
| 23 | | divid 11953 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑥 / 𝑥) = 1) |
| 25 | 24 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = (1 / (𝑥 / 𝑦))) |
| 26 | | simpll 767 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → 𝑥 ∈
ℂ) |
| 27 | | simpl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
| 28 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) |
| 29 | | divdivdiv 11968 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) ∧ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
| 30 | 26, 27, 27, 28, 29 | syl22anc 839 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → ((𝑥 / 𝑥) / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
| 31 | 25, 30 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
| 32 | 31 | an4s 660 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
| 33 | 7, 32 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0)) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
| 34 | 33 | anass1rs 655 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝑥 ≠ 0) → (1 / (𝑥 / 𝑦)) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
| 35 | 22, 34 | sylan9eqr 2799 |
. . . . . . . . . . . 12
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝑥 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
| 36 | 35 | an32s 652 |
. . . . . . . . . . 11
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) |
| 37 | 21, 36 | jca 511 |
. . . . . . . . . 10
⊢
(((((𝑥 ∈
ℤ ∧ 𝑦 ∈
ℕ) ∧ 𝑦 ≠ 0)
∧ 𝐴 = (𝑥 / 𝑦)) ∧ 𝑥 ≠ 0) → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))) |
| 38 | 37 | ex 412 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝑥 ≠ 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))))) |
| 39 | 12, 38 | sylbid 240 |
. . . . . . . 8
⊢ ((((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) ∧ 𝐴 = (𝑥 / 𝑦)) → (𝐴 ≠ 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))))) |
| 40 | 39 | ex 412 |
. . . . . . 7
⊢ (((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) ∧ 𝑦 ≠ 0) → (𝐴 = (𝑥 / 𝑦) → (𝐴 ≠ 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
| 41 | 40 | anasss 466 |
. . . . . 6
⊢ ((𝑥 ∈ ℤ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ≠ 0)) → (𝐴 = (𝑥 / 𝑦) → (𝐴 ≠ 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
| 42 | 3, 41 | sylan2 593 |
. . . . 5
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → (𝐴 ≠ 0 → (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥)))))) |
| 43 | | rspceov 7480 |
. . . . . . 7
⊢ (((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ (1 / 𝐴) = (𝑧 / 𝑤)) |
| 44 | 43 | 3expa 1119 |
. . . . . 6
⊢ ((((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℕ (1 / 𝐴) = (𝑧 / 𝑤)) |
| 45 | | elq 12992 |
. . . . . 6
⊢ ((1 /
𝐴) ∈ ℚ ↔
∃𝑧 ∈ ℤ
∃𝑤 ∈ ℕ (1
/ 𝐴) = (𝑧 / 𝑤)) |
| 46 | 44, 45 | sylibr 234 |
. . . . 5
⊢ ((((𝑥 · 𝑦) ∈ ℤ ∧ (𝑥 · 𝑥) ∈ ℕ) ∧ (1 / 𝐴) = ((𝑥 · 𝑦) / (𝑥 · 𝑥))) → (1 / 𝐴) ∈ ℚ) |
| 47 | 42, 46 | syl8 76 |
. . . 4
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → (𝐴 ≠ 0 → (1 / 𝐴) ∈ ℚ))) |
| 48 | 47 | rexlimivv 3201 |
. . 3
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℕ 𝐴 = (𝑥 / 𝑦) → (𝐴 ≠ 0 → (1 / 𝐴) ∈ ℚ)) |
| 49 | 1, 48 | sylbi 217 |
. 2
⊢ (𝐴 ∈ ℚ → (𝐴 ≠ 0 → (1 / 𝐴) ∈
ℚ)) |
| 50 | 49 | imp 406 |
1
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℚ) |