PA00A3

factorial_one_value

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

The relational factorial of one has value one.

Exact expanded PA statement

forall n F. n = 1 -> (exists ff_b_wer_one ff_c_wer_one. ((forall ff_i_wer_one_range. (exists ff_lt_wer_one_range_bound. ff_lt_wer_one_range_bound + S ff_i_wer_one_range = n) -> (((exists ff_h_wer_one_range_decoded. ff_h_wer_one_range_decoded + S (1 + ff_i_wer_one_range) = S ((S (ff_i_wer_one_range)) * ff_c_wer_one)) /\ exists ff_q_wer_one_range_decoded. ff_b_wer_one = ff_q_wer_one_range_decoded * S ((S (ff_i_wer_one_range)) * ff_c_wer_one) + (1 + ff_i_wer_one_range)))) /\ (exists ff_u_wer_one_product ff_v_wer_one_product. ((((exists ff_h_wer_one_product_start. ff_h_wer_one_product_start + S (1) = S ((S (0)) * ff_v_wer_one_product)) /\ exists ff_q_wer_one_product_start. ff_u_wer_one_product = ff_q_wer_one_product_start * S ((S (0)) * ff_v_wer_one_product) + (1))) /\ ((((exists ff_h_wer_one_product_terminal. ff_h_wer_one_product_terminal + S (F) = S ((S (n)) * ff_v_wer_one_product)) /\ exists ff_q_wer_one_product_terminal. ff_u_wer_one_product = ff_q_wer_one_product_terminal * S ((S (n)) * ff_v_wer_one_product) + (F))) /\ forall ff_i_wer_one_product. (exists ff_lt_wer_one_product_bound. ff_lt_wer_one_product_bound + S ff_i_wer_one_product = n) -> exists ff_p_wer_one_product ff_r_wer_one_product ff_s_wer_one_product. ((((exists ff_h_wer_one_product_factor. ff_h_wer_one_product_factor + S (ff_p_wer_one_product) = S ((S (ff_i_wer_one_product)) * ff_c_wer_one)) /\ exists ff_q_wer_one_product_factor. ff_b_wer_one = ff_q_wer_one_product_factor * S ((S (ff_i_wer_one_product)) * ff_c_wer_one) + (ff_p_wer_one_product))) /\ ((((exists ff_h_wer_one_product_partial. ff_h_wer_one_product_partial + S (ff_r_wer_one_product) = S ((S (ff_i_wer_one_product)) * ff_v_wer_one_product)) /\ exists ff_q_wer_one_product_partial. ff_u_wer_one_product = ff_q_wer_one_product_partial * S ((S (ff_i_wer_one_product)) * ff_v_wer_one_product) + (ff_r_wer_one_product))) /\ ((((exists ff_h_wer_one_product_successor. ff_h_wer_one_product_successor + S (ff_s_wer_one_product) = S ((S (S ff_i_wer_one_product)) * ff_v_wer_one_product)) /\ exists ff_q_wer_one_product_successor. ff_u_wer_one_product = ff_q_wer_one_product_successor * S ((S (S ff_i_wer_one_product)) * ff_v_wer_one_product) + (ff_s_wer_one_product))) /\ ff_s_wer_one_product = ff_r_wer_one_product * ff_p_wer_one_product)))))))) -> F = 1

Structural proof guide

Generated structural guide

The relational factorial of one has value one.

Use the direct prerequisites factorial_succ_decompose, factorial_zero, mul_one as previously established PA formulas.

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

Referenced ingredients

PA0065 factorial_succ_decompose PA0066 factorial_zero PA0002 mul_one

Proof neighborhood

Direct dependencies

PA0065 factorial_succ_decompose PA0066 factorial_zero PA0002 mul_one

Direct dependents

