## Stream: new members

### Topic: 4 | 2 → false

#### Jia Ming (Oct 13 2020 at 10:07):

Hello, may I have some hints as to how to solve these simple questions? I've tried many powerful tactics but all seem to fail :(

example : (4 ∣ 2) → false := sorry
example : (∃ i : ℤ, (1/2 : ℝ) = ↑i) → false := sorry


#### Kenny Lau (Oct 13 2020 at 10:10):

the first one decidable, so dec_trivial

#### Kenny Lau (Oct 13 2020 at 10:11):

... and the second one can be reduced to the first one :P

#### Jia Ming (Oct 13 2020 at 10:19):

Ooo wow thank you!!!

#### Jia Ming (Oct 13 2020 at 10:23):

Umm huh, what exactly do u mean by reduced to the first one?

#### Kenny Lau (Oct 13 2020 at 10:28):

well you can prove that 2 * i = 1 given the assumption

#### Kenny Lau (Oct 13 2020 at 10:28):

which will allow you to deduce 2 \| 1

#### Kenny Lau (Oct 13 2020 at 10:28):

so it reduces to the first one

Ooh rightt

#### Mario Carneiro (Oct 13 2020 at 10:35):

Hm, this didn't go as smoothly as I would hope

example : (∃ i : ℤ, (1/2 : ℝ) = ↑i) → false :=
begin
rintro ⟨i, h⟩,
have : (1/2 : ℚ) = i,
{ rw ← @rat.cast_inj ℝ,
simpa using h },
have := congr_arg rat.denom this,
simp at this,
cases this
end


#### Mario Carneiro (Oct 13 2020 at 10:37):

Kenny's proof goes a little better

example : (∃ i : ℤ, (1/2 : ℝ) = ↑i) → false :=
begin
rintro ⟨i, h⟩,
field_simp at h,
norm_cast at h,
have : (2:ℤ) ∣ 1 := ⟨i, by simpa [mul_comm] using h⟩,
exact absurd this dec_trivial
end


Awesome! Thanks

#### Shing Tak Lam (Oct 13 2020 at 12:01):

slightly different approach, I showed if there was such an integer, it'd be between 0 and 1.

example : (∃ i : ℤ, (1/2 : ℝ) = ↑i) → false :=
begin
rintro ⟨x, hx⟩,
have h1 : (0 : ℝ) < x, linarith,
have h2 : (x : ℝ) < 1, linarith,
norm_cast at h1 h2,
linarith,
end


Last updated: May 14 2021 at 23:14 UTC