BT011Q

bertrand_covering_interval

Alpha body-checked · checked-use disabled

One checked adjacent cover supplies a Bertrand witness.

Exact expanded PA statement

forall a b n. ((~(b = 1) /\ forall bpr_left_bb8ci_prime bpr_right_bb8ci_prime. b = bpr_left_bb8ci_prime * bpr_right_bb8ci_prime -> bpr_left_bb8ci_prime = 1 \/ bpr_right_bb8ci_prime = 1)) -> (exists bpr_le_gap_bb8ci_lower. bpr_le_gap_bb8ci_lower + (a) = (n)) -> (exists bpr_gap_bb8ci_strict. bpr_gap_bb8ci_strict + S (n) = b) -> (exists bpr_le_gap_bb8ci_cover. bpr_le_gap_bb8ci_cover + (b) = (a + a)) -> exists p. ((~(p = 1) /\ forall bpr_left_bb8ci_result_prime bpr_right_bb8ci_result_prime. p = bpr_left_bb8ci_result_prime * bpr_right_bb8ci_result_prime -> bpr_left_bb8ci_result_prime = 1 \/ bpr_right_bb8ci_result_prime = 1)) /\ ((exists bpr_gap_bb8ci_result_strict. bpr_gap_bb8ci_result_strict + S (n) = p) /\ (exists bpr_le_gap_bb8ci_result_upper. bpr_le_gap_bb8ci_result_upper + (p) = (n + n)))

Structural proof guide

One checked adjacent cover supplies a Bertrand witness.

Direct prerequisites: add_le_add_right, add_le_add_left, le_trans. The authored body proceeds by intermediate claims (4).

Proof neighborhood

Direct dependencies

BT0014 add_le_add_right BT0015 add_le_add_left BT000F le_trans

Direct dependents

BT0124 bertrand_small_closed_upper

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro n
  4. 0004intro hprime
  5. 0005intro hlower
  6. 0006intro hstrict
  7. 0007intro hcover
  8. 0008have hfirst : exists k. k + (a + a) = n + a
  9. 0009specialize add_le_add_right a
  10. 0010specialize add_le_add_right n
  11. 0011specialize add_le_add_right a
  12. 0012apply add_le_add_right
  13. 0013exact hlower
  14. 0014have hsecond : exists k. k + (n + a) = n + n
  15. 0015specialize add_le_add_left a
  16. 0016specialize add_le_add_left n
  17. 0017specialize add_le_add_left n
  18. 0018apply add_le_add_left
  19. 0019exact hlower
  20. 0020have hdouble : exists k. k + (a + a) = n + n
  21. 0021specialize le_trans (a + a)
  22. 0022specialize le_trans (n + a)
  23. 0023specialize le_trans (n + n)
  24. 0024apply le_trans
  25. 0025exact hfirst
  26. 0026exact hsecond
  27. 0027have hupper : exists k. k + b = n + n
  28. 0028specialize le_trans b
  29. 0029specialize le_trans (a + a)
  30. 0030specialize le_trans (n + n)
  31. 0031apply le_trans
  32. 0032exact hcover
  33. 0033exact hdouble
  34. 0034exists b
  35. 0035split
  36. 0036exact hprime
  37. 0037split
  38. 0038exact hstrict
  39. 0039exact hupper