BT003H

prime_decidable

Stable · empty-context checked

Primality of every natural number is constructively decidable.

Exact expanded PA statement

forall n. ((~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1) \/ ~((~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1)))

Structural proof guide

Primality of every natural number is constructively decidable.

Direct prerequisites: eq_decidable, prime_or_composite, prime_nonzero. The authored body proceeds by case analysis (10), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT003A eq_decidable BT003F prime_or_composite BT003G prime_nonzero

Direct dependents

BT00PR prime_strictly_above_decidable BT00U5 primorial_factor_choice_exists BT00YN prime_contribution_choice_exists BT0119 prime_of_no_small_prime_divisor_below_square

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002specialize eq_decidable n
  3. 0003specialize eq_decidable 0
  4. 0004have hn0 : n = 0 \/ ~(n = 0)
  5. 0005apply eq_decidable
  6. 0006cases hn0
  7. 0007right
  8. 0008intro hp
  9. 0009specialize prime_nonzero n
  10. 0010apply prime_nonzero
  11. 0011exact hp
  12. 0012exact hn0_left
  13. 0013specialize eq_decidable_before n
  14. 0014specialize eq_decidable_before 1
  15. 0015have hn1 : n = 1 \/ ~(n = 1)
  16. 0016apply eq_decidable_before
  17. 0017cases hn1
  18. 0018right
  19. 0019intro hp
  20. 0020cases hp
  21. 0021apply hp_left
  22. 0022exact hn1_left
  23. 0023specialize prime_or_composite n
  24. 0024have hkind : ((~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1) \/ exists c d. ((~(c = 1) /\ ~(d = 1)) /\ n = c * d))
  25. 0025apply prime_or_composite
  26. 0026exact hn0_right
  27. 0027exact hn1_right
  28. 0028cases hkind
  29. 0029left
  30. 0030exact hkind_left
  31. 0031right
  32. 0032intro hp
  33. 0033cases hp
  34. 0034cases hkind_right
  35. 0035cases hkind_right_witness
  36. 0036cases hkind_right_witness_witness
  37. 0037cases hkind_right_witness_witness_left
  38. 0038specialize hp_right x
  39. 0039specialize hp_right x1
  40. 0040have hunit : x = 1 \/ x1 = 1
  41. 0041apply hp_right
  42. 0042exact hkind_right_witness_witness_right
  43. 0043cases hunit
  44. 0044apply hkind_right_witness_witness_left_left
  45. 0045exact hunit_left
  46. 0046apply hkind_right_witness_witness_left_right
  47. 0047exact hunit_right