PA00A3 · theorem

factorial_one_value

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

The relational factorial of one has value one.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ n. ∀ F. n = 1 → Factorial(n,F) → F = 1

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0023 Factorial

1 occurrences

In local proof propositions

PD0023 Factorial

1 occurrences

Exact expanded native-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

Proof neighborhood

Direct theorem prerequisites

PA0065 factorial_succ_decompose PA0066 factorial_zero PA0002 mul_one

Direct theorem dependents

PA00BG beta_range_two_product_is_factorial_succ PA00BJ prime_factorial_wilson_congruence

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

25 script commands · 5 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
factorial succ decomposefactorial zeromul one
01Fix variables and assumptionsL1–4

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro F
  3. L3
    intro hn
  4. L4
    intro hfactorial
02Establish hdecompL5–11

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factorial succ decompose.

  1. L5
    have hdecomp : ∃ R. Factorial(0,R) ∧ F = R · 1Definitions: Factorial(0,R)Original native command in the exact edition
  2. L6
    specialize factorial_succ_decompose 0
  3. L7
    specialize factorial_succ_decompose n
  4. L8
    specialize factorial_succ_decompose F
  5. L9
    apply factorial_succ_decompose
  6. L10
    exact hn
  7. L11
    exact hfactorial
03Separate the logical casesL12–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases hdecomp
  2. L13
    cases hdecomp_witness
04Establish hzeroL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factorial zero.

  1. L14
    have hzero : x = 1
  2. L15
    specialize factorial_zero 0
  3. L16
    specialize factorial_zero x
  4. L17
    apply factorial_zero
  5. L18
    refl
  6. L19
    exact hdecomp_witness_left
  7. L20
    trans x * 1
  8. L21
    exact hdecomp_witness_right
  9. L22
    trans x
  10. L23
    specialize mul_one x
05Use earlier factsL24–25

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L24
    exact mul_one
  2. L25
    exact hzero

Library-wide reading audit

Original defined command ledger · 25 lines
  1. 0001intro n
  2. 0002intro F
  3. 0003intro hn
  4. 0004intro hfactorial
  5. 0005have hdecomp : ∃ R. Factorial(0,R) ∧ F = R · 1
    Exact native replay linehave 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