PA0049

beta_product_zero

Stable checked-use theorem · independently closed

The product of an empty decoded prefix is one.

Exact expanded PA statement

forall b c n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + n) /\ forall i. (exists h. h + S i = 0) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> n = 1

Structural proof guide

Generated structural guide

The product of an empty decoded prefix is one.

Use the direct prerequisites beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (4).

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA004B pow_zero PA0066 factorial_zero PA007I beta_sign_factor_product_power PA007N beta_product_pointwise_mul_exact PA007Q beta_product_pointwise_scale_mod PA007X beta_product_permutation_invariant PA0081 beta_product_pointwise_coprime PA00A0 beta_adjacent_target_pairs_product_power PA00B9 beta_adjacent_unit_pairs_product_one PA00BG beta_range_two_product_is_factorial_succ

Formal native tactic body

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

  1. 0001intro b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro hproduct
  5. 0005cases hproduct
  6. 0006cases hproduct_witness
  7. 0007cases hproduct_witness_witness
  8. 0008cases hproduct_witness_witness_right
  9. 0009specialize beta_at_unique x
  10. 0010specialize beta_at_unique x1
  11. 0011specialize beta_at_unique 0
  12. 0012specialize beta_at_unique n
  13. 0013specialize beta_at_unique 1
  14. 0014apply beta_at_unique
  15. 0015exact hproduct_witness_witness_right_left
  16. 0016exact hproduct_witness_witness_left