素数全体の集合が上に有界でないこと（その２）

前回程度なら参照する定理を与えるだけで．．．

# MESON [FACT_LE; ARITH_RULE `1 <= f ==> ~(f + 1 = 1)`; PRIME_FACTOR; DIVIDES_FA
CT_PRIME; COPRIME_PLUS1; coprime; prime; NOT_LE] `!n. ?p. prime p /\ n < p` ;;
0..0..0..6..16..39..92..171..316..618..1073..1919..3361..5464..9446..solved at 1
4672
val it : thm = |- !n. ?p. prime p /\ n < p

# MESON [FACT_LE; ARITH_RULE `1 <= f ==> ~(f + 1 = 1)`; PRIME_FACTOR; DIVIDES_FA
CT_PRIME; COPRIME_PLUS1; coprime; prime] `~(?n. !p. prime p ==> p <= n)` ;;
0..0..0..3..9..27..64..117..221..428..742..1402..2437..4001..solved at 5874
val it : thm = |- ~(?n. !p. prime p ==> p <= n)

と証明してくれます．ただし，ARITH_RULE で明示した部分を既存の定理で構成すると

# MESON [FACT_LE; LE_1; ONE; ADD1; SUC_INJ; PRIME_FACTOR; DIVIDES_FACT_PRIME; COPRIME_PLUS1; coprime; prime] `~(?n. !p. prime p ==> p <= n)` ;;
0..0..0..3..9..24..60..112..240..503..944..2307..5015..10282..32668..80687..186333..745893..2020724..4951370..

と MESON には荷が勝ち過ぎようですから，PV9 を用いれば当然

# PV9 [FACT_LE; LE_1; ONE; ADD1; SUC_INJ; PRIME_FACTOR; DIVIDES_FACT_PRI
ME; COPRIME_PLUS1; coprime; prime] `~(?n. !p. prime p ==> p <= n)` ;;
-------- Proof 1 --------

THEOREM PROVED

------ process 10100 exit (max_proofs) ------
val it : thm = |- ~(?n. !p. prime p ==> p <= n)

のように即答です．

なお，参照定理を列挙すると

# [FACT_LE; LE_1; ONE; ADD1; SUC_INJ; PRIME_FACTOR; DIVIDES_FACT_PRIME; COPRIME_PLUS1; coprime; prime];;
val it : thm list =
  [|- !n. 1 <= FACT n;
   |- (!n. ~(n = 0) ==> 0 < n) /\
      (!n. ~(n = 0) ==> 1 <= n) /\
      (!n. 0 < n ==> ~(n = 0)) /\
      (!n. 0 < n ==> 1 <= n) /\
      (!n. 1 <= n ==> 0 < n) /\
      (!n. 1 <= n ==> ~(n = 0));
   |- 1 = SUC 0; |- !m. SUC m = m + 1; |- !m n. SUC m = SUC n <=> m = n;
   |- !n. ~(n = 1) ==> (?p. prime p /\ p divides n);
   |- !p. prime p ==> (!n. p divides FACT n <=> p <= n);
   |- !n. coprime (n + 1,n);
   |- coprime (a,b) <=> (!d. d divides a /\ d divides b ==> d = 1);
   |- !p. prime p <=> ~(p = 1) /\ (!x. x divides p ==> x = 1 \/ x = p)]

なので，これらに prover 自身が FACT n + 1 を適用しているわけで．．．