BT00RK

factorial_nonzero

Alpha body-checked · checked-use disabled

A relational factorial value is never zero.

Exact expanded PA statement

forall n F. (exists ff_b_bfv_nonzero ff_c_bfv_nonzero. ((forall ff_i_bfv_nonzero_range. (exists ff_lt_bfv_nonzero_range_bound. ff_lt_bfv_nonzero_range_bound + S ff_i_bfv_nonzero_range = n) -> (((exists ff_h_bfv_nonzero_range_decoded. ff_h_bfv_nonzero_range_decoded + S (1 + ff_i_bfv_nonzero_range) = S ((S (ff_i_bfv_nonzero_range)) * ff_c_bfv_nonzero)) /\ exists ff_q_bfv_nonzero_range_decoded. ff_b_bfv_nonzero = ff_q_bfv_nonzero_range_decoded * S ((S (ff_i_bfv_nonzero_range)) * ff_c_bfv_nonzero) + (1 + ff_i_bfv_nonzero_range)))) /\ (exists ff_u_bfv_nonzero_product ff_v_bfv_nonzero_product. ((((exists ff_h_bfv_nonzero_product_start. ff_h_bfv_nonzero_product_start + S (1) = S ((S (0)) * ff_v_bfv_nonzero_product)) /\ exists ff_q_bfv_nonzero_product_start. ff_u_bfv_nonzero_product = ff_q_bfv_nonzero_product_start * S ((S (0)) * ff_v_bfv_nonzero_product) + (1))) /\ ((((exists ff_h_bfv_nonzero_product_terminal. ff_h_bfv_nonzero_product_terminal + S (F) = S ((S (n)) * ff_v_bfv_nonzero_product)) /\ exists ff_q_bfv_nonzero_product_terminal. ff_u_bfv_nonzero_product = ff_q_bfv_nonzero_product_terminal * S ((S (n)) * ff_v_bfv_nonzero_product) + (F))) /\ forall ff_i_bfv_nonzero_product. (exists ff_lt_bfv_nonzero_product_bound. ff_lt_bfv_nonzero_product_bound + S ff_i_bfv_nonzero_product = n) -> exists ff_p_bfv_nonzero_product ff_r_bfv_nonzero_product ff_s_bfv_nonzero_product. ((((exists ff_h_bfv_nonzero_product_factor. ff_h_bfv_nonzero_product_factor + S (ff_p_bfv_nonzero_product) = S ((S (ff_i_bfv_nonzero_product)) * ff_c_bfv_nonzero)) /\ exists ff_q_bfv_nonzero_product_factor. ff_b_bfv_nonzero = ff_q_bfv_nonzero_product_factor * S ((S (ff_i_bfv_nonzero_product)) * ff_c_bfv_nonzero) + (ff_p_bfv_nonzero_product))) /\ ((((exists ff_h_bfv_nonzero_product_partial. ff_h_bfv_nonzero_product_partial + S (ff_r_bfv_nonzero_product) = S ((S (ff_i_bfv_nonzero_product)) * ff_v_bfv_nonzero_product)) /\ exists ff_q_bfv_nonzero_product_partial. ff_u_bfv_nonzero_product = ff_q_bfv_nonzero_product_partial * S ((S (ff_i_bfv_nonzero_product)) * ff_v_bfv_nonzero_product) + (ff_r_bfv_nonzero_product))) /\ ((((exists ff_h_bfv_nonzero_product_successor. ff_h_bfv_nonzero_product_successor + S (ff_s_bfv_nonzero_product) = S ((S (S ff_i_bfv_nonzero_product)) * ff_v_bfv_nonzero_product)) /\ exists ff_q_bfv_nonzero_product_successor. ff_u_bfv_nonzero_product = ff_q_bfv_nonzero_product_successor * S ((S (S ff_i_bfv_nonzero_product)) * ff_v_bfv_nonzero_product) + (ff_s_bfv_nonzero_product))) /\ ff_s_bfv_nonzero_product = ff_r_bfv_nonzero_product * ff_p_bfv_nonzero_product)))))))) -> ~(F = 0)

Structural proof guide

A relational factorial value is never zero.

Direct prerequisites: factorial_zero, factorial_succ_decompose, succ_ne_zero, mul_ne_zero. The authored body proceeds by structural induction (1), case analysis (2), intermediate claims (4).

Proof neighborhood

Direct dependencies

BT0091 factorial_zero BT0092 factorial_succ_decompose BT000C succ_ne_zero BT0021 mul_ne_zero

Direct dependents

