BT0092

factorial_succ_decompose

Stable · empty-context checked

A successor factorial is its predecessor factorial times the successor.

Exact expanded PA statement

forall n sn z. sn = S n -> (exists ff_b_successor ff_c_successor. ((forall ff_i_successor_range. (exists ff_lt_successor_range_bound. ff_lt_successor_range_bound + S ff_i_successor_range = sn) -> (((exists ff_h_successor_range_decoded. ff_h_successor_range_decoded + S (1 + ff_i_successor_range) = S ((S (ff_i_successor_range)) * ff_c_successor)) /\ exists ff_q_successor_range_decoded. ff_b_successor = ff_q_successor_range_decoded * S ((S (ff_i_successor_range)) * ff_c_successor) + (1 + ff_i_successor_range)))) /\ (exists ff_u_successor_product ff_v_successor_product. ((((exists ff_h_successor_product_start. ff_h_successor_product_start + S (1) = S ((S (0)) * ff_v_successor_product)) /\ exists ff_q_successor_product_start. ff_u_successor_product = ff_q_successor_product_start * S ((S (0)) * ff_v_successor_product) + (1))) /\ ((((exists ff_h_successor_product_terminal. ff_h_successor_product_terminal + S (z) = S ((S (sn)) * ff_v_successor_product)) /\ exists ff_q_successor_product_terminal. ff_u_successor_product = ff_q_successor_product_terminal * S ((S (sn)) * ff_v_successor_product) + (z))) /\ forall ff_i_successor_product. (exists ff_lt_successor_product_bound. ff_lt_successor_product_bound + S ff_i_successor_product = sn) -> exists ff_p_successor_product ff_r_successor_product ff_s_successor_product. ((((exists ff_h_successor_product_factor. ff_h_successor_product_factor + S (ff_p_successor_product) = S ((S (ff_i_successor_product)) * ff_c_successor)) /\ exists ff_q_successor_product_factor. ff_b_successor = ff_q_successor_product_factor * S ((S (ff_i_successor_product)) * ff_c_successor) + (ff_p_successor_product))) /\ ((((exists ff_h_successor_product_partial. ff_h_successor_product_partial + S (ff_r_successor_product) = S ((S (ff_i_successor_product)) * ff_v_successor_product)) /\ exists ff_q_successor_product_partial. ff_u_successor_product = ff_q_successor_product_partial * S ((S (ff_i_successor_product)) * ff_v_successor_product) + (ff_r_successor_product))) /\ ((((exists ff_h_successor_product_successor. ff_h_successor_product_successor + S (ff_s_successor_product) = S ((S (S ff_i_successor_product)) * ff_v_successor_product)) /\ exists ff_q_successor_product_successor. ff_u_successor_product = ff_q_successor_product_successor * S ((S (S ff_i_successor_product)) * ff_v_successor_product) + (ff_s_successor_product))) /\ ff_s_successor_product = ff_r_successor_product * ff_p_successor_product)))))))) -> exists r. (exists ff_b_predecessor ff_c_predecessor. ((forall ff_i_predecessor_range. (exists ff_lt_predecessor_range_bound. ff_lt_predecessor_range_bound + S ff_i_predecessor_range = n) -> (((exists ff_h_predecessor_range_decoded. ff_h_predecessor_range_decoded + S (1 + ff_i_predecessor_range) = S ((S (ff_i_predecessor_range)) * ff_c_predecessor)) /\ exists ff_q_predecessor_range_decoded. ff_b_predecessor = ff_q_predecessor_range_decoded * S ((S (ff_i_predecessor_range)) * ff_c_predecessor) + (1 + ff_i_predecessor_range)))) /\ (exists ff_u_predecessor_product ff_v_predecessor_product. ((((exists ff_h_predecessor_product_start. ff_h_predecessor_product_start + S (1) = S ((S (0)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_start. ff_u_predecessor_product = ff_q_predecessor_product_start * S ((S (0)) * ff_v_predecessor_product) + (1))) /\ ((((exists ff_h_predecessor_product_terminal. ff_h_predecessor_product_terminal + S (r) = S ((S (n)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_terminal. ff_u_predecessor_product = ff_q_predecessor_product_terminal * S ((S (n)) * ff_v_predecessor_product) + (r))) /\ forall ff_i_predecessor_product. (exists ff_lt_predecessor_product_bound. ff_lt_predecessor_product_bound + S ff_i_predecessor_product = n) -> exists ff_p_predecessor_product ff_r_predecessor_product ff_s_predecessor_product. ((((exists ff_h_predecessor_product_factor. ff_h_predecessor_product_factor + S (ff_p_predecessor_product) = S ((S (ff_i_predecessor_product)) * ff_c_predecessor)) /\ exists ff_q_predecessor_product_factor. ff_b_predecessor = ff_q_predecessor_product_factor * S ((S (ff_i_predecessor_product)) * ff_c_predecessor) + (ff_p_predecessor_product))) /\ ((((exists ff_h_predecessor_product_partial. ff_h_predecessor_product_partial + S (ff_r_predecessor_product) = S ((S (ff_i_predecessor_product)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_partial. ff_u_predecessor_product = ff_q_predecessor_product_partial * S ((S (ff_i_predecessor_product)) * ff_v_predecessor_product) + (ff_r_predecessor_product))) /\ ((((exists ff_h_predecessor_product_successor. ff_h_predecessor_product_successor + S (ff_s_predecessor_product) = S ((S (S ff_i_predecessor_product)) * ff_v_predecessor_product)) /\ exists ff_q_predecessor_product_successor. ff_u_predecessor_product = ff_q_predecessor_product_successor * S ((S (S ff_i_predecessor_product)) * ff_v_predecessor_product) + (ff_s_predecessor_product))) /\ ff_s_predecessor_product = ff_r_predecessor_product * ff_p_predecessor_product)))))))) /\ z = r * S n

Structural proof guide

A successor factorial is its predecessor factorial times the successor.

Direct prerequisites: beta_product_succ_decompose, beta_range_entry_eq, le_refl, le_succ, add_succ_left, zero_add. The authored body proceeds by case analysis (7), intermediate claims (2), equality transport (5).

Proof neighborhood

Direct dependencies

BT005J beta_product_succ_decompose BT0087 beta_range_entry_eq BT000E le_refl BT0018 le_succ BT0001 add_succ_left BT0000 zero_add

Direct dependents

BT00RK factorial_nonzero BT00RP prime_factorial_valuation_succ BT00TX choose_factorial_bridge BT00VB factorial_prime_le_of_divides

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro sn
  3. 0003intro z
  4. 0004intro hsn
  5. 0005intro hfactorial
  6. 0006rewrite hsn at hfactorial
  7. 0007rewrite hsn at hfactorial
  8. 0008rewrite hsn at hfactorial
  9. 0009rewrite hsn at hfactorial
  10. 0010cases hfactorial
  11. 0011cases hfactorial_witness
  12. 0012cases hfactorial_witness_witness
  13. 0013have hdecomp : exists p r. (((exists ff_h_factorial_succ_factor. ff_h_factorial_succ_factor + S (p) = S ((S (n)) * x1)) /\ exists ff_q_factorial_succ_factor. x = ff_q_factorial_succ_factor * S ((S (n)) * x1) + (p))) /\ ((exists ff_u_factorial_succ_prefix ff_v_factorial_succ_prefix. ((((exists ff_h_factorial_succ_prefix_start. ff_h_factorial_succ_prefix_start + S (1) = S ((S (0)) * ff_v_factorial_succ_prefix)) /\ exists ff_q_factorial_succ_prefix_start. ff_u_factorial_succ_prefix = ff_q_factorial_succ_prefix_start * S ((S (0)) * ff_v_factorial_succ_prefix) + (1))) /\ ((((exists ff_h_factorial_succ_prefix_terminal. ff_h_factorial_succ_prefix_terminal + S (r) = S ((S (n)) * ff_v_factorial_succ_prefix)) /\ exists ff_q_factorial_succ_prefix_terminal. ff_u_factorial_succ_prefix = ff_q_factorial_succ_prefix_terminal * S ((S (n)) * ff_v_factorial_succ_prefix) + (r))) /\ forall ff_i_factorial_succ_prefix. (exists ff_lt_factorial_succ_prefix_bound. ff_lt_factorial_succ_prefix_bound + S ff_i_factorial_succ_prefix = n) -> exists ff_p_factorial_succ_prefix ff_r_factorial_succ_prefix ff_s_factorial_succ_prefix. ((((exists ff_h_factorial_succ_prefix_factor. ff_h_factorial_succ_prefix_factor + S (ff_p_factorial_succ_prefix) = S ((S (ff_i_factorial_succ_prefix)) * x1)) /\ exists ff_q_factorial_succ_prefix_factor. x = ff_q_factorial_succ_prefix_factor * S ((S (ff_i_factorial_succ_prefix)) * x1) + (ff_p_factorial_succ_prefix))) /\ ((((exists ff_h_factorial_succ_prefix_partial. ff_h_factorial_succ_prefix_partial + S (ff_r_factorial_succ_prefix) = S ((S (ff_i_factorial_succ_prefix)) * ff_v_factorial_succ_prefix)) /\ exists ff_q_factorial_succ_prefix_partial. ff_u_factorial_succ_prefix = ff_q_factorial_succ_prefix_partial * S ((S (ff_i_factorial_succ_prefix)) * ff_v_factorial_succ_prefix) + (ff_r_factorial_succ_prefix))) /\ ((((exists ff_h_factorial_succ_prefix_successor. ff_h_factorial_succ_prefix_successor + S (ff_s_factorial_succ_prefix) = S ((S (S ff_i_factorial_succ_prefix)) * ff_v_factorial_succ_prefix)) /\ exists ff_q_factorial_succ_prefix_successor. ff_u_factorial_succ_prefix = ff_q_factorial_succ_prefix_successor * S ((S (S ff_i_factorial_succ_prefix)) * ff_v_factorial_succ_prefix) + (ff_s_factorial_succ_prefix))) /\ ff_s_factorial_succ_prefix = ff_r_factorial_succ_prefix * ff_p_factorial_succ_prefix)))))) /\ z = r * p)
  14. 0014specialize beta_product_succ_decompose x
  15. 0015specialize beta_product_succ_decompose x1
  16. 0016specialize beta_product_succ_decompose n
  17. 0017specialize beta_product_succ_decompose z
  18. 0018apply beta_product_succ_decompose
  19. 0019exact hfactorial_witness_witness_right
  20. 0020cases hdecomp
  21. 0021cases hdecomp_witness
  22. 0022cases hdecomp_witness_witness
  23. 0023cases hdecomp_witness_witness_right
  24. 0024have hp : x2 = 1 + n
  25. 0025specialize beta_range_entry_eq x
  26. 0026specialize beta_range_entry_eq x1
  27. 0027specialize beta_range_entry_eq 1
  28. 0028specialize beta_range_entry_eq (S n)
  29. 0029specialize beta_range_entry_eq n
  30. 0030specialize beta_range_entry_eq x2
  31. 0031apply beta_range_entry_eq
  32. 0032exact hfactorial_witness_witness_left
  33. 0033specialize le_refl (S n)
  34. 0034exact le_refl
  35. 0035exact hdecomp_witness_witness_left
  36. 0036exists x3
  37. 0037split
  38. 0038exists x
  39. 0039exists x1
  40. 0040split
  41. 0041intro i
  42. 0042intro hi
  43. 0043specialize hfactorial_witness_witness_left i
  44. 0044apply hfactorial_witness_witness_left
  45. 0045specialize le_succ (S i)
  46. 0046specialize le_succ n
  47. 0047apply le_succ
  48. 0048exact hi
  49. 0049exact hdecomp_witness_witness_right_left
  50. 0050trans x3 * x2
  51. 0051exact hdecomp_witness_witness_right_right
  52. 0052rewrite hp
  53. 0053congr
  54. 0054refl
  55. 0055specialize add_succ_left 0
  56. 0056specialize add_succ_left n
  57. 0057trans S (0 + n)
  58. 0058exact add_succ_left
  59. 0059congr
  60. 0060apply zero_add