Theorem: exercise4_5 (LeanCourse/Assignments/Assignment4.lean)

State before:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
⊢ Nat.Prime n
Tactic:
by_contra h2n
State after:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
h2n : ¬Nat.Prime n
⊢ False

State before:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
h2n : ¬Nat.Prime n
⊢ False
Tactic:
rw [exercise4_4] at h2n
State after:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
h2n : n = 0 ∨ n = 1 ∨ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
⊢ False

State before:
n : ℕ
hn : Nat.Prime (2 ^ n - 1)
h2n : n = 0 ∨ n = 1 ∨ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
⊢ False
Tactic:
obtain rfl|rfl|⟨a, b, ha, hb, rfl⟩ := h2n
State after:
case inl
hn : Nat.Prime (2 ^ 0 - 1)
⊢ False

case inr.inl
hn : Nat.Prime (2 ^ 1 - 1)
⊢ False

case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ False
Tactic:
have h : (2 : ℤ) ^ a - 1 ∣ (2 : ℤ) ^ (a * b) - 1
State after:
case h
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ a - 1 ∣ 2 ^ (a * b) - 1

case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Tactic:
have h2 : 2 ^ 2 ≤ 2 ^ a := by sorry
State after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
⊢ False
Tactic:
have h3 : 1 ≤ 2 ^ a := by sorry
State after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ False
Tactic:
have h4 : 2 ^ a - 1 ≠ 1 := by zify; simp [h3]; linarith
State after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ False
Tactic:
have h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1 := by
  apply tsub_lt_tsub_right_of_le h3
  sorry
State after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
⊢ False
Tactic:
have h6' : 2 ^ 0 ≤ 2 ^ (a * b) := by sorry
State after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
⊢ False
Tactic:
have h6 : 1 ≤ 2 ^ (a * b) := h6'
State after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
⊢ False
Tactic:
have h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
State after:
case h'
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
⊢ 2 ^ a - 1 ∣ 2 ^ (a * b) - 1

case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Tactic:
rw [Nat.prime_def_lt] at hn
State after:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : 2 ≤ 2 ^ (a * b) - 1 ∧ ∀ m < 2 ^ (a * b) - 1, m ∣ 2 ^ (a * b) - 1 → m = 1
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False

State before:
case inr.inr.intro.intro.intro.intro
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : 2 ≤ 2 ^ (a * b) - 1 ∧ ∀ m < 2 ^ (a * b) - 1, m ∣ 2 ^ (a * b) - 1 → m = 1
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
h' : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ False
Tactic:
sorry
State after:
no goals

State before:
case inl
hn : Nat.Prime (2 ^ 0 - 1)
⊢ False
Tactic:
sorry
State after:
no goals

State before:
case inr.inl
hn : Nat.Prime (2 ^ 1 - 1)
⊢ False
Tactic:
sorry
State after:
no goals

State before:
case h
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
Tactic:
rw [← Int.modEq_zero_iff_dvd]
State after:
case h
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ (a * b) - 1 ≡ 0 [ZMOD 2 ^ a - 1]

State before:
case h
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ (a * b) - 1 ≡ 0 [ZMOD 2 ^ a - 1]
Tactic:
calc (2 : ℤ) ^ (a * b) - 1
    ≡ ((2 : ℤ) ^ a) ^ b - 1 [ZMOD (2 : ℤ) ^ a - 1] := by sorry
  _ ≡ (1 : ℤ) ^ b - 1 [ZMOD (2 : ℤ) ^ a - 1] := by sorry
  _ ≡ 0 [ZMOD (2 : ℤ) ^ a - 1] := by sorry
State after:
no goals

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 2 ^ (a * b) - 1 ≡ (2 ^ a) ^ b - 1 [ZMOD 2 ^ a - 1]
Tactic:
sorry
State after:
no goals

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ (2 ^ a) ^ b - 1 ≡ 1 ^ b - 1 [ZMOD 2 ^ a - 1]
Tactic:
sorry
State after:
no goals

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
⊢ 1 ^ b - 1 ≡ 0 [ZMOD 2 ^ a - 1]
Tactic:
sorry
State after:
no goals

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
⊢ 2 ^ 2 ≤ 2 ^ a
Tactic:
sorry
State after:
no goals

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
⊢ 1 ≤ 2 ^ a
Tactic:
sorry
State after:
no goals

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ 2 ^ a - 1 ≠ 1
Tactic:
zify
State after:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ ↑(2 ^ a - 1) ≠ 1

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ ↑(2 ^ a - 1) ≠ 1
Tactic:
simp [h3]
State after:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ ¬2 ^ a - 1 = 1

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
⊢ ¬2 ^ a - 1 = 1
Tactic:
linarith
State after:
no goals

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ 2 ^ a - 1 < 2 ^ (a * b) - 1
Tactic:
apply tsub_lt_tsub_right_of_le h3
State after:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ 2 ^ a < 2 ^ (a * b)

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
⊢ 2 ^ a < 2 ^ (a * b)
Tactic:
sorry
State after:
no goals

State before:
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
⊢ 2 ^ 0 ≤ 2 ^ (a * b)
Tactic:
sorry
State after:
no goals

State before:
case h'
a b : ℕ
ha : 2 ≤ a
hb : 2 ≤ b
hn : Nat.Prime (2 ^ (a * b) - 1)
h : 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
h2 : 2 ^ 2 ≤ 2 ^ a
h3 : 1 ≤ 2 ^ a
h4 : 2 ^ a - 1 ≠ 1
h5 : 2 ^ a - 1 < 2 ^ (a * b) - 1
h6' : 2 ^ 0 ≤ 2 ^ (a * b)
h6 : 1 ≤ 2 ^ (a * b)
⊢ 2 ^ a - 1 ∣ 2 ^ (a * b) - 1
Tactic:
norm_cast at h
State after:
no goals