BT00RP prime_factorial_valuation_succ BT00XM central_binom_factorial_valuation_balance

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. 0002induction n
  3. 0003intro F
  4. 0004intro hfactorial
  5. 0005have hvalue : F = 1
  6. 0006specialize factorial_zero 0
  7. 0007specialize factorial_zero F
  8. 0008apply factorial_zero
  9. 0009refl
  10. 0010exact hfactorial
  11. 0011intro hzero
  12. 0012specialize succ_ne_zero 0
  13. 0013apply succ_ne_zero
  14. 0014trans F
  15. 0015symm
  16. 0016exact hvalue
  17. 0017exact hzero
  18. 0018intro F
  19. 0019intro hfactorial
  20. 0020have hdecomposition : exists R. (exists ff_b_bfv_nonzero_predecessor ff_c_bfv_nonzero_predecessor. ((forall ff_i_bfv_nonzero_predecessor_range. (exists ff_lt_bfv_nonzero_predecessor_range_bound. ff_lt_bfv_nonzero_predecessor_range_bound + S ff_i_bfv_nonzero_predecessor_range = n) -> (((exists ff_h_bfv_nonzero_predecessor_range_decoded. ff_h_bfv_nonzero_predecessor_range_decoded + S (1 + ff_i_bfv_nonzero_predecessor_range) = S ((S (ff_i_bfv_nonzero_predecessor_range)) * ff_c_bfv_nonzero_predecessor)) /\ exists ff_q_bfv_nonzero_predecessor_range_decoded. ff_b_bfv_nonzero_predecessor = ff_q_bfv_nonzero_predecessor_range_decoded * S ((S (ff_i_bfv_nonzero_predecessor_range)) * ff_c_bfv_nonzero_predecessor) + (1 + ff_i_bfv_nonzero_predecessor_range)))) /\ (exists ff_u_bfv_nonzero_predecessor_product ff_v_bfv_nonzero_predecessor_product. ((((exists ff_h_bfv_nonzero_predecessor_product_start. ff_h_bfv_nonzero_predecessor_product_start + S (1) = S ((S (0)) * ff_v_bfv_nonzero_predecessor_product)) /\ exists ff_q_bfv_nonzero_predecessor_product_start. ff_u_bfv_nonzero_predecessor_product = ff_q_bfv_nonzero_predecessor_product_start * S ((S (0)) * ff_v_bfv_nonzero_predecessor_product) + (1))) /\ ((((exists ff_h_bfv_nonzero_predecessor_product_terminal. ff_h_bfv_nonzero_predecessor_product_terminal + S (R) = S ((S (n)) * ff_v_bfv_nonzero_predecessor_product)) /\ exists ff_q_bfv_nonzero_predecessor_product_terminal. ff_u_bfv_nonzero_predecessor_product = ff_q_bfv_nonzero_predecessor_product_terminal * S ((S (n)) * ff_v_bfv_nonzero_predecessor_product) + (R))) /\ forall ff_i_bfv_nonzero_predecessor_product. (exists ff_lt_bfv_nonzero_predecessor_product_bound. ff_lt_bfv_nonzero_predecessor_product_bound + S ff_i_bfv_nonzero_predecessor_product = n) -> exists ff_p_bfv_nonzero_predecessor_product ff_r_bfv_nonzero_predecessor_product ff_s_bfv_nonzero_predecessor_product. ((((exists ff_h_bfv_nonzero_predecessor_product_factor. ff_h_bfv_nonzero_predecessor_product_factor + S (ff_p_bfv_nonzero_predecessor_product) = S ((S (ff_i_bfv_nonzero_predecessor_product)) * ff_c_bfv_nonzero_predecessor)) /\ exists ff_q_bfv_nonzero_predecessor_product_factor. ff_b_bfv_nonzero_predecessor = ff_q_bfv_nonzero_predecessor_product_factor * S ((S (ff_i_bfv_nonzero_predecessor_product)) * ff_c_bfv_nonzero_predecessor) + (ff_p_bfv_nonzero_predecessor_product))) /\ ((((exists ff_h_bfv_nonzero_predecessor_product_partial. ff_h_bfv_nonzero_predecessor_product_partial + S (ff_r_bfv_nonzero_predecessor_product) = S ((S (ff_i_bfv_nonzero_predecessor_product)) * ff_v_bfv_nonzero_predecessor_product)) /\ exists ff_q_bfv_nonzero_predecessor_product_partial. ff_u_bfv_nonzero_predecessor_product = ff_q_bfv_nonzero_predecessor_product_partial * S ((S (ff_i_bfv_nonzero_predecessor_product)) * ff_v_bfv_nonzero_predecessor_product) + (ff_r_bfv_nonzero_predecessor_product))) /\ ((((exists ff_h_bfv_nonzero_predecessor_product_successor. ff_h_bfv_nonzero_predecessor_product_successor + S (ff_s_bfv_nonzero_predecessor_product) = S ((S (S ff_i_bfv_nonzero_predecessor_product)) * ff_v_bfv_nonzero_predecessor_product)) /\ exists ff_q_bfv_nonzero_predecessor_product_successor. ff_u_bfv_nonzero_predecessor_product = ff_q_bfv_nonzero_predecessor_product_successor * S ((S (S ff_i_bfv_nonzero_predecessor_product)) * ff_v_bfv_nonzero_predecessor_product) + (ff_s_bfv_nonzero_predecessor_product))) /\ ff_s_bfv_nonzero_predecessor_product = ff_r_bfv_nonzero_predecessor_product * ff_p_bfv_nonzero_predecessor_product)))))))) /\ F = R * S n
  21. 0021specialize factorial_succ_decompose n
  22. 0022specialize factorial_succ_decompose (S n)
  23. 0023specialize factorial_succ_decompose F
  24. 0024apply factorial_succ_decompose
  25. 0025refl
  26. 0026exact hfactorial
  27. 0027cases hdecomposition
  28. 0028cases hdecomposition_witness
  29. 0029have hpredecessor : ~(x = 0)
  30. 0030intro hpredecessor_zero
  31. 0031specialize IH x
  32. 0032apply IH
  33. 0033exact hdecomposition_witness_left
  34. 0034exact hpredecessor_zero
  35. 0035have hsuccessor : ~(S n = 0)
  36. 0036specialize succ_ne_zero n
  37. 0037exact succ_ne_zero
  38. 0038intro hzero
  39. 0039specialize mul_ne_zero x
  40. 0040specialize mul_ne_zero (S n)
  41. 0041apply mul_ne_zero
  42. 0042exact hpredecessor
  43. 0043exact hsuccessor
  44. 0044trans F
  45. 0045symm
  46. 0046exact hdecomposition_witness_right
  47. 0047exact hzero