PA00BH

beta_range_two_product_restore_last

Alpha v16 checked-use theorem · independently closed; not Stable

Restore the final factor l+2 after the leading unit has been absorbed.

Exact expanded PA statement

forall b c l P n F. n = S (S l) -> (forall wtp_range_index_wer_range_two. (exists wtp_range_gap_wer_range_two. wtp_range_gap_wer_range_two + S wtp_range_index_wer_range_two = l) -> (((exists ff_h_wer_range_two_decoded. ff_h_wer_range_two_decoded + S (2 + wtp_range_index_wer_range_two) = S ((S (wtp_range_index_wer_range_two)) * c)) /\ exists ff_q_wer_range_two_decoded. b = ff_q_wer_range_two_decoded * S ((S (wtp_range_index_wer_range_two)) * c) + (2 + wtp_range_index_wer_range_two)))) -> (exists ff_u_wer_range_two_product ff_v_wer_range_two_product. ((((exists ff_h_wer_range_two_product_start. ff_h_wer_range_two_product_start + S (1) = S ((S (0)) * ff_v_wer_range_two_product)) /\ exists ff_q_wer_range_two_product_start. ff_u_wer_range_two_product = ff_q_wer_range_two_product_start * S ((S (0)) * ff_v_wer_range_two_product) + (1))) /\ ((((exists ff_h_wer_range_two_product_terminal. ff_h_wer_range_two_product_terminal + S (P) = S ((S (l)) * ff_v_wer_range_two_product)) /\ exists ff_q_wer_range_two_product_terminal. ff_u_wer_range_two_product = ff_q_wer_range_two_product_terminal * S ((S (l)) * ff_v_wer_range_two_product) + (P))) /\ forall ff_i_wer_range_two_product. (exists ff_lt_wer_range_two_product_bound. ff_lt_wer_range_two_product_bound + S ff_i_wer_range_two_product = l) -> exists ff_p_wer_range_two_product ff_r_wer_range_two_product ff_s_wer_range_two_product. ((((exists ff_h_wer_range_two_product_factor. ff_h_wer_range_two_product_factor + S (ff_p_wer_range_two_product) = S ((S (ff_i_wer_range_two_product)) * c)) /\ exists ff_q_wer_range_two_product_factor. b = ff_q_wer_range_two_product_factor * S ((S (ff_i_wer_range_two_product)) * c) + (ff_p_wer_range_two_product))) /\ ((((exists ff_h_wer_range_two_product_partial. ff_h_wer_range_two_product_partial + S (ff_r_wer_range_two_product) = S ((S (ff_i_wer_range_two_product)) * ff_v_wer_range_two_product)) /\ exists ff_q_wer_range_two_product_partial. ff_u_wer_range_two_product = ff_q_wer_range_two_product_partial * S ((S (ff_i_wer_range_two_product)) * ff_v_wer_range_two_product) + (ff_r_wer_range_two_product))) /\ ((((exists ff_h_wer_range_two_product_successor. ff_h_wer_range_two_product_successor + S (ff_s_wer_range_two_product) = S ((S (S ff_i_wer_range_two_product)) * ff_v_wer_range_two_product)) /\ exists ff_q_wer_range_two_product_successor. ff_u_wer_range_two_product = ff_q_wer_range_two_product_successor * S ((S (S ff_i_wer_range_two_product)) * ff_v_wer_range_two_product) + (ff_s_wer_range_two_product))) /\ ff_s_wer_range_two_product = ff_r_wer_range_two_product * ff_p_wer_range_two_product)))))) -> (exists ff_b_wer_endpoint ff_c_wer_endpoint. ((forall ff_i_wer_endpoint_range. (exists ff_lt_wer_endpoint_range_bound. ff_lt_wer_endpoint_range_bound + S ff_i_wer_endpoint_range = n) -> (((exists ff_h_wer_endpoint_range_decoded. ff_h_wer_endpoint_range_decoded + S (1 + ff_i_wer_endpoint_range) = S ((S (ff_i_wer_endpoint_range)) * ff_c_wer_endpoint)) /\ exists ff_q_wer_endpoint_range_decoded. ff_b_wer_endpoint = ff_q_wer_endpoint_range_decoded * S ((S (ff_i_wer_endpoint_range)) * ff_c_wer_endpoint) + (1 + ff_i_wer_endpoint_range)))) /\ (exists ff_u_wer_endpoint_product ff_v_wer_endpoint_product. ((((exists ff_h_wer_endpoint_product_start. ff_h_wer_endpoint_product_start + S (1) = S ((S (0)) * ff_v_wer_endpoint_product)) /\ exists ff_q_wer_endpoint_product_start. ff_u_wer_endpoint_product = ff_q_wer_endpoint_product_start * S ((S (0)) * ff_v_wer_endpoint_product) + (1))) /\ ((((exists ff_h_wer_endpoint_product_terminal. ff_h_wer_endpoint_product_terminal + S (F) = S ((S (n)) * ff_v_wer_endpoint_product)) /\ exists ff_q_wer_endpoint_product_terminal. ff_u_wer_endpoint_product = ff_q_wer_endpoint_product_terminal * S ((S (n)) * ff_v_wer_endpoint_product) + (F))) /\ forall ff_i_wer_endpoint_product. (exists ff_lt_wer_endpoint_product_bound. ff_lt_wer_endpoint_product_bound + S ff_i_wer_endpoint_product = n) -> exists ff_p_wer_endpoint_product ff_r_wer_endpoint_product ff_s_wer_endpoint_product. ((((exists ff_h_wer_endpoint_product_factor. ff_h_wer_endpoint_product_factor + S (ff_p_wer_endpoint_product) = S ((S (ff_i_wer_endpoint_product)) * ff_c_wer_endpoint)) /\ exists ff_q_wer_endpoint_product_factor. ff_b_wer_endpoint = ff_q_wer_endpoint_product_factor * S ((S (ff_i_wer_endpoint_product)) * ff_c_wer_endpoint) + (ff_p_wer_endpoint_product))) /\ ((((exists ff_h_wer_endpoint_product_partial. ff_h_wer_endpoint_product_partial + S (ff_r_wer_endpoint_product) = S ((S (ff_i_wer_endpoint_product)) * ff_v_wer_endpoint_product)) /\ exists ff_q_wer_endpoint_product_partial. ff_u_wer_endpoint_product = ff_q_wer_endpoint_product_partial * S ((S (ff_i_wer_endpoint_product)) * ff_v_wer_endpoint_product) + (ff_r_wer_endpoint_product))) /\ ((((exists ff_h_wer_endpoint_product_successor. ff_h_wer_endpoint_product_successor + S (ff_s_wer_endpoint_product) = S ((S (S ff_i_wer_endpoint_product)) * ff_v_wer_endpoint_product)) /\ exists ff_q_wer_endpoint_product_successor. ff_u_wer_endpoint_product = ff_q_wer_endpoint_product_successor * S ((S (S ff_i_wer_endpoint_product)) * ff_v_wer_endpoint_product) + (ff_s_wer_endpoint_product))) /\ ff_s_wer_endpoint_product = ff_r_wer_endpoint_product * ff_p_wer_endpoint_product)))))))) -> F = P * n

