Theorem: gapAfterProdPrimeRange (FromTheBook/Ch02/UnboundedGaps.lean)

State before:
k u : ℕ
⊢ 2 ≤ u ∧ u ≤ Nat.succ k → ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
Tactic:
intros
State after:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + u)

State before:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
Tactic:
rw [Nat.prime_def_lt']
State after:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬(2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧
      ∀ (m : ℕ),
        2 ≤ m → m < PrimeRange.prod (Nat.succ (Nat.succ k)) + u → ¬m ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u)

State before:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ ¬(2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧
      ∀ (m : ℕ),
        2 ≤ m → m < PrimeRange.prod (Nat.succ (Nat.succ k)) + u → ¬m ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u)
Tactic:
simp
State after:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u →
    ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
k u : ℕ
a✝ : 2 ≤ u ∧ u ≤ Nat.succ k
⊢ 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u →
    ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
intros
State after:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
have : u ≠ 1
State after:
case this
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ u ≠ 1

k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case this
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ u ≠ 1

k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. linarith
State after:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
cases Nat.exists_prime_and_dvd this with
| intro p hp =>
  exists p
  have hu_pos : 0 < u
  . linarith
  have hpu : p ≤ u := Nat.le_of_dvd hu_pos hp.right
  apply And.intro
  . apply lt_of_le_of_lt hpu
    apply Nat.lt_add_of_pos_left
    apply PrimeRange.prodPos
  . apply And.intro
    . exact Nat.Prime.two_le hp.left
    . apply Nat.dvd_add _ hp.right
      apply PrimeRange.prodDvdOfLt hp.left
      linarith
State after:
no goals

State before:
case this
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
⊢ u ≠ 1
Tactic:
linarith
State after:
no goals

State before:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ ∃ x, x < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ x ∧ x ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
exists p
State after:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
have hu_pos : 0 < u
State after:
case hu_pos
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ 0 < u

case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case hu_pos
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ 0 < u

case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. linarith
State after:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
have hpu : p ≤ u := Nat.le_of_dvd hu_pos hp.right
State after:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case intro
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u ∧ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply And.intro
State after:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u

case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u

case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. apply lt_of_le_of_lt hpu
  apply Nat.lt_add_of_pos_left
  apply PrimeRange.prodPos
State after:
case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. apply And.intro
  . exact Nat.Prime.two_le hp.left
  . apply Nat.dvd_add _ hp.right
    apply PrimeRange.prodDvdOfLt hp.left
    linarith
State after:
no goals

State before:
case hu_pos
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ 0 < u
Tactic:
linarith
State after:
no goals

State before:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply lt_of_le_of_lt hpu
State after:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ u < PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ u < PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply Nat.lt_add_of_pos_left
State after:
case intro.left.h
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 0 < PrimeRange.prod (Nat.succ (Nat.succ k))

State before:
case intro.left.h
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 0 < PrimeRange.prod (Nat.succ (Nat.succ k))
Tactic:
apply PrimeRange.prodPos
State after:
no goals

State before:
case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply And.intro
State after:
case intro.right.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p

case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case intro.right.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p

case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. exact Nat.Prime.two_le hp.left
State after:
case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u

State before:
case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. apply Nat.dvd_add _ hp.right
  apply PrimeRange.prodDvdOfLt hp.left
  linarith
State after:
no goals

State before:
case intro.right.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p
Tactic:
exact Nat.Prime.two_le hp.left
State after:
no goals

State before:
case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply Nat.dvd_add _ hp.right
State after:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k))

State before:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k))
Tactic:
apply PrimeRange.prodDvdOfLt hp.left
State after:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < Nat.succ (Nat.succ k)

State before:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < Nat.succ (Nat.succ k)
Tactic:
linarith
State after:
no goals