Real.cos N cannot be 1

Stream: Is there code for X?

[Christian K]

How can i prove that there is no Natural Number n, so that Real.cos n = 1.

I have this set A

def A : Set r_3 := {w : r_3 | ∃ n : ℕ, w = ![Real.cos n, Real.sin n, 0]}

and i want to prove that ![1,0,0] is not in this set

lemma origin_not_in_A : ![1,0,0] ∉ A := by

btw, r_3 is defined as

abbrev r_3 := Fin 3 -> ℝ

And, while were at it, is there a smarter way to define A ?

[David Renshaw]

this could help: docs#Real.cos_eq_one_iff

[Edward van de Meent]

isn't this just not true because of n=0?

[Christian K]

Ohh, right, i forgot, n cannot be 0

[Edward van de Meent]

i think your proof will hinge on pi being irrational, and i'm not sure we have that... a quick search didn't reveal any such lemmas...

[Christian K]

Yeah, i found some stuff with irrational numbers. But there is nothing about Pi being irrational? And this also doesn't sound like something that would be very easy?

[Christian K]

Ok it seems like there is a github issue about this but it is still open...

[Edward van de Meent]

out of curiosity, what do you need this result for?

[Christian K]

The big project is formalizing the Banach Tarski Paradox, i need this specific lemma for Proving that a Circle is equidecomposable

[Edward van de Meent]

it might be the case that we do have the tools for proving pi is irrational...
maybe have a look at https://en.wikipedia.org/wiki/Proof_that_%CF%80_is_irrational and see if one of those is viable?

[Eric Wieser]

@loogle Irrational, Real.pi

[loogle]

:shrug: nothing found

[Ruben Van de Velde]

#6718 includes it

[Christian K]

OK, this look intersting, I'll look if i can contribute something helpfull.

[Kevin Buzzard]

Why don't you use another irrational number and rescale?

[Christian K]

How would i do that?

[Kevin Buzzard]

If you want to prove some geometric fact about the circle then my guess is that irrationality of pi is irrelevant (I'm working on some distant memory of having worked through Banach-Tarski years ago) so I'm suggesting that if you understand the proof and believe me then just modify it so that it relies on some other number like $\sqrt{2}$ being irrational instead. I might be wrong but if I'm right then this might well be the simplest solution. Don't you just need some dense infinite set which is sent to a proper subset of itself after a rotation, or something? This has nothing to do with irrationality of pi.

[Christian K]

Ohhh, yeah i see, this could work, thank you very much for this idea. I'll try it and let you know if it works