[GOAL]
p : ℕ
pp : Prime p
m : ℕ
hm : m ∣ p
⊢ m = 1 ∨ m = p
[PROOFSTEP]
obtain ⟨n, hn⟩ := hm
[GOAL]
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
⊢ m = 1 ∨ m = p
[PROOFSTEP]
have := pp.isUnit_or_isUnit hn
[GOAL]
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : IsUnit m ∨ IsUnit n
⊢ m = 1 ∨ m = p
[PROOFSTEP]
rw [Nat.isUnit_iff, Nat.isUnit_iff] at this 
[GOAL]
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ m = 1 ∨ m = p
[PROOFSTEP]
apply Or.imp_right _ this
[GOAL]
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ n = 1 → m = p
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = p
[PROOFSTEP]
rw [hn, mul_one]
[GOAL]
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
[PROOFSTEP]
refine'
  ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => _⟩
    -- Porting note: needed to make ℕ explicit
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p
[PROOFSTEP]
have h1 := (@one_lt_two ℕ ..).trans_le h.1
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p
[PROOFSTEP]
refine' ⟨mt Nat.isUnit_iff.mp h1.ne', fun a b hab => _⟩
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ IsUnit a ∨ IsUnit b
[PROOFSTEP]
simp only [Nat.isUnit_iff]
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = 1 ∨ b = 1
[PROOFSTEP]
apply Or.imp_right _ (h.2 a _)
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a = p → b = 1
[PROOFSTEP]
rintro rfl
[GOAL]
a b : ℕ
h : 2 ≤ a ∧ ∀ (m : ℕ), m ∣ a → m = 1 ∨ m = a
h1 : 1 < a
hab : a = a * b
⊢ b = 1
[PROOFSTEP]
rw [← mul_right_inj' (pos_of_gt h1).ne', ← hab, mul_one]
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ p
[PROOFSTEP]
rw [hab]
[GOAL]
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
a b : ℕ
hab : p = a * b
⊢ a ∣ a * b
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : m < p → m ∣ p → m = 1
m2 : 2 ≤ m
l : m < p
d : m ∣ p
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m → m < p → ¬m ∣ p
l : m < p
d : m ∣ p
⊢ m = 1
[PROOFSTEP]
rcases m with (_ | _ | m)
[GOAL]
case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ zero = 1
[PROOFSTEP]
rw [eq_zero_of_zero_dvd d] at p2 
[GOAL]
case zero
p : ℕ
p2 : 2 ≤ 0
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ zero = 1
[PROOFSTEP]
revert p2
[GOAL]
case zero
p : ℕ
h : 2 ≤ zero → zero < p → ¬zero ∣ p
l : zero < p
d : zero ∣ p
⊢ 2 ≤ 0 → zero = 1
[PROOFSTEP]
decide
[GOAL]
case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ succ zero → succ zero < p → ¬succ zero ∣ p
l : succ zero < p
d : succ zero ∣ p
⊢ succ zero = 1
[PROOFSTEP]
rfl
[GOAL]
case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ succ (succ m) → succ (succ m) < p → ¬succ (succ m) ∣ p
l : succ (succ m) < p
d : succ (succ m) ∣ p
⊢ succ (succ m) = 1
[PROOFSTEP]
exact (h le_add_self l).elim d
[GOAL]
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
⊢ False
[PROOFSTEP]
cases' le_total m k with mk km
[GOAL]
case inl
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
mk : m ≤ k
⊢ False
[PROOFSTEP]
exact this mk m2 e
[GOAL]
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = m * k
km : k ≤ m
⊢ False
[PROOFSTEP]
rw [mul_comm] at e 
[GOAL]
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ False
[PROOFSTEP]
refine' this km (lt_of_mul_lt_mul_right _ (zero_le m)) e
[GOAL]
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt p → ¬m ∣ p
this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ : m ∣ p
k : ℕ
e : p = k * m
km : k ≤ m
⊢ 1 * m < k * m
[PROOFSTEP]
rwa [one_mul, ← e]
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
⊢ Prime n
[PROOFSTEP]
refine' prime_def_lt.mpr ⟨h1, fun m mlt mdvd => _⟩
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m = 1
[PROOFSTEP]
have hm : m ≠ 0 := by
  rintro rfl
  rw [zero_dvd_iff] at mdvd 
  exact mlt.ne' mdvd
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False
[PROOFSTEP]
rw [zero_dvd_iff] at mdvd 
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
mlt : 0 < n
mdvd : n = 0
⊢ False
[PROOFSTEP]
exact mlt.ne' mdvd
[GOAL]
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → coprime n m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1
[PROOFSTEP]
exact (h m mlt hm).symm.eq_one_of_dvd mdvd
[GOAL]
⊢ Prime 2
[PROOFSTEP]
decide
[GOAL]
⊢ Prime 3
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
⊢ 5 ≤ p
[PROOFSTEP]
by_contra' h
[GOAL]
p : ℕ
hp : Prime p
h_two : p ≠ 2
h_three : p ≠ 3
h : p < 5
⊢ False
[PROOFSTEP]
revert h_two h_three hp
[GOAL]
p : ℕ
h : p < 5
⊢ Prime p → p ≠ 2 → p ≠ 3 → False
[PROOFSTEP]
match p with
| 0 => decide
| 1 => decide
| 2 => decide
| 3 => decide
| 4 => decide
| n + 5 => exact (h.not_le le_add_self).elim
[GOAL]
p : ℕ
h : 0 < 5
⊢ Prime 0 → 0 ≠ 2 → 0 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p : ℕ
h : 1 < 5
⊢ Prime 1 → 1 ≠ 2 → 1 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p : ℕ
h : 2 < 5
⊢ Prime 2 → 2 ≠ 2 → 2 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p : ℕ
h : 3 < 5
⊢ Prime 3 → 3 ≠ 2 → 3 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p : ℕ
h : 4 < 5
⊢ Prime 4 → 4 ≠ 2 → 4 ≠ 3 → False
[PROOFSTEP]
decide
[GOAL]
p n : ℕ
h : n + 5 < 5
⊢ Prime (n + 5) → n + 5 ≠ 2 → n + 5 ≠ 3 → False
[PROOFSTEP]
exact (h.not_le le_add_self).elim
[GOAL]
a b : ℕ
a1 : 1 < a
b1 : 1 < b
h : Prime (a * b)
⊢ a * 1 = a * b
[PROOFSTEP]
simpa using (dvd_prime_two_le h a1).1 (dvd_mul_right _ _)
[GOAL]
a b n : ℕ
h : a * b = n
h₁ : 1 < a
h₂ : 1 < b
⊢ ¬Prime n
[PROOFSTEP]
rw [← h]
[GOAL]
a b n : ℕ
h : a * b = n
h₁ : 1 < a
h₂ : 1 < b
⊢ ¬Prime (a * b)
[PROOFSTEP]
exact not_prime_mul h₁ h₂
[GOAL]
a b : ℕ
⊢ Prime (a * b) ↔ Prime a ∧ b = 1 ∨ Prime b ∧ a = 1
[PROOFSTEP]
simp only [iff_self_iff, irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]
[GOAL]
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p ↔ p = a
[PROOFSTEP]
refine'
  ⟨_, by
    rintro rfl
    rfl⟩
