> On Wednesday, 30 July 2014 23:53:07 UTC+2, Ben Bacarisse wrote: > >> As you one asked me "please formulate them in the correct way like >> forall x in X exists y in Y : y = f(x) in order to avoid misreading". >> > For every k in |N there is n_0 in |N such that for n >= n_0: (n-k, n] > c s_n, i.e., an interval that does not contain rational numbers > indexed by n or smaller naturals.
So we're getting somewhere: one of the two contradictory statements, P and not(P) that you can prove is the theorem in 533. Now all you have to do now is prove its negation and you are done.
Since this is set theory and not WMaths, I can help. The final part of the theorem is still not written "in the correct way" as you put it but that's easy enough to fix. I think you mean "forall n c N: n >= n_0 => (n-k, n] c s_n" at the end. If I have that right, you are claiming to have a proof that
exists k c N: forall n_0 c N: exists n c N: n >= n_0 and not((n-k, n] c s_n)
or any of the many equivalent forms (again, assuming I've got the negation right). Can we see this proof you claim to have?