PA00BG beta_range_two_product_is_factorial_succ 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 n
  2. 0002intro F
  3. 0003intro hn
  4. 0004intro hfactorial
  5. 0005have hdecomp : exists R. ((exists wer_factor_code_wer_one_zero wer_factor_scale_wer_one_zero. ((forall wer_range_index_wer_one_zero_range. (exists wer_range_gap_wer_one_zero_range. wer_range_gap_wer_one_zero_range + S wer_range_index_wer_one_zero_range = 0) -> (((exists ff_h_wer_one_zero_range_decoded. ff_h_wer_one_zero_range_decoded + S (1 + wer_range_index_wer_one_zero_range) = S ((S (wer_range_index_wer_one_zero_range)) * wer_factor_scale_wer_one_zero)) /\ exists ff_q_wer_one_zero_range_decoded. wer_factor_code_wer_one_zero = ff_q_wer_one_zero_range_decoded * S ((S (wer_range_index_wer_one_zero_range)) * wer_factor_scale_wer_one_zero) + (1 + wer_range_index_wer_one_zero_range)))) /\ (exists ff_u_wer_one_zero_product ff_v_wer_one_zero_product. ((((exists ff_h_wer_one_zero_product_start. ff_h_wer_one_zero_product_start + S (1) = S ((S (0)) * ff_v_wer_one_zero_product)) /\ exists ff_q_wer_one_zero_product_start. ff_u_wer_one_zero_product = ff_q_wer_one_zero_product_start * S ((S (0)) * ff_v_wer_one_zero_product) + (1))) /\ ((((exists ff_h_wer_one_zero_product_terminal. ff_h_wer_one_zero_product_terminal + S (R) = S ((S (0)) * ff_v_wer_one_zero_product)) /\ exists ff_q_wer_one_zero_product_terminal. ff_u_wer_one_zero_product = ff_q_wer_one_zero_product_terminal * S ((S (0)) * ff_v_wer_one_zero_product) + (R))) /\ forall ff_i_wer_one_zero_product. (exists ff_lt_wer_one_zero_product_bound. ff_lt_wer_one_zero_product_bound + S ff_i_wer_one_zero_product = 0) -> exists ff_p_wer_one_zero_product ff_r_wer_one_zero_product ff_s_wer_one_zero_product. ((((exists ff_h_wer_one_zero_product_factor. ff_h_wer_one_zero_product_factor + S (ff_p_wer_one_zero_product) = S ((S (ff_i_wer_one_zero_product)) * wer_factor_scale_wer_one_zero)) /\ exists ff_q_wer_one_zero_product_factor. wer_factor_code_wer_one_zero = ff_q_wer_one_zero_product_factor * S ((S (ff_i_wer_one_zero_product)) * wer_factor_scale_wer_one_zero) + (ff_p_wer_one_zero_product))) /\ ((((exists ff_h_wer_one_zero_product_partial. ff_h_wer_one_zero_product_partial + S (ff_r_wer_one_zero_product) = S ((S (ff_i_wer_one_zero_product)) * ff_v_wer_one_zero_product)) /\ exists ff_q_wer_one_zero_product_partial. ff_u_wer_one_zero_product = ff_q_wer_one_zero_product_partial * S ((S (ff_i_wer_one_zero_product)) * ff_v_wer_one_zero_product) + (ff_r_wer_one_zero_product))) /\ ((((exists ff_h_wer_one_zero_product_successor. ff_h_wer_one_zero_product_successor + S (ff_s_wer_one_zero_product) = S ((S (S ff_i_wer_one_zero_product)) * ff_v_wer_one_zero_product)) /\ exists ff_q_wer_one_zero_product_successor. ff_u_wer_one_zero_product = ff_q_wer_one_zero_product_successor * S ((S (S ff_i_wer_one_zero_product)) * ff_v_wer_one_zero_product) + (ff_s_wer_one_zero_product))) /\ ff_s_wer_one_zero_product = ff_r_wer_one_zero_product * ff_p_wer_one_zero_product)))))))) /\ F = R * 1)
  6. 0006specialize factorial_succ_decompose 0
  7. 0007specialize factorial_succ_decompose n
  8. 0008specialize factorial_succ_decompose F
  9. 0009apply factorial_succ_decompose
  10. 0010exact hn
  11. 0011exact hfactorial
  12. 0012cases hdecomp
  13. 0013cases hdecomp_witness
  14. 0014have hzero : x = 1
  15. 0015specialize factorial_zero 0
  16. 0016specialize factorial_zero x
  17. 0017apply factorial_zero
  18. 0018refl
  19. 0019exact hdecomp_witness_left
  20. 0020trans x * 1
  21. 0021exact hdecomp_witness_right
  22. 0022trans x
  23. 0023specialize mul_one x
  24. 0024exact mul_one
  25. 0025exact hzero