[GOAL]
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ p = a → a ∣ p
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℕ
hp : Prime p
a1 : p ≠ 1
⊢ p ∣ p
[PROOFSTEP]
rfl
[GOAL]
p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ a ∣ p → p = a
[PROOFSTEP]
rintro ⟨j, rfl⟩
[GOAL]
case intro
a : ℕ
a1 : a ≠ 1
j : ℕ
hp : Prime (a * j)
⊢ a * j = a
[PROOFSTEP]
rcases prime_mul_iff.mp hp with (⟨_, rfl⟩ | ⟨_, rfl⟩)
[GOAL]
case intro.inl.intro
a : ℕ
a1 : a ≠ 1
left✝ : Prime a
hp : Prime (a * 1)
⊢ a * 1 = a
[PROOFSTEP]
exact mul_one _
[GOAL]
case intro.inr.intro
j : ℕ
left✝ : Prime j
a1 : 1 ≠ 1
hp : Prime (1 * j)
⊢ 1 * j = 1
[PROOFSTEP]
exact (a1 rfl).elim
[GOAL]
n k : ℕ
h : ¬n < k * k
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ Nat.minFacProp n (minFacAux n x✝)
[PROOFSTEP]
rw [minFacAux]
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
⊢ Nat.minFacProp n
    (if h : n < x✝ * x✝ then n
    else
      if x✝ ∣ n then x✝
      else
        let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝);
        minFacAux n (x✝ + 2))
[PROOFSTEP]
by_cases h : n < k * k
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ Nat.minFacProp n
    (if h : n < x✝ * x✝ then n
    else
      if x✝ ∣ n then x✝
      else
        let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝);
        minFacAux n (x✝ + 2))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ Nat.minFacProp n
    (if h : n < x✝ * x✝ then n
    else
      if x✝ ∣ n then x✝
      else
        let_fun this := (_ : sqrt n - x✝ < sqrt n + 2 - x✝);
        minFacAux n (x✝ + 2))
[PROOFSTEP]
simp [h]
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ Nat.minFacProp n n
[PROOFSTEP]
have pp : Prime n := prime_def_le_sqrt.2 ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
pp : Prime n
⊢ Nat.minFacProp n n
[PROOFSTEP]
exact ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
[PROOFSTEP]
have k2 : 2 ≤ k := by
  subst e
  apply Nat.le_add_left
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
[PROOFSTEP]
subst e
[GOAL]
n : ℕ
n2 : 2 ≤ n
i : ℕ
k : ℕ := 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
[PROOFSTEP]
by_cases dk : k ∣ n
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
[PROOFSTEP]
simp [dk]
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ Nat.minFacProp n (if x✝ ∣ n then x✝ else minFacAux n (x✝ + 2))
[PROOFSTEP]
simp [dk]
[GOAL]
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ Nat.minFacProp n x✝
[PROOFSTEP]
exact ⟨k2, dk, a⟩
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ Nat.minFacProp n (minFacAux n (x✝ + 2))
[PROOFSTEP]
refine'
  have := minFac_lemma n k h
  minFacAux_has_prop n2 (k + 2) (i + 1) (by simp [e, left_distrib]) fun m m2 d => _
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3
[PROOFSTEP]
simp [e, left_distrib]
[GOAL]
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ k + 2 ≤ m
[PROOFSTEP]
cases' Nat.eq_or_lt_of_le (a m m2 d) with me ml
[GOAL]
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
me : x✝ = m
⊢ k + 2 ≤ m
[PROOFSTEP]
subst me
[GOAL]
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m2 : 2 ≤ x✝
d : x✝ ∣ n
⊢ k + 2 ≤ x✝
[PROOFSTEP]
contradiction
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ k + 2 ≤ m
[PROOFSTEP]
apply (Nat.eq_or_lt_of_le ml).resolve_left
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ ¬succ x✝ = m
[PROOFSTEP]
intro me
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
me : succ x✝ = m
⊢ False
[PROOFSTEP]
rw [← me, e] at d 
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
⊢ False
[PROOFSTEP]
have d' : 2 * (i + 2) ∣ n := d
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
⊢ False
[PROOFSTEP]
have := a _ le_rfl (dvd_of_mul_right_dvd d')
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : x✝ ≤ 2
⊢ False
[PROOFSTEP]
rw [e] at this 
[GOAL]
case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ False
[PROOFSTEP]
exact absurd this (by contradiction)
[GOAL]
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : sqrt n - k < sqrt n + 2 - k
m : ℕ
m2 : 2 ≤ m
d : succ (2 * i + 3) ∣ n
ml : x✝ < m
me : succ x✝ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
n1 : n ≠ 1
⊢ Nat.minFacProp n (minFac n)
[PROOFSTEP]
by_cases n0 : n = 0
[GOAL]
case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ Nat.minFacProp n (minFac n)
[PROOFSTEP]
simp [n0, minFacProp, GE.ge]
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ Nat.minFacProp n (minFac n)
[PROOFSTEP]
have n2 : 2 ≤ n := by
  revert n0 n1
  rcases n with (_ | _ | _) <;> simp [succ_le_succ]
[GOAL]
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ 2 ≤ n
[PROOFSTEP]
revert n0 n1
[GOAL]
n : ℕ
⊢ n ≠ 1 → ¬n = 0 → 2 ≤ n
[PROOFSTEP]
rcases n with (_ | _ | _)
[GOAL]
case zero
⊢ zero ≠ 1 → ¬zero = 0 → 2 ≤ zero
[PROOFSTEP]
simp [succ_le_succ]
[GOAL]
case succ.zero
⊢ succ zero ≠ 1 → ¬succ zero = 0 → 2 ≤ succ zero
[PROOFSTEP]
simp [succ_le_succ]
[GOAL]
case succ.succ
n✝ : ℕ
⊢ succ (succ n✝) ≠ 1 → ¬succ (succ n✝) = 0 → 2 ≤ succ (succ n✝)
[PROOFSTEP]
simp [succ_le_succ]
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (minFac n)
[PROOFSTEP]
simp [minFac_eq]
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else minFacAux n 3)
[PROOFSTEP]
by_cases d2 : 2 ∣ n
[GOAL]
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else minFacAux n 3)
[PROOFSTEP]
simp [d2]
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else minFacAux n 3)
[PROOFSTEP]
simp [d2]
[GOAL]
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ Nat.minFacProp n 2
[PROOFSTEP]
exact ⟨le_rfl, d2, fun k k2 _ => k2⟩
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ Nat.minFacProp n (minFacAux n 3)
[PROOFSTEP]
refine' minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt _ d2)
[GOAL]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n
[PROOFSTEP]
exact fun e => e.symm ▸ d
[GOAL]
n : ℕ
n1 : n = 1
⊢ minFac n ∣ n
[PROOFSTEP]
simp [n1]
[GOAL]
n : ℕ
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → minFac n ≤ m
[PROOFSTEP]
by_cases n1 : n = 1 <;> [exact fun m2 _ => n1.symm ▸ le_trans (by decide) m2; apply (minFac_has_prop n1).2.2]
[GOAL]
n : ℕ
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → minFac n ≤ m
[PROOFSTEP]
by_cases n1 : n = 1
[GOAL]
case pos
n m✝ : ℕ
n1 : n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → minFac n ≤ m✝
[PROOFSTEP]
exact fun m2 _ => n1.symm ▸ le_trans (by decide) m2
[GOAL]
n m✝ : ℕ
n1 : n = 1
m2 : 2 ≤ m✝
x✝ : m✝ ∣ n
⊢ minFac 1 ≤ 2
[PROOFSTEP]
decide
[GOAL]
case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → minFac n ≤ m✝
[PROOFSTEP]
apply (minFac_has_prop n1).2.2
[GOAL]
n : ℕ
⊢ 0 < minFac n
[PROOFSTEP]
by_cases n1 : n = 1 <;> [exact n1.symm ▸ (by decide); exact (minFac_prime n1).pos]
[GOAL]
n : ℕ
⊢ 0 < minFac n
[PROOFSTEP]
by_cases n1 : n = 1
[GOAL]
case pos
n : ℕ
n1 : n = 1
⊢ 0 < minFac n
[PROOFSTEP]
exact n1.symm ▸ (by decide)
[GOAL]
n : ℕ
n1 : n = 1
⊢ 0 < minFac 1
[PROOFSTEP]
decide
[GOAL]
case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < minFac n
[PROOFSTEP]
exact (minFac_prime n1).pos
[GOAL]
m n : ℕ
h : n = 1 ∨ m ≤ minFac n
p : ℕ
pp : Prime p
d : p ∣ n
⊢ n = 1 → m ≤ p
[PROOFSTEP]
rintro rfl
[GOAL]
m p : ℕ
pp : Prime p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
[PROOFSTEP]
cases pp.not_dvd_one d
[GOAL]
m n : ℕ
h : n = 1 ∨ m ≤ minFac n
p : ℕ
pp : 1 < p
d : p ∣ n
⊢ n = 1 → m ≤ p
[PROOFSTEP]
rintro rfl
[GOAL]
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
[PROOFSTEP]
cases not_le_of_lt pp (le_of_dvd (by decide) d)
[GOAL]
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ 0 < 1
[PROOFSTEP]
decide
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < n
[PROOFSTEP]
rw [h0, mul_zero]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < 0
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < 0
[PROOFSTEP]
decide
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = minFac n * 1
⊢ minFac n ≤ n / minFac n
[PROOFSTEP]
rw [mul_one] at h1 
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = minFac n
⊢ minFac n ≤ n / minFac n
[PROOFSTEP]
rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, or_false_iff, not_le] at np 
[GOAL]
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = minFac n
⊢ minFac n ≤ n / minFac n
[PROOFSTEP]
rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ n / minFac n
[PROOFSTEP]
conv_rhs =>
  congr
  rw [hx]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
