Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) ) |
2 |
|
simpll |
⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ e = ( 𝑝 / 𝑞 ) ) → 𝑝 ∈ ℤ ) |
3 |
|
simplr |
⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ e = ( 𝑝 / 𝑞 ) ) → 𝑞 ∈ ℕ ) |
4 |
|
simpr |
⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ e = ( 𝑝 / 𝑞 ) ) → e = ( 𝑝 / 𝑞 ) ) |
5 |
1 2 3 4
|
eirrlem |
⊢ ¬ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ e = ( 𝑝 / 𝑞 ) ) |
6 |
5
|
imnani |
⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ¬ e = ( 𝑝 / 𝑞 ) ) |
7 |
6
|
nrexdv |
⊢ ( 𝑝 ∈ ℤ → ¬ ∃ 𝑞 ∈ ℕ e = ( 𝑝 / 𝑞 ) ) |
8 |
7
|
nrex |
⊢ ¬ ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ e = ( 𝑝 / 𝑞 ) |
9 |
|
elq |
⊢ ( e ∈ ℚ ↔ ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ e = ( 𝑝 / 𝑞 ) ) |
10 |
8 9
|
mtbir |
⊢ ¬ e ∈ ℚ |
11 |
10
|
nelir |
⊢ e ∉ ℚ |