Homework 7

1. (hard) Show that $\lnot(P\to Q)$ is logically equivalent to $P\land \lnot Q$.

   Write this problem only in Lean, not on paper.

2. Show that it is not true that for all rational numbers $x$, we have $2x^2\geq x$.

3. Let $n$ be a natural number. Show that $6^n$ is congruent to either $1$ or $6$ modulo 7.

4. Let $n$ be a natural number. Show that $4^n$ is congruent to either $1$, $2$ or $4$ modulo 7.

5. (hard) Let $a\geq -1$ be a real number. Show that it is not true that there exists a natural number $n$, such that $(1+a)^n<1+na$.

6. Show that for all natural numbers $n$ sufficiently large, $3^n \geq 2^n + 100$.

Notes

For 1, the point of the exercise is that you are proving the lemma not_imp, from Table 5.1. So don't use that lemma or the tactic push_neg which depends on it; instead prove this from scratch. You will need to use the law of the excluded middle (the tactic by_cases).

For 2 and 5, please give a proof which begins with negation-normalization. In Lean this is the tactic push_neg. On paper your proof will begin, "It suffices to prove that ..." (and then state the logically equivalent goal obtained by negation-normalization).

For 6, in Lean, you may need to explicitly specify the number type for the first appearance of the "3" in each part of the problem: (3:ℤ). (Note how this is done in the problem statement.)