m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
h : 0 = ∏ k in Finset.range n, (m - ↑k)
⊢ m ∈ Ico 0 ↑n
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
⊢ 0 < ∏ k in Finset.range n, (m - ↑k)
refine' (int_prod_range_nonneg m n hn).lt_of_ne fun h => hm _
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
h : ∃ a, a ∈ Finset.range n ∧ m - ↑a = 0
⊢ m ∈ Ico 0 ↑n
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
h : 0 = ∏ k in Finset.range n, (m - ↑k)
⊢ m ∈ Ico 0 ↑n
rw [eq_comm, Finset.prod_eq_zero_iff] at h
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ m ∈ Ico 0 ↑n
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
h : ∃ a, a ∈ Finset.range n ∧ m - ↑a = 0
⊢ m ∈ Ico 0 ↑n
obtain ⟨a, ha, h⟩ := h
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ ↑a ∈ Ico 0 ↑n
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ m ∈ Ico 0 ↑n
rw [sub_eq_zero.1 h]
no goals
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ ↑a ∈ Ico 0 ↑n
exact ⟨Int.ofNat_zero_le _, Int.ofNat_lt.2 <| Finset.mem_range.1 ha⟩