clear h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
⊢ False
a b c : ℤθ
n : ℕ
j : 1 ≤ n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
⊢ False