BT00PR

prime_strictly_above_decidable

Alpha body-checked · checked-use disabled

Being prime and strictly above a fixed lower endpoint is decidable.

Exact expanded PA statement

forall l p. ((((~(p = 1) /\ forall frm_prime_left_bpi_above_decidable_prime frm_prime_right_bpi_above_decidable_prime. p = frm_prime_left_bpi_above_decidable_prime * frm_prime_right_bpi_above_decidable_prime -> frm_prime_left_bpi_above_decidable_prime = 1 \/ frm_prime_right_bpi_above_decidable_prime = 1)) /\ (exists frm_gap_bpi_above_decidable_lower. frm_gap_bpi_above_decidable_lower + S l = p))) \/ ~((((~(p = 1) /\ forall frm_prime_left_bpi_above_decidable_prime frm_prime_right_bpi_above_decidable_prime. p = frm_prime_left_bpi_above_decidable_prime * frm_prime_right_bpi_above_decidable_prime -> frm_prime_left_bpi_above_decidable_prime = 1 \/ frm_prime_right_bpi_above_decidable_prime = 1)) /\ (exists frm_gap_bpi_above_decidable_lower. frm_gap_bpi_above_decidable_lower + S l = p)))

Structural proof guide

Being prime and strictly above a fixed lower endpoint is decidable.

Direct prerequisites: prime_decidable, lt_trichotomy, lt_to_le, lt_not_le, le_refl. The authored body proceeds by case analysis (6), equality transport (1).

Proof neighborhood

Direct dependencies

BT003H prime_decidable BT001H lt_trichotomy BT0019 lt_to_le BT001I lt_not_le BT000E le_refl

Direct dependents

BT00PS bounded_prime_interval_search

Formal native tactic body

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

  1. 0001intro l
  2. 0002intro p
  3. 0003specialize prime_decidable p
  4. 0004cases prime_decidable
  5. 0005specialize lt_trichotomy l
  6. 0006specialize lt_trichotomy p
  7. 0007cases lt_trichotomy
  8. 0008right
  9. 0009intro habove
  10. 0010cases habove
  11. 0011specialize lt_not_le p
  12. 0012specialize lt_not_le p
  13. 0013apply lt_not_le
  14. 0014rewrite lt_trichotomy_left at habove_right
  15. 0015exact habove_right
  16. 0016specialize le_refl p
  17. 0017exact le_refl
  18. 0018cases lt_trichotomy_right
  19. 0019left
  20. 0020split
  21. 0021exact prime_decidable_left
  22. 0022exact lt_trichotomy_right_left
  23. 0023right
  24. 0024intro habove
  25. 0025cases habove
  26. 0026specialize lt_not_le p
  27. 0027specialize lt_not_le l
  28. 0028apply lt_not_le
  29. 0029exact lt_trichotomy_right_right
  30. 0030specialize lt_to_le l
  31. 0031specialize lt_to_le p
  32. 0032apply lt_to_le
  33. 0033exact habove_right
  34. 0034right
  35. 0035intro habove
  36. 0036cases habove
  37. 0037apply prime_decidable_right
  38. 0038exact habove_left