Structural proof guide

Generated structural guide

Restore the final factor l+2 after the leading unit has been absorbed.

Use the direct prerequisites beta_range_two_product_is_factorial_succ, factorial_succ_decompose, factorial_functional, mul_congr as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (3).

Referenced ingredients

PA00BG beta_range_two_product_is_factorial_succ PA0065 factorial_succ_decompose PA006B factorial_functional PA0050 mul_congr

Proof neighborhood

Direct dependencies

PA00BG beta_range_two_product_is_factorial_succ PA0065 factorial_succ_decompose PA006B factorial_functional PA0050 mul_congr

Direct dependents

PA00BJ prime_factorial_wilson_congruence

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro P
  5. 0005intro n
  6. 0006intro F
  7. 0007intro hterminal
  8. 0008intro hrange
  9. 0009intro hproduct
  10. 0010intro hfactorial
  11. 0011have hprefix_factorial : exists wer_factor_code_wer_endpoint_prefix_factorial wer_factor_scale_wer_endpoint_prefix_factorial. ((forall wer_range_index_wer_endpoint_prefix_factorial_range. (exists wer_range_gap_wer_endpoint_prefix_factorial_range. wer_range_gap_wer_endpoint_prefix_factorial_range + S wer_range_index_wer_endpoint_prefix_factorial_range = S l) -> (((exists ff_h_wer_endpoint_prefix_factorial_range_decoded. ff_h_wer_endpoint_prefix_factorial_range_decoded + S (1 + wer_range_index_wer_endpoint_prefix_factorial_range) = S ((S (wer_range_index_wer_endpoint_prefix_factorial_range)) * wer_factor_scale_wer_endpoint_prefix_factorial)) /\ exists ff_q_wer_endpoint_prefix_factorial_range_decoded. wer_factor_code_wer_endpoint_prefix_factorial = ff_q_wer_endpoint_prefix_factorial_range_decoded * S ((S (wer_range_index_wer_endpoint_prefix_factorial_range)) * wer_factor_scale_wer_endpoint_prefix_factorial) + (1 + wer_range_index_wer_endpoint_prefix_factorial_range)))) /\ (exists ff_u_wer_endpoint_prefix_factorial_product ff_v_wer_endpoint_prefix_factorial_product. ((((exists ff_h_wer_endpoint_prefix_factorial_product_start. ff_h_wer_endpoint_prefix_factorial_product_start + S (1) = S ((S (0)) * ff_v_wer_endpoint_prefix_factorial_product)) /\ exists ff_q_wer_endpoint_prefix_factorial_product_start. ff_u_wer_endpoint_prefix_factorial_product = ff_q_wer_endpoint_prefix_factorial_product_start * S ((S (0)) * ff_v_wer_endpoint_prefix_factorial_product) + (1))) /\ ((((exists ff_h_wer_endpoint_prefix_factorial_product_terminal. ff_h_wer_endpoint_prefix_factorial_product_terminal + S (P) = S ((S (S l)) * ff_v_wer_endpoint_prefix_factorial_product)) /\ exists ff_q_wer_endpoint_prefix_factorial_product_terminal. ff_u_wer_endpoint_prefix_factorial_product = ff_q_wer_endpoint_prefix_factorial_product_terminal * S ((S (S l)) * ff_v_wer_endpoint_prefix_factorial_product) + (P))) /\ forall ff_i_wer_endpoint_prefix_factorial_product. (exists ff_lt_wer_endpoint_prefix_factorial_product_bound. ff_lt_wer_endpoint_prefix_factorial_product_bound + S ff_i_wer_endpoint_prefix_factorial_product = S l) -> exists ff_p_wer_endpoint_prefix_factorial_product ff_r_wer_endpoint_prefix_factorial_product ff_s_wer_endpoint_prefix_factorial_product. ((((exists ff_h_wer_endpoint_prefix_factorial_product_factor. ff_h_wer_endpoint_prefix_factorial_product_factor + S (ff_p_wer_endpoint_prefix_factorial_product) = S ((S (ff_i_wer_endpoint_prefix_factorial_product)) * wer_factor_scale_wer_endpoint_prefix_factorial)) /\ exists ff_q_wer_endpoint_prefix_factorial_product_factor. wer_factor_code_wer_endpoint_prefix_factorial = ff_q_wer_endpoint_prefix_factorial_product_factor * S ((S (ff_i_wer_endpoint_prefix_factorial_product)) * wer_factor_scale_wer_endpoint_prefix_factorial) + (ff_p_wer_endpoint_prefix_factorial_product))) /\ ((((exists ff_h_wer_endpoint_prefix_factorial_product_partial. ff_h_wer_endpoint_prefix_factorial_product_partial + S (ff_r_wer_endpoint_prefix_factorial_product) = S ((S (ff_i_wer_endpoint_prefix_factorial_product)) * ff_v_wer_endpoint_prefix_factorial_product)) /\ exists ff_q_wer_endpoint_prefix_factorial_product_partial. ff_u_wer_endpoint_prefix_factorial_product = ff_q_wer_endpoint_prefix_factorial_product_partial * S ((S (ff_i_wer_endpoint_prefix_factorial_product)) * ff_v_wer_endpoint_prefix_factorial_product) + (ff_r_wer_endpoint_prefix_factorial_product))) /\ ((((exists ff_h_wer_endpoint_prefix_factorial_product_successor. ff_h_wer_endpoint_prefix_factorial_product_successor + S (ff_s_wer_endpoint_prefix_factorial_product) = S ((S (S ff_i_wer_endpoint_prefix_factorial_product)) * ff_v_wer_endpoint_prefix_factorial_product)) /\ exists ff_q_wer_endpoint_prefix_factorial_product_successor. ff_u_wer_endpoint_prefix_factorial_product = ff_q_wer_endpoint_prefix_factorial_product_successor * S ((S (S ff_i_wer_endpoint_prefix_factorial_product)) * ff_v_wer_endpoint_prefix_factorial_product) + (ff_s_wer_endpoint_prefix_factorial_product))) /\ ff_s_wer_endpoint_prefix_factorial_product = ff_r_wer_endpoint_prefix_factorial_product * ff_p_wer_endpoint_prefix_factorial_product)))))))
  12. 0012specialize beta_range_two_product_is_factorial_succ l
  13. 0013specialize beta_range_two_product_is_factorial_succ b
  14. 0014specialize beta_range_two_product_is_factorial_succ c
  15. 0015specialize beta_range_two_product_is_factorial_succ P
  16. 0016apply beta_range_two_product_is_factorial_succ
  17. 0017exact hrange
  18. 0018exact hproduct
  19. 0019have hdecomp : exists R. ((exists wer_factor_code_wer_endpoint_previous_factorial wer_factor_scale_wer_endpoint_previous_factorial. ((forall wer_range_index_wer_endpoint_previous_factorial_range. (exists wer_range_gap_wer_endpoint_previous_factorial_range. wer_range_gap_wer_endpoint_previous_factorial_range + S wer_range_index_wer_endpoint_previous_factorial_range = S l) -> (((exists ff_h_wer_endpoint_previous_factorial_range_decoded. ff_h_wer_endpoint_previous_factorial_range_decoded + S (1 + wer_range_index_wer_endpoint_previous_factorial_range) = S ((S (wer_range_index_wer_endpoint_previous_factorial_range)) * wer_factor_scale_wer_endpoint_previous_factorial)) /\ exists ff_q_wer_endpoint_previous_factorial_range_decoded. wer_factor_code_wer_endpoint_previous_factorial = ff_q_wer_endpoint_previous_factorial_range_decoded * S ((S (wer_range_index_wer_endpoint_previous_factorial_range)) * wer_factor_scale_wer_endpoint_previous_factorial) + (1 + wer_range_index_wer_endpoint_previous_factorial_range)))) /\ (exists ff_u_wer_endpoint_previous_factorial_product ff_v_wer_endpoint_previous_factorial_product. ((((exists ff_h_wer_endpoint_previous_factorial_product_start. ff_h_wer_endpoint_previous_factorial_product_start + S (1) = S ((S (0)) * ff_v_wer_endpoint_previous_factorial_product)) /\ exists ff_q_wer_endpoint_previous_factorial_product_start. ff_u_wer_endpoint_previous_factorial_product = ff_q_wer_endpoint_previous_factorial_product_start * S ((S (0)) * ff_v_wer_endpoint_previous_factorial_product) + (1))) /\ ((((exists ff_h_wer_endpoint_previous_factorial_product_terminal. ff_h_wer_endpoint_previous_factorial_product_terminal + S (R) = S ((S (S l)) * ff_v_wer_endpoint_previous_factorial_product)) /\ exists ff_q_wer_endpoint_previous_factorial_product_terminal. ff_u_wer_endpoint_previous_factorial_product = ff_q_wer_endpoint_previous_factorial_product_terminal * S ((S (S l)) * ff_v_wer_endpoint_previous_factorial_product) + (R))) /\ forall ff_i_wer_endpoint_previous_factorial_product. (exists ff_lt_wer_endpoint_previous_factorial_product_bound. ff_lt_wer_endpoint_previous_factorial_product_bound + S ff_i_wer_endpoint_previous_factorial_product = S l) -> exists ff_p_wer_endpoint_previous_factorial_product ff_r_wer_endpoint_previous_factorial_product ff_s_wer_endpoint_previous_factorial_product. ((((exists ff_h_wer_endpoint_previous_factorial_product_factor. ff_h_wer_endpoint_previous_factorial_product_factor + S (ff_p_wer_endpoint_previous_factorial_product) = S ((S (ff_i_wer_endpoint_previous_factorial_product)) * wer_factor_scale_wer_endpoint_previous_factorial)) /\ exists ff_q_wer_endpoint_previous_factorial_product_factor. wer_factor_code_wer_endpoint_previous_factorial = ff_q_wer_endpoint_previous_factorial_product_factor * S ((S (ff_i_wer_endpoint_previous_factorial_product)) * wer_factor_scale_wer_endpoint_previous_factorial) + (ff_p_wer_endpoint_previous_factorial_product))) /\ ((((exists ff_h_wer_endpoint_previous_factorial_product_partial. ff_h_wer_endpoint_previous_factorial_product_partial + S (ff_r_wer_endpoint_previous_factorial_product) = S ((S (ff_i_wer_endpoint_previous_factorial_product)) * ff_v_wer_endpoint_previous_factorial_product)) /\ exists ff_q_wer_endpoint_previous_factorial_product_partial. ff_u_wer_endpoint_previous_factorial_product = ff_q_wer_endpoint_previous_factorial_product_partial * S ((S (ff_i_wer_endpoint_previous_factorial_product)) * ff_v_wer_endpoint_previous_factorial_product) + (ff_r_wer_endpoint_previous_factorial_product))) /\ ((((exists ff_h_wer_endpoint_previous_factorial_product_successor. ff_h_wer_endpoint_previous_factorial_product_successor + S (ff_s_wer_endpoint_previous_factorial_product) = S ((S (S ff_i_wer_endpoint_previous_factorial_product)) * ff_v_wer_endpoint_previous_factorial_product)) /\ exists ff_q_wer_endpoint_previous_factorial_product_successor. ff_u_wer_endpoint_previous_factorial_product = ff_q_wer_endpoint_previous_factorial_product_successor * S ((S (S ff_i_wer_endpoint_previous_factorial_product)) * ff_v_wer_endpoint_previous_factorial_product) + (ff_s_wer_endpoint_previous_factorial_product))) /\ ff_s_wer_endpoint_previous_factorial_product = ff_r_wer_endpoint_previous_factorial_product * ff_p_wer_endpoint_previous_factorial_product)))))))) /\ F = R * S (S l))
  20. 0020specialize factorial_succ_decompose (S l)
  21. 0021specialize factorial_succ_decompose n
  22. 0022specialize factorial_succ_decompose F
  23. 0023apply factorial_succ_decompose
  24. 0024exact hterminal
  25. 0025exact hfactorial
  26. 0026cases hdecomp
  27. 0027cases hdecomp_witness
  28. 0028have hpref : P = x
  29. 0029specialize factorial_functional (S l)
  30. 0030specialize factorial_functional P
  31. 0031specialize factorial_functional x
  32. 0032apply factorial_functional
  33. 0033exact hprefix_factorial
  34. 0034exact hdecomp_witness_left
  35. 0035trans x * S (S l)
  36. 0036exact hdecomp_witness_right
  37. 0037trans P * S (S l)
  38. 0038apply mul_congr
  39. 0039symm
  40. 0040exact hpref
  41. 0041refl
  42. 0042apply mul_congr
  43. 0043refl
  44. 0044symm
  45. 0045exact hterminal