BT003F

prime_or_composite

Stable · empty-context checked

Every nonzero nonunit natural is constructively prime or has a nontrivial factor pair.

Exact expanded PA statement

forall n. ~(n = 0) -> ~(n = 1) -> ((~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1) \/ exists c d. ((~(c = 1) /\ ~(d = 1)) /\ n = c * d))

Structural proof guide

Every nonzero nonunit natural is constructively prime or has a nontrivial factor pair.

Direct prerequisites: divisor_le_nonzero, factor_search_up_to. The authored body proceeds by case analysis (6), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT002D divisor_le_nonzero BT003E factor_search_up_to

Direct dependents

BT003H prime_decidable BT003K prime_divisor_exists_up_to BT0118 nonprime_has_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. 0002intro hn0
  3. 0003intro hn1
  4. 0004specialize factor_search_up_to n
  5. 0005specialize factor_search_up_to n
  6. 0006have hsearch : (forall c d. (exists k. k + c = n) -> n = c * d -> c = 1 \/ d = 1) \/ exists c d. ((((exists k. k + c = n) /\ ~(c = 1)) /\ ~(d = 1)) /\ n = c * d)
  7. 0007apply factor_search_up_to
  8. 0008exact hn0
  9. 0009cases hsearch
  10. 0010left
  11. 0011split
  12. 0012exact hn1
  13. 0013intro c
  14. 0014intro d
  15. 0015intro hfac
  16. 0016specialize hsearch_left c
  17. 0017specialize hsearch_left d
  18. 0018apply hsearch_left
  19. 0019specialize divisor_le_nonzero c
  20. 0020specialize divisor_le_nonzero n
  21. 0021apply divisor_le_nonzero
  22. 0022exact hn0
  23. 0023exists d
  24. 0024exact hfac
  25. 0025exact hfac
  26. 0026right
  27. 0027cases hsearch_right
  28. 0028cases hsearch_right_witness
  29. 0029cases hsearch_right_witness_witness
  30. 0030cases hsearch_right_witness_witness_left
  31. 0031cases hsearch_right_witness_witness_left_left
  32. 0032exists x
  33. 0033exists x1
  34. 0034split
  35. 0035split
  36. 0036exact hsearch_right_witness_witness_left_left_right
  37. 0037exact hsearch_right_witness_witness_left_right
  38. 0038exact hsearch_right_witness_witness_right