BT00VA

factorial_prime_divides_of_le

Alpha body-checked · checked-use disabled

Every prime at most n divides the relational factorial n!.

Exact expanded PA statement

forall p n F. ((~(p = 1) /\ forall bpr_left_bfpdol_prime bpr_right_bfpdol_prime. p = bpr_left_bfpdol_prime * bpr_right_bfpdol_prime -> bpr_left_bfpdol_prime = 1 \/ bpr_right_bfpdol_prime = 1)) -> (exists bpr_le_gap_bfpdol_bound. bpr_le_gap_bfpdol_bound + (p) = (n)) -> (exists ff_b_bfpdol_source ff_c_bfpdol_source. ((forall ff_i_bfpdol_source_range. (exists ff_lt_bfpdol_source_range_bound. ff_lt_bfpdol_source_range_bound + S ff_i_bfpdol_source_range = n) -> (((exists ff_h_bfpdol_source_range_decoded. ff_h_bfpdol_source_range_decoded + S (1 + ff_i_bfpdol_source_range) = S ((S (ff_i_bfpdol_source_range)) * ff_c_bfpdol_source)) /\ exists ff_q_bfpdol_source_range_decoded. ff_b_bfpdol_source = ff_q_bfpdol_source_range_decoded * S ((S (ff_i_bfpdol_source_range)) * ff_c_bfpdol_source) + (1 + ff_i_bfpdol_source_range)))) /\ (exists ff_u_bfpdol_source_product ff_v_bfpdol_source_product. ((((exists ff_h_bfpdol_source_product_start. ff_h_bfpdol_source_product_start + S (1) = S ((S (0)) * ff_v_bfpdol_source_product)) /\ exists ff_q_bfpdol_source_product_start. ff_u_bfpdol_source_product = ff_q_bfpdol_source_product_start * S ((S (0)) * ff_v_bfpdol_source_product) + (1))) /\ ((((exists ff_h_bfpdol_source_product_terminal. ff_h_bfpdol_source_product_terminal + S (F) = S ((S (n)) * ff_v_bfpdol_source_product)) /\ exists ff_q_bfpdol_source_product_terminal. ff_u_bfpdol_source_product = ff_q_bfpdol_source_product_terminal * S ((S (n)) * ff_v_bfpdol_source_product) + (F))) /\ forall ff_i_bfpdol_source_product. (exists ff_lt_bfpdol_source_product_bound. ff_lt_bfpdol_source_product_bound + S ff_i_bfpdol_source_product = n) -> exists ff_p_bfpdol_source_product ff_r_bfpdol_source_product ff_s_bfpdol_source_product. ((((exists ff_h_bfpdol_source_product_factor. ff_h_bfpdol_source_product_factor + S (ff_p_bfpdol_source_product) = S ((S (ff_i_bfpdol_source_product)) * ff_c_bfpdol_source)) /\ exists ff_q_bfpdol_source_product_factor. ff_b_bfpdol_source = ff_q_bfpdol_source_product_factor * S ((S (ff_i_bfpdol_source_product)) * ff_c_bfpdol_source) + (ff_p_bfpdol_source_product))) /\ ((((exists ff_h_bfpdol_source_product_partial. ff_h_bfpdol_source_product_partial + S (ff_r_bfpdol_source_product) = S ((S (ff_i_bfpdol_source_product)) * ff_v_bfpdol_source_product)) /\ exists ff_q_bfpdol_source_product_partial. ff_u_bfpdol_source_product = ff_q_bfpdol_source_product_partial * S ((S (ff_i_bfpdol_source_product)) * ff_v_bfpdol_source_product) + (ff_r_bfpdol_source_product))) /\ ((((exists ff_h_bfpdol_source_product_successor. ff_h_bfpdol_source_product_successor + S (ff_s_bfpdol_source_product) = S ((S (S ff_i_bfpdol_source_product)) * ff_v_bfpdol_source_product)) /\ exists ff_q_bfpdol_source_product_successor. ff_u_bfpdol_source_product = ff_q_bfpdol_source_product_successor * S ((S (S ff_i_bfpdol_source_product)) * ff_v_bfpdol_source_product) + (ff_s_bfpdol_source_product))) /\ ff_s_bfpdol_source_product = ff_r_bfpdol_source_product * ff_p_bfpdol_source_product)))))))) -> (exists bpr_quotient_bfpdol_result. F = (p) * bpr_quotient_bfpdol_result)

Structural proof guide

Every prime at most n divides the relational factorial n!.

Direct prerequisites: prime_is_succ_succ, beta_factor_divides_product, add_succ_left, zero_add. The authored body proceeds by case analysis (5), intermediate claims (3), equality transport (2).

Proof neighborhood

Direct dependencies

BT00AW prime_is_succ_succ BT0069 beta_factor_divides_product BT0001 add_succ_left BT0000 zero_add

Direct dependents

BT00VC choose_prime_divides_between

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro n
  3. 0003intro F
  4. 0004intro hp
  5. 0005intro hle
  6. 0006intro hfactorial
  7. 0007have hshape : exists k. p = S (S k)
  8. 0008apply prime_is_succ_succ
  9. 0009exact hp
  10. 0010cases hshape
  11. 0011rewrite hshape_witness at hle
  12. 0012cases hfactorial
  13. 0013cases hfactorial_witness
  14. 0014cases hfactorial_witness_witness
  15. 0015have hentry : ((exists bpr_height_bfpdol_entry. bpr_height_bfpdol_entry + S (1 + S x) = S ((S (S x)) * x2)) /\ exists bpr_quotient_bfpdol_entry. x1 = bpr_quotient_bfpdol_entry * S ((S (S x)) * x2) + (1 + S x))
  16. 0016apply hfactorial_witness_witness_left
  17. 0017exact hle
  18. 0018have hraw : exists q. F = (1 + S x) * q
  19. 0019specialize beta_factor_divides_product x1
  20. 0020specialize beta_factor_divides_product x2
  21. 0021specialize beta_factor_divides_product n
  22. 0022specialize beta_factor_divides_product F
  23. 0023specialize beta_factor_divides_product (S x)
  24. 0024specialize beta_factor_divides_product (1 + S x)
  25. 0025apply beta_factor_divides_product
  26. 0026exact hle
  27. 0027exact hentry
  28. 0028exact hfactorial_witness_witness_right
  29. 0029cases hraw
  30. 0030exists x3
  31. 0031rewrite hshape_witness
  32. 0032trans (1 + S x) * x3
  33. 0033exact hraw_witness
  34. 0034congr
  35. 0035trans S (1 + x)
  36. 0036apply PA4
  37. 0037congr
  38. 0038trans S (0 + x)
  39. 0039specialize add_succ_left 0
  40. 0040specialize add_succ_left x
  41. 0041apply add_succ_left
  42. 0042congr
  43. 0043apply zero_add
  44. 0044refl