Proof step 1 from proof prime-prime (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ prime(n) ↔ n ≠ 0 ∧ n ≠ 1 ∧ (∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0)

Rule argument

Additional information

Used simplifier rules: ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s)

Proof step 2 from proof prime-prime (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  prime(n) ⊦ n ≠ 0 ∧ n ≠ 1 ∧ (∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0)

• Proof step 6:

  n ≠ 1, n ≠ 0, ¬ prime(n), ∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0 ⊦

Rule argument

Additional information

Proof step 3 from proof prime-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  n % n0 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, prime(n), prime(n0), 2 ≤ n0, n0 * n0 ≤ n ⊦

Rule argument

Additional information

Used simplifier rules: zero: ⊦ ¬ prime(0); one: ⊦ ¬ prime(1); not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat

Proof step 4 from proof prime-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ n ≠ 0 → (m % n = 0 ↔ (∃ n0. m = n0 * n))

Rule argument

Additional information

Used simplifier rules: mult-02: ⊦ prime(m) → (prime(m * n) ↔ n = 1); ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws) ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n); (s) ⊦ m0 * m = 1 ↔ m0 = 1 ∧ m = 1; (ws) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat Used terms: n0, n

Proof step 5 from proof prime-prime (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof prime-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  n ≠ 1, n ≠ 0, ¬ prime(n), ∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0 ⊦

Rule argument

Additional information

Proof step 7 from proof prime-prime (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 8:

  ¬ prime(n), 2 ≤ n ⊦ ∃ m. m | n ∧ prime(m) ∧ m * m ≤ n

• Proof step 9:

  n ≠ 1, n ≠ 0, ¬ prime(n), ∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0, ∃ m. m | n ∧ prime(m) ∧ m * m ≤ n ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n ≠ 1 → (n < 2 ↔ n = 0); (s) Used terms: n

Proof step 8 from proof prime-prime (previous step) (back to tree)

Lemma not-prime

Proof step 9 from proof prime-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  n ≠ 1, n ≠ 0, prime(n0), n0 | n, n0 * n0 ≤ n, ¬ prime(n), ∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0 ⊦

Rule argument

Additional information

Proof step 10 from proof prime-prime (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  m ≠ 0 ⊦ m | n ↔ n % m = 0

• Proof step 12:

  n % n0 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, prime(n0), n0 * n0 ≤ n, ¬ prime(n), ∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0 ⊦

Rule argument

Additional information

Used simplifier rules: zero: ⊦ ¬ prime(0); ⊦ 0 ≤ m; (s) Used terms: n, n0

Proof step 11 from proof prime-prime (previous step) (back to tree)

Lemma divi-mod

Proof step 12 from proof prime-prime (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  n % n0 = 0, n ≠ 1, n ≠ 0, n0 ≠ 0, prime(n0), n0 * n0 ≤ n, ¬ prime(n), ∀ m. 2 ≤ m ∧ prime(m) ∧ m * m ≤ n → n % m ≠ 0 ⊦

Rule argument

Additional information

Proof step 13 from proof prime-prime (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: one: ⊦ ¬ prime(1); ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m ≠ 0 → (m < 2 ↔ m = 1); (s) ⊦ m % 1 = 0; (s) Used terms: n0