BT003D

factor_property_succ

Stable · empty-context checked

Extend a bounded prime factor-pair property by checking the new boundary.

Exact expanded PA statement

forall B n. (forall c d. (exists k. k + c = B) -> n = c * d -> c = 1 \/ d = 1) -> (forall d. n = S B * d -> S B = 1 \/ d = 1) -> forall c d. (exists k. k + c = S B) -> n = c * d -> c = 1 \/ d = 1

Structural proof guide

Extend a bounded prime factor-pair property by checking the new boundary.

Direct prerequisites: le_eq_or_lt, le_of_succ_le_succ. The authored body proceeds by case analysis (1), intermediate claims (2), equality transport (2).

Proof neighborhood

Direct dependencies

BT001C le_eq_or_lt BT0017 le_of_succ_le_succ

Direct dependents

BT003E factor_search_up_to

Formal native tactic body

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

  1. 0001intro B
  2. 0002intro n
  3. 0003intro hprev
  4. 0004intro hboundary
  5. 0005intro c
  6. 0006intro d
  7. 0007intro hc
  8. 0008intro hfac
  9. 0009specialize le_eq_or_lt c
  10. 0010specialize le_eq_or_lt (S B)
  11. 0011have hsplit : c = S B \/ exists k. k + S c = S B
  12. 0012apply le_eq_or_lt
  13. 0013exact hc
  14. 0014cases hsplit
  15. 0015rewrite hsplit_left
  16. 0016specialize hboundary d
  17. 0017apply hboundary
  18. 0018rewrite <- hsplit_left
  19. 0019exact hfac
  20. 0020have hcB : exists k. k + c = B
  21. 0021apply le_of_succ_le_succ
  22. 0022exact hsplit_right
  23. 0023specialize hprev c
  24. 0024specialize hprev d
  25. 0025apply hprev
  26. 0026exact hcB
  27. 0027exact hfac