BT00VB

factorial_prime_le_of_divides

Alpha body-checked · checked-use disabled

Every prime divisor of n! is at most n.

Exact expanded PA statement

forall p n F. ((~(p = 1) /\ forall bpr_left_bfplod_prime bpr_right_bfplod_prime. p = bpr_left_bfplod_prime * bpr_right_bfplod_prime -> bpr_left_bfplod_prime = 1 \/ bpr_right_bfplod_prime = 1)) -> (exists ff_b_bfplod_source ff_c_bfplod_source. ((forall ff_i_bfplod_source_range. (exists ff_lt_bfplod_source_range_bound. ff_lt_bfplod_source_range_bound + S ff_i_bfplod_source_range = n) -> (((exists ff_h_bfplod_source_range_decoded. ff_h_bfplod_source_range_decoded + S (1 + ff_i_bfplod_source_range) = S ((S (ff_i_bfplod_source_range)) * ff_c_bfplod_source)) /\ exists ff_q_bfplod_source_range_decoded. ff_b_bfplod_source = ff_q_bfplod_source_range_decoded * S ((S (ff_i_bfplod_source_range)) * ff_c_bfplod_source) + (1 + ff_i_bfplod_source_range)))) /\ (exists ff_u_bfplod_source_product ff_v_bfplod_source_product. ((((exists ff_h_bfplod_source_product_start. ff_h_bfplod_source_product_start + S (1) = S ((S (0)) * ff_v_bfplod_source_product)) /\ exists ff_q_bfplod_source_product_start. ff_u_bfplod_source_product = ff_q_bfplod_source_product_start * S ((S (0)) * ff_v_bfplod_source_product) + (1))) /\ ((((exists ff_h_bfplod_source_product_terminal. ff_h_bfplod_source_product_terminal + S (F) = S ((S (n)) * ff_v_bfplod_source_product)) /\ exists ff_q_bfplod_source_product_terminal. ff_u_bfplod_source_product = ff_q_bfplod_source_product_terminal * S ((S (n)) * ff_v_bfplod_source_product) + (F))) /\ forall ff_i_bfplod_source_product. (exists ff_lt_bfplod_source_product_bound. ff_lt_bfplod_source_product_bound + S ff_i_bfplod_source_product = n) -> exists ff_p_bfplod_source_product ff_r_bfplod_source_product ff_s_bfplod_source_product. ((((exists ff_h_bfplod_source_product_factor. ff_h_bfplod_source_product_factor + S (ff_p_bfplod_source_product) = S ((S (ff_i_bfplod_source_product)) * ff_c_bfplod_source)) /\ exists ff_q_bfplod_source_product_factor. ff_b_bfplod_source = ff_q_bfplod_source_product_factor * S ((S (ff_i_bfplod_source_product)) * ff_c_bfplod_source) + (ff_p_bfplod_source_product))) /\ ((((exists ff_h_bfplod_source_product_partial. ff_h_bfplod_source_product_partial + S (ff_r_bfplod_source_product) = S ((S (ff_i_bfplod_source_product)) * ff_v_bfplod_source_product)) /\ exists ff_q_bfplod_source_product_partial. ff_u_bfplod_source_product = ff_q_bfplod_source_product_partial * S ((S (ff_i_bfplod_source_product)) * ff_v_bfplod_source_product) + (ff_r_bfplod_source_product))) /\ ((((exists ff_h_bfplod_source_product_successor. ff_h_bfplod_source_product_successor + S (ff_s_bfplod_source_product) = S ((S (S ff_i_bfplod_source_product)) * ff_v_bfplod_source_product)) /\ exists ff_q_bfplod_source_product_successor. ff_u_bfplod_source_product = ff_q_bfplod_source_product_successor * S ((S (S ff_i_bfplod_source_product)) * ff_v_bfplod_source_product) + (ff_s_bfplod_source_product))) /\ ff_s_bfplod_source_product = ff_r_bfplod_source_product * ff_p_bfplod_source_product)))))))) -> (exists bpr_quotient_bfplod_divides. F = (p) * bpr_quotient_bfplod_divides) -> (exists bpr_le_gap_bfplod_result. bpr_le_gap_bfplod_result + (p) = (n))

Structural proof guide

Every prime divisor of n! is at most n.

Direct prerequisites: divisor_one, le_succ, euclid_prime_dvd_product, divisor_le_nonzero, succ_ne_zero, factorial_zero, factorial_succ_decompose. The authored body proceeds by structural induction (1), case analysis (5), intermediate claims (5), equality transport (2).

Proof neighborhood

Direct dependencies

BT002E divisor_one BT0018 le_succ BT003N euclid_prime_dvd_product BT002D divisor_le_nonzero BT000C succ_ne_zero BT0091 factorial_zero BT0092 factorial_succ_decompose

Direct dependents

