Theorem: Imo1964P1.imo_1964_p1b' (Compfiles/Imo1964P1.lean)

State before:
⊢ (2 ^ 2 + 1) % 7 ≠ 0
Tactic:
decide
State after:
no goals

State before:
n : ℕ
⊢ (2 ^ (n + 3) + 1) % 7 ≠ 0
Tactic:
rw [pow_add, Nat.add_mod, Nat.mul_mod, show 2 ^ 3 % 7 = 1 by rfl]
State after:
n : ℕ
⊢ (2 ^ n % 7 * 1 % 7 + 1 % 7) % 7 ≠ 0

State before:
n : ℕ
⊢ (2 ^ n % 7 * 1 % 7 + 1 % 7) % 7 ≠ 0
Tactic:
simp [imo_1964_p1b' n]
State after:
no goals

State before:
n : ℕ
⊢ 2 ^ 3 % 7 = 1
Tactic:
rfl
State after:
no goals