| n / minFac n
[PROOFSTEP]
  congr
  rw [hx]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
| n / minFac n
[PROOFSTEP]
  congr
  rw [hx]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
| n / minFac n
[PROOFSTEP]
congr
[GOAL]
case a
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
| n
case a n : ℕ pos : 0 < n np : ¬Prime n x : ℕ hx : n = minFac n * (x + 2) | minFac n
[PROOFSTEP]
rw [hx]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ minFac n * (x + 2) / minFac n
[PROOFSTEP]
rw [Nat.mul_div_cancel_left _ (minFac_pos _)]
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ x + 2
[PROOFSTEP]
exact minFac_le_of_dvd (le_add_left 2 x) ⟨minFac n, by rwa [mul_comm]⟩
[GOAL]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ n = (x + 2) * minFac n
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
n : ℕ
⊢ minFac n = 1 ↔ n = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ minFac n = 1 → n = 1
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
h : minFac n = 1
⊢ n = 1
[PROOFSTEP]
by_contra hn
[GOAL]
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
⊢ False
[PROOFSTEP]
have := minFac_prime hn
[GOAL]
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
this : Prime (minFac n)
⊢ False
[PROOFSTEP]
rw [h] at this 
[GOAL]
case mp
n : ℕ
h : minFac n = 1
hn : ¬n = 1
this : Prime 1
⊢ False
[PROOFSTEP]
exact not_prime_one this
[GOAL]
case mpr
n : ℕ
⊢ n = 1 → minFac n = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
⊢ minFac 1 = 1
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ minFac n = 2 ↔ 2 ∣ n
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ minFac n = 2 → 2 ∣ n
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
h : minFac n = 2
⊢ 2 ∣ n
[PROOFSTEP]
rw [← h]
[GOAL]
case mp
n : ℕ
h : minFac n = 2
⊢ minFac n ∣ n
[PROOFSTEP]
exact minFac_dvd n
[GOAL]
case mpr
n : ℕ
⊢ 2 ∣ n → minFac n = 2
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
⊢ minFac n = 2
[PROOFSTEP]
have ub := minFac_le_of_dvd (le_refl 2) h
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
⊢ minFac n = 2
[PROOFSTEP]
have lb := minFac_pos n
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
⊢ minFac n = 2
[PROOFSTEP]
refine ub.eq_or_lt.resolve_right fun h' => ?_
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
⊢ False
[PROOFSTEP]
have := le_antisymm (Nat.succ_le_of_lt lb) (lt_succ_iff.mp h')
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
this : succ 0 = minFac n
⊢ False
[PROOFSTEP]
rw [eq_comm, Nat.minFac_eq_one_iff] at this 
[GOAL]
case mpr
n : ℕ
h : 2 ∣ n
ub : minFac n ≤ 2
lb : 0 < minFac n
h' : minFac n < 2
this : n = 1
⊢ False
[PROOFSTEP]
subst this
[GOAL]
case mpr
h : 2 ∣ 1
ub : minFac 1 ≤ 2
lb : 0 < minFac 1
h' : minFac 1 < 2
⊢ False
[PROOFSTEP]
exact not_lt_of_le (le_of_dvd zero_lt_one h) one_lt_two
[GOAL]
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
⊢ a ∣ b
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a 1
[GOAL]
case inl
b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ 1 → p * 1 ∣ b
⊢ 1 ∣ b
[PROOFSTEP]
apply one_dvd
[GOAL]
case inr
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
⊢ a ∣ b
[PROOFSTEP]
obtain ⟨p, hp⟩ := exists_prime_and_dvd ha
[GOAL]
case inr.intro
a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
ha : a ≠ 1
p : ℕ
hp : Prime p ∧ p ∣ a
⊢ a ∣ b
[PROOFSTEP]
exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)
[GOAL]
⊢ ¬BddAbove {p | Prime p}
[PROOFSTEP]
rw [not_bddAbove_iff]
[GOAL]
⊢ ∀ (x : ℕ), ∃ y, y ∈ {p | Prime p} ∧ x < y
[PROOFSTEP]
intro n
[GOAL]
n : ℕ
⊢ ∃ y, y ∈ {p | Prime p} ∧ n < y
[PROOFSTEP]
obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ
[GOAL]
case intro.intro
n p : ℕ
hi : succ n ≤ p
hp : Prime p
⊢ ∃ y, y ∈ {p | Prime p} ∧ n < y
[PROOFSTEP]
exact ⟨p, hp, hi⟩
[GOAL]
p : ℕ
hp : Prime p
h : p % 2 = 0
⊢ ¬2 = 1
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Prime p
⊢ Even p ↔ p = 2
[PROOFSTEP]
rw [even_iff_two_dvd, prime_dvd_prime_iff_eq prime_two hp, eq_comm]
[GOAL]
p : ℕ
hp : Prime p
h2 : p ≠ 2
n : ℕ
hn : p = 2 * n + 1
⊢ p - 1 = n + n
[PROOFSTEP]
rw [hn, Nat.add_sub_cancel, two_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
⊢ p % 2 = 1 ↔ p ≠ 2
[PROOFSTEP]
refine' ⟨fun h hf => _, (Nat.Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left⟩
[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
h : p % 2 = 1
hf : p = 2
⊢ False
[PROOFSTEP]
rw [hf] at h 
[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
h : 2 % 2 = 1
hf : p = 2
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ coprime m n
[PROOFSTEP]
rw [coprime_iff_gcd_eq_one]
[GOAL]
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
⊢ gcd m n = 1
[PROOFSTEP]
by_contra g2
[GOAL]
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
⊢ False
[PROOFSTEP]
obtain ⟨p, hp, hpdvd⟩ := exists_prime_and_dvd g2
[GOAL]
case intro.intro
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ False
[PROOFSTEP]
apply H p hp
[GOAL]
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ p ∣ m
[PROOFSTEP]
apply dvd_trans hpdvd
[GOAL]
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ p ∣ n
[PROOFSTEP]
apply dvd_trans hpdvd
[GOAL]
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ gcd m n ∣ m
[PROOFSTEP]
exact gcd_dvd_left _ _
[GOAL]
case intro.intro.a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬gcd m n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ gcd m n
⊢ gcd m n ∣ n
[PROOFSTEP]
exact gcd_dvd_right _ _
[GOAL]
k : ℕ
⊢ k + 2 ≠ 1
[PROOFSTEP]
apply Nat.ne_of_gt
[GOAL]
case h
k : ℕ
⊢ 1 < k + 2
[PROOFSTEP]
apply Nat.succ_lt_succ
[GOAL]
case h.a
k : ℕ
⊢ 0 < k + 1
[PROOFSTEP]
apply Nat.zero_lt_succ
[GOAL]
p n : ℕ
pp : Prime p
co : coprime p n
d : p ∣ n
⊢ p ∣ n * 1
[PROOFSTEP]
simp [d]
[GOAL]
m n : ℕ
⊢ ¬coprime m n ↔ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
m n : ℕ
⊢ ¬coprime m n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
[PROOFSTEP]
intro h
[GOAL]
case mp
m n : ℕ
h : ¬coprime m n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
[PROOFSTEP]
exact
  ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
    (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩
[GOAL]
case mpr
m n : ℕ
⊢ (∃ p, Prime p ∧ p ∣ m ∧ p ∣ n) → ¬coprime m n
[PROOFSTEP]
intro h
[GOAL]
case mpr
m n : ℕ
h : ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬coprime m n
[PROOFSTEP]
cases' h with p hp
[GOAL]
case mpr.intro
m n p : ℕ
hp : Prime p ∧ p ∣ m ∧ p ∣ n
⊢ ¬coprime m n
[PROOFSTEP]
apply Nat.not_coprime_of_dvd_of_dvd (Prime.one_lt hp.1) hp.2.1 hp.2.2
[GOAL]
p m n : ℕ
pp : Prime p
Hm : ¬p ∣ m
Hn : ¬p ∣ n
⊢ ¬(p ∣ m ∨ p ∣ n)
[PROOFSTEP]
simp [Hm, Hn]
[GOAL]
p m n : ℕ
pp : Prime p
h : p ∣ m ^ n
⊢ p ∣ m
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
p m n : ℕ
pp : Prime p
h✝ : p ∣ m ^ n
h : p ∣ m ^ zero
⊢ p ∣ m
[PROOFSTEP]
exact pp.not_dvd_one.elim h
[GOAL]
case succ
p m n✝ : ℕ
pp : Prime p
h✝ : p ∣ m ^ n✝
n : ℕ
IH : p ∣ m ^ n → p ∣ m
h : p ∣ m ^ succ n
⊢ p ∣ m
[PROOFSTEP]
rw [pow_succ] at h 
[GOAL]
case succ
p m n✝ : ℕ
pp : Prime p
h✝ : p ∣ m ^ n✝
n : ℕ
IH : p ∣ m ^ n → p ∣ m
h : p ∣ m ^ n * m
⊢ p ∣ m
[PROOFSTEP]
exact (pp.dvd_mul.1 h).elim IH id
[GOAL]
p a k : ℕ
hp : Prime p
⊢ a ^ k = p ↔ a = p ∧ k = 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by rw [h.1, h.2, pow_one]⟩
[GOAL]
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p
[PROOFSTEP]
rw [h.1, h.2, pow_one]
[GOAL]
p a k : ℕ
hp : Prime p
h : a ^ k = p
⊢ a = p ∧ k = 1
[PROOFSTEP]
rw [← h] at hp 
[GOAL]
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = p ∧ k = 1
[PROOFSTEP]
rw [← h, hp.eq_one_of_pow, eq_self_iff_true, and_true_iff, pow_one]
[GOAL]
n k : ℕ
hk : k ≠ 0
⊢ minFac (n ^ k) = minFac n
[PROOFSTEP]
rcases eq_or_ne n 1 with (rfl | hn)
[GOAL]
case inl
k : ℕ
hk : k ≠ 0
⊢ minFac (1 ^ k) = minFac 1
[PROOFSTEP]
simp
[GOAL]
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ minFac (n ^ k) = minFac n
[PROOFSTEP]
have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff hk).1 hk')
[GOAL]
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ minFac (n ^ k) = minFac n
[PROOFSTEP]
apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
[GOAL]
case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
hnk : n ^ k ≠ 1
⊢ minFac n ≤ minFac (n ^ k)
[PROOFSTEP]
apply minFac_le_of_dvd (minFac_prime hnk).two_le ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))
[GOAL]
p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ minFac (p ^ k) = p
[PROOFSTEP]
rw [Nat.pow_minFac hk, hp.minFac_eq]
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
⊢ x * y = p ^ 2 ↔ x = p ∧ y = p
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨h₁, h₂⟩ => h₁.symm ▸ h₂.symm ▸ (sq _).symm⟩
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ x = p ∧ y = p
[PROOFSTEP]
have pdvdxy : p ∣ x * y := by rw [h];
  simp [sq]
    -- Could be `wlog := hp.dvd_mul.1 pdvdxy using x y`, but that imports more than we want.
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ p ∣ x * y
[PROOFSTEP]
rw [h]
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
⊢ p ∣ p ^ 2
[PROOFSTEP]
simp [sq]
  -- Could be `wlog := hp.dvd_mul.1 pdvdxy using x y`, but that imports more than we want.
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
⊢ x = p ∧ y = p
[PROOFSTEP]
suffices ∀ x' y' : ℕ, x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p by
  obtain hx | hy := hp.dvd_mul.1 pdvdxy <;> [skip; rw [And.comm]] <;> [skip; rw [mul_comm] at h pdvdxy ] <;>
      apply this <;>
    assumption
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p
[PROOFSTEP]
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;> [skip; rw [And.comm]] <;> [skip; rw [mul_comm] at h pdvdxy ]
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p
[PROOFSTEP]
obtain hx | hy := hp.dvd_mul.1 pdvdxy <;> [skip; rw [And.comm]]
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
⊢ x = p ∧ y = p
[PROOFSTEP]
obtain hx | hy := hp.dvd_mul.1 pdvdxy
[GOAL]
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p
[PROOFSTEP]
skip
[GOAL]
case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ x = p ∧ y = p
[PROOFSTEP]
rw [And.comm]
[GOAL]
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p
[PROOFSTEP]
skip
[GOAL]
case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p
[PROOFSTEP]
rw [mul_comm] at h pdvdxy 
[GOAL]
case inl
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x = p ∧ y = p
[PROOFSTEP]
apply this
[GOAL]
case inr
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y = p ∧ x = p
[PROOFSTEP]
apply this
[GOAL]
case inl.a
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inl.a
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ y ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inl.a
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ x * y = p ^ 2
[PROOFSTEP]
assumption
[GOAL]
case inl.a
x y p : ℕ
hp : Prime p
hx✝ : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hx : p ∣ x
⊢ p ∣ x
[PROOFSTEP]
assumption
[GOAL]
case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ x ≠ 1
[PROOFSTEP]
assumption
[GOAL]
case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ y * x = p ^ 2
[PROOFSTEP]
assumption
[GOAL]
case inr.a
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy✝ : y ≠ 1
h : y * x = p ^ 2
pdvdxy : p ∣ y * x
this : ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
hy : p ∣ y
⊢ p ∣ y
[PROOFSTEP]
assumption
[GOAL]
x y p : ℕ
hp : Prime p
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
pdvdxy : p ∣ x * y
⊢ ∀ (x' y' : ℕ), x' ≠ 1 → y' ≠ 1 → x' * y' = p ^ 2 → p ∣ x' → x' = p ∧ y' = p
[PROOFSTEP]
rintro x y hx hy h ⟨a, ha⟩
[GOAL]
case intro
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
⊢ x = p ∧ y = p
[PROOFSTEP]
have : a ∣ p := ⟨y, by rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h ⟩
[GOAL]
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
⊢ p = a * y
[PROOFSTEP]
rwa [ha, sq, mul_assoc, mul_right_inj' hp.ne_zero, eq_comm] at h 
[GOAL]
case intro
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
⊢ x = p ∧ y = p
[PROOFSTEP]
obtain ha1 | hap := (Nat.dvd_prime hp).mp ‹a ∣ p›
[GOAL]
case intro.inl
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
ha1 : a = 1
⊢ x = p ∧ y = p
[PROOFSTEP]
subst ha1
[GOAL]
case intro.inl
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
ha : x = p * 1
this : 1 ∣ p
⊢ x = p ∧ y = p
[PROOFSTEP]
rw [mul_one] at ha 
[GOAL]
case intro.inl
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
ha : x = p
this : 1 ∣ p
⊢ x = p ∧ y = p
[PROOFSTEP]
subst ha
[GOAL]
case intro.inl
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
hp : Prime x
h✝ : x✝ * y✝ = x ^ 2
pdvdxy : x ∣ x✝ * y✝
h : x * y = x ^ 2
this : 1 ∣ x
⊢ x = x ∧ y = x
[PROOFSTEP]
simp only [sq, mul_right_inj' hp.ne_zero] at h 
[GOAL]
case intro.inl
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
hp : Prime x
h✝ : x✝ * y✝ = x ^ 2
pdvdxy : x ∣ x✝ * y✝
this : 1 ∣ x
h : y = x
⊢ x = x ∧ y = x
[PROOFSTEP]
subst h
[GOAL]
case intro.inl
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy hx : y ≠ 1
hp : Prime y
h : x * y✝ = y ^ 2
pdvdxy : y ∣ x * y✝
this : 1 ∣ y
⊢ y = y ∧ y = y
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
case intro.inr
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
hap : a = p
⊢ x = p ∧ y = p
[PROOFSTEP]
refine' (hy ?_).elim
[GOAL]
case intro.inr
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
h : x * y = p ^ 2
a : ℕ
ha : x = p * a
this : a ∣ p
hap : a = p
⊢ y = 1
[PROOFSTEP]
subst hap
[GOAL]
case intro.inr
x✝ y✝ : ℕ
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x✝ * y✝ = a ^ 2
pdvdxy : a ∣ x✝ * y✝
h : x * y = a ^ 2
ha : x = a * a
this : a ∣ a
⊢ y = 1
[PROOFSTEP]
subst ha
[GOAL]
case intro.inr
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x * y✝ = a ^ 2
pdvdxy : a ∣ x * y✝
this : a ∣ a
hx : a * a ≠ 1
h : a * a * y = a ^ 2
⊢ y = 1
[PROOFSTEP]
rw [sq, Nat.mul_right_eq_self_iff (Nat.mul_pos hp.pos hp.pos : 0 < a * a)] at h 
[GOAL]
case intro.inr
x y✝ : ℕ
hx✝ : x ≠ 1
hy✝ : y✝ ≠ 1
y : ℕ
hy : y ≠ 1
a : ℕ
hp : Prime a
h✝ : x * y✝ = a ^ 2
pdvdxy : a ∣ x * y✝
this : a ∣ a
hx : a * a ≠ 1
h : y = 1
⊢ y = 1
[PROOFSTEP]
exact h
[GOAL]
n p : ℕ
hp : Prime p
⊢ p ∣ (n + 1)! ↔ p ≤ n + 1
[PROOFSTEP]
rw [factorial_succ, hp.dvd_mul, Prime.dvd_factorial hp]
[GOAL]
n p : ℕ
hp : Prime p
⊢ p ∣ n + 1 ∨ p ≤ n ↔ p ≤ n + 1
[PROOFSTEP]
exact
  ⟨fun h => h.elim (le_of_dvd (succ_pos _)) le_succ_of_le, fun h =>
    (_root_.lt_or_eq_of_le h).elim (Or.inr ∘ le_of_lt_succ) fun h => Or.inl <| by rw [h]⟩
[GOAL]
n p : ℕ
hp : Prime p
h✝ : p ≤ n + 1
h : p = n + 1
⊢ p ∣ n + 1
[PROOFSTEP]
rw [h]
[GOAL]
p : ℕ
pp : Prime p
i : ℕ
⊢ coprime p i ∨ p ∣ i
[PROOFSTEP]
rw [pp.dvd_iff_not_coprime]
[GOAL]
p : ℕ
pp : Prime p
i : ℕ
⊢ coprime p i ∨ ¬coprime p i
[PROOFSTEP]
apply em
[GOAL]
p : ℕ
pp : Prime p
m i : ℕ
⊢ i ∣ p ^ m ↔ ∃ k, k ≤ m ∧ i = p ^ k
[PROOFSTEP]
simp_rw [_root_.dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]
[GOAL]
a p k : ℕ
pp : Prime p
h₁ : ¬a ∣ p ^ k
h₂ : a ∣ p ^ (k + 1)
⊢ a = p ^ (k + 1)
[PROOFSTEP]
obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂
[GOAL]
case intro.intro
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ p ^ l = p ^ (k + 1)
[PROOFSTEP]
congr
[GOAL]
case intro.intro.e_a
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1
[PROOFSTEP]
exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))
[GOAL]
⊢ 0 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 0
[PROOFSTEP]
simpa using Exists.intro 2 Nat.prime_two
[GOAL]
⊢ 1 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 1
[PROOFSTEP]
simp [Nat.not_prime_one]
[GOAL]
n : ℕ
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
[PROOFSTEP]
let a := n + 2
[GOAL]
n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
[PROOFSTEP]
let ha : a ≠ 1 := Nat.succ_succ_ne_one n
[GOAL]
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1 := succ_succ_ne_one n
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
[PROOFSTEP]
simp only [true_iff_iff, Ne.def, not_false_iff, ha]
[GOAL]
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1 := succ_succ_ne_one n
⊢ ∃ p, Prime p ∧ p ∣ n + 2
[PROOFSTEP]
exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩
[GOAL]
n : ℕ
⊢ n = 1 ↔ ∀ (p : ℕ), Prime p → ¬p ∣ n
[PROOFSTEP]
simpa using not_iff_not.mpr ne_one_iff_exists_prime_dvd
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd : p ^ (k + l) * p ∣ m * n :=
  by
  let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
  rwa [pow_succ'] at hpmn' 
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
⊢ p ^ (k + l) * p ∣ m * n
[PROOFSTEP]
let hpmn' : p ^ (succ (k + l)) ∣ m * n := hpmn
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpmn' : p ^ succ (k + l) ∣ m * n := hpmn
⊢ p ^ (k + l) * p ∣ m * n
[PROOFSTEP]
rwa [pow_succ'] at hpmn' 
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd2 : p ∣ m * n / p ^ (k + l) := dvd_div_of_mul_dvd hpd
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd3 : p ∣ m * n / (p ^ k * p ^ l) := by simpa [pow_add] using hpd2
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
⊢ p ∣ m * n / (p ^ k * p ^ l)
[PROOFSTEP]
simpa [pow_add] using hpd2
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd4 : p ∣ m / p ^ k * (n / p ^ l) := by simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
⊢ p ∣ m / p ^ k * (n / p ^ l)
[PROOFSTEP]
simpa [Nat.div_mul_div_comm hpm hpn] using hpd3
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
have hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l := (Prime.dvd_mul p_prime).1 hpd4
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
suffices p ^ k * p ∣ m ∨ p ^ l * p ∣ n by rwa [_root_.pow_succ', _root_.pow_succ']
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
this : p ^ k * p ∣ m ∨ p ^ l * p ∣ n
⊢ p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
[PROOFSTEP]
rwa [_root_.pow_succ', _root_.pow_succ']
[GOAL]
p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
⊢ p ^ k * p ∣ m ∨ p ^ l * p ∣ n
[PROOFSTEP]
exact
  hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h) fun h : p ∣ n / p ^ l =>
    Or.inr <| mul_dvd_of_dvd_div hpn h
[GOAL]
p : ℕ
hp : Prime p
a b : ℤ
h : ↑p ∣ a * b
⊢ ↑p ∣ a ∨ ↑p ∣ b
[PROOFSTEP]
rw [← Int.dvd_natAbs, Int.coe_nat_dvd, Int.natAbs_mul, hp.dvd_mul] at h 
[GOAL]
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ Int.natAbs a ∨ p ∣ Int.natAbs b
⊢ ↑p ∣ a ∨ ↑p ∣ b
[PROOFSTEP]
rwa [← Int.dvd_natAbs, Int.coe_nat_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd]
[GOAL]
p : ℕ
hp : _root_.Prime ↑p
h : p = 1
⊢ False
[PROOFSTEP]
simp [h, not_prime_one] at hp 
[GOAL]
p : ℕ
hp : _root_.Prime ↑p
a b : ℕ
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b
[PROOFSTEP]
simpa only [Int.coe_nat_dvd, (Int.ofNat_mul _ _).symm] using hp.2.2 a b