BT00VC choose_prime_divides_between BT00VX central_binom_prime_divisor_le_double

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. 0002induction n
  3. 0003intro F
  4. 0004intro hp
  5. 0005cases hp
  6. 0006intro hfactorial
  7. 0007intro hdivides
  8. 0008have hF_one : F = 1
  9. 0009specialize factorial_zero 0
  10. 0010specialize factorial_zero F
  11. 0011apply factorial_zero
  12. 0012refl
  13. 0013exact hfactorial
  14. 0014rewrite hF_one at hdivides
  15. 0015have hp_one : p = 1
  16. 0016specialize divisor_one p
  17. 0017apply divisor_one
  18. 0018exact hdivides
  19. 0019exfalso
  20. 0020apply hp_left
  21. 0021exact hp_one
  22. 0022intro F
  23. 0023intro hp
  24. 0024cases hp
  25. 0025intro hfactorial
  26. 0026intro hdivides
  27. 0027have hdecomposition : exists r. (exists ff_b_bfplod_previous ff_c_bfplod_previous. ((forall ff_i_bfplod_previous_range. (exists ff_lt_bfplod_previous_range_bound. ff_lt_bfplod_previous_range_bound + S ff_i_bfplod_previous_range = n) -> (((exists ff_h_bfplod_previous_range_decoded. ff_h_bfplod_previous_range_decoded + S (1 + ff_i_bfplod_previous_range) = S ((S (ff_i_bfplod_previous_range)) * ff_c_bfplod_previous)) /\ exists ff_q_bfplod_previous_range_decoded. ff_b_bfplod_previous = ff_q_bfplod_previous_range_decoded * S ((S (ff_i_bfplod_previous_range)) * ff_c_bfplod_previous) + (1 + ff_i_bfplod_previous_range)))) /\ (exists ff_u_bfplod_previous_product ff_v_bfplod_previous_product. ((((exists ff_h_bfplod_previous_product_start. ff_h_bfplod_previous_product_start + S (1) = S ((S (0)) * ff_v_bfplod_previous_product)) /\ exists ff_q_bfplod_previous_product_start. ff_u_bfplod_previous_product = ff_q_bfplod_previous_product_start * S ((S (0)) * ff_v_bfplod_previous_product) + (1))) /\ ((((exists ff_h_bfplod_previous_product_terminal. ff_h_bfplod_previous_product_terminal + S (r) = S ((S (n)) * ff_v_bfplod_previous_product)) /\ exists ff_q_bfplod_previous_product_terminal. ff_u_bfplod_previous_product = ff_q_bfplod_previous_product_terminal * S ((S (n)) * ff_v_bfplod_previous_product) + (r))) /\ forall ff_i_bfplod_previous_product. (exists ff_lt_bfplod_previous_product_bound. ff_lt_bfplod_previous_product_bound + S ff_i_bfplod_previous_product = n) -> exists ff_p_bfplod_previous_product ff_r_bfplod_previous_product ff_s_bfplod_previous_product. ((((exists ff_h_bfplod_previous_product_factor. ff_h_bfplod_previous_product_factor + S (ff_p_bfplod_previous_product) = S ((S (ff_i_bfplod_previous_product)) * ff_c_bfplod_previous)) /\ exists ff_q_bfplod_previous_product_factor. ff_b_bfplod_previous = ff_q_bfplod_previous_product_factor * S ((S (ff_i_bfplod_previous_product)) * ff_c_bfplod_previous) + (ff_p_bfplod_previous_product))) /\ ((((exists ff_h_bfplod_previous_product_partial. ff_h_bfplod_previous_product_partial + S (ff_r_bfplod_previous_product) = S ((S (ff_i_bfplod_previous_product)) * ff_v_bfplod_previous_product)) /\ exists ff_q_bfplod_previous_product_partial. ff_u_bfplod_previous_product = ff_q_bfplod_previous_product_partial * S ((S (ff_i_bfplod_previous_product)) * ff_v_bfplod_previous_product) + (ff_r_bfplod_previous_product))) /\ ((((exists ff_h_bfplod_previous_product_successor. ff_h_bfplod_previous_product_successor + S (ff_s_bfplod_previous_product) = S ((S (S ff_i_bfplod_previous_product)) * ff_v_bfplod_previous_product)) /\ exists ff_q_bfplod_previous_product_successor. ff_u_bfplod_previous_product = ff_q_bfplod_previous_product_successor * S ((S (S ff_i_bfplod_previous_product)) * ff_v_bfplod_previous_product) + (ff_s_bfplod_previous_product))) /\ ff_s_bfplod_previous_product = ff_r_bfplod_previous_product * ff_p_bfplod_previous_product)))))))) /\ F = r * S n
  28. 0028specialize factorial_succ_decompose n
  29. 0029specialize factorial_succ_decompose (S n)
  30. 0030specialize factorial_succ_decompose F
  31. 0031apply factorial_succ_decompose
  32. 0032refl
  33. 0033exact hfactorial
  34. 0034cases hdecomposition
  35. 0035cases hdecomposition_witness
  36. 0036rewrite hdecomposition_witness_right at hdivides
  37. 0037have hsplit : (exists bpr_quotient_bfplod_split_left. x = (p) * bpr_quotient_bfplod_split_left) \/ (exists bpr_quotient_bfplod_split_right. S n = (p) * bpr_quotient_bfplod_split_right)
  38. 0038specialize euclid_prime_dvd_product p
  39. 0039specialize euclid_prime_dvd_product x
  40. 0040specialize euclid_prime_dvd_product (S n)
  41. 0041apply euclid_prime_dvd_product
  42. 0042split
  43. 0043exact hp_left
  44. 0044exact hp_right
  45. 0045exact hdivides
  46. 0046cases hsplit
  47. 0047have hprevious : exists g. g + p = n
  48. 0048specialize IH x
  49. 0049apply IH
  50. 0050split
  51. 0051exact hp_left
  52. 0052exact hp_right
  53. 0053exact hdecomposition_witness_left
  54. 0054exact hsplit_left
  55. 0055specialize le_succ p
  56. 0056specialize le_succ n
  57. 0057apply le_succ
  58. 0058exact hprevious
  59. 0059specialize divisor_le_nonzero p
  60. 0060specialize divisor_le_nonzero (S n)
  61. 0061apply divisor_le_nonzero
  62. 0062specialize succ_ne_zero n
  63. 0063exact succ_ne_zero
  64. 0064exact hsplit_right