BT00RO · Bertrand theorem

prime_factorial_valuation_zero

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

The prime valuation of zero factorial is zero.

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

∀ p. ∀ n. ∀ e. n = 0 → Prime(p) → FactorialValuation(p,n,e) → e = 0

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0048 FactorialValuation

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall p n e. n = 0 -> ((~(p = 1) /\ forall frm_prime_left_bfv_prime frm_prime_right_bfv_prime. p = frm_prime_left_bfv_prime * frm_prime_right_bfv_prime -> frm_prime_left_bfv_prime = 1 \/ frm_prime_right_bfv_prime = 1)) -> (exists bfv_factorial_bfv_zero. ((exists ff_b_bfv_zero_factorial ff_c_bfv_zero_factorial. ((forall ff_i_bfv_zero_factorial_range. (exists ff_lt_bfv_zero_factorial_range_bound. ff_lt_bfv_zero_factorial_range_bound + S ff_i_bfv_zero_factorial_range = n) -> (((exists ff_h_bfv_zero_factorial_range_decoded. ff_h_bfv_zero_factorial_range_decoded + S (1 + ff_i_bfv_zero_factorial_range) = S ((S (ff_i_bfv_zero_factorial_range)) * ff_c_bfv_zero_factorial)) /\ exists ff_q_bfv_zero_factorial_range_decoded. ff_b_bfv_zero_factorial = ff_q_bfv_zero_factorial_range_decoded * S ((S (ff_i_bfv_zero_factorial_range)) * ff_c_bfv_zero_factorial) + (1 + ff_i_bfv_zero_factorial_range)))) /\ (exists ff_u_bfv_zero_factorial_product ff_v_bfv_zero_factorial_product. ((((exists ff_h_bfv_zero_factorial_product_start. ff_h_bfv_zero_factorial_product_start + S (1) = S ((S (0)) * ff_v_bfv_zero_factorial_product)) /\ exists ff_q_bfv_zero_factorial_product_start. ff_u_bfv_zero_factorial_product = ff_q_bfv_zero_factorial_product_start * S ((S (0)) * ff_v_bfv_zero_factorial_product) + (1))) /\ ((((exists ff_h_bfv_zero_factorial_product_terminal. ff_h_bfv_zero_factorial_product_terminal + S (bfv_factorial_bfv_zero) = S ((S (n)) * ff_v_bfv_zero_factorial_product)) /\ exists ff_q_bfv_zero_factorial_product_terminal. ff_u_bfv_zero_factorial_product = ff_q_bfv_zero_factorial_product_terminal * S ((S (n)) * ff_v_bfv_zero_factorial_product) + (bfv_factorial_bfv_zero))) /\ forall ff_i_bfv_zero_factorial_product. (exists ff_lt_bfv_zero_factorial_product_bound. ff_lt_bfv_zero_factorial_product_bound + S ff_i_bfv_zero_factorial_product = n) -> exists ff_p_bfv_zero_factorial_product ff_r_bfv_zero_factorial_product ff_s_bfv_zero_factorial_product. ((((exists ff_h_bfv_zero_factorial_product_factor. ff_h_bfv_zero_factorial_product_factor + S (ff_p_bfv_zero_factorial_product) = S ((S (ff_i_bfv_zero_factorial_product)) * ff_c_bfv_zero_factorial)) /\ exists ff_q_bfv_zero_factorial_product_factor. ff_b_bfv_zero_factorial = ff_q_bfv_zero_factorial_product_factor * S ((S (ff_i_bfv_zero_factorial_product)) * ff_c_bfv_zero_factorial) + (ff_p_bfv_zero_factorial_product))) /\ ((((exists ff_h_bfv_zero_factorial_product_partial. ff_h_bfv_zero_factorial_product_partial + S (ff_r_bfv_zero_factorial_product) = S ((S (ff_i_bfv_zero_factorial_product)) * ff_v_bfv_zero_factorial_product)) /\ exists ff_q_bfv_zero_factorial_product_partial. ff_u_bfv_zero_factorial_product = ff_q_bfv_zero_factorial_product_partial * S ((S (ff_i_bfv_zero_factorial_product)) * ff_v_bfv_zero_factorial_product) + (ff_r_bfv_zero_factorial_product))) /\ ((((exists ff_h_bfv_zero_factorial_product_successor. ff_h_bfv_zero_factorial_product_successor + S (ff_s_bfv_zero_factorial_product) = S ((S (S ff_i_bfv_zero_factorial_product)) * ff_v_bfv_zero_factorial_product)) /\ exists ff_q_bfv_zero_factorial_product_successor. ff_u_bfv_zero_factorial_product = ff_q_bfv_zero_factorial_product_successor * S ((S (S ff_i_bfv_zero_factorial_product)) * ff_v_bfv_zero_factorial_product) + (ff_s_bfv_zero_factorial_product))) /\ ff_s_bfv_zero_factorial_product = ff_r_bfv_zero_factorial_product * ff_p_bfv_zero_factorial_product)))))))) /\ (((exists bpv_gap_bfv_zero_valuation_exponent_bound. bpv_gap_bfv_zero_valuation_exponent_bound + e = bfv_factorial_bfv_zero) /\ (exists bpv_result_bfv_zero_valuation_selected. ((exists ff_b_bfv_zero_valuation_selected_power ff_c_bfv_zero_valuation_selected_power. ((forall ff_i_bfv_zero_valuation_selected_power_repeat. (exists ff_lt_bfv_zero_valuation_selected_power_repeat_bound. ff_lt_bfv_zero_valuation_selected_power_repeat_bound + S ff_i_bfv_zero_valuation_selected_power_repeat = e) -> (((exists ff_h_bfv_zero_valuation_selected_power_repeat_decoded. ff_h_bfv_zero_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_zero_valuation_selected_power_repeat)) * ff_c_bfv_zero_valuation_selected_power)) /\ exists ff_q_bfv_zero_valuation_selected_power_repeat_decoded. ff_b_bfv_zero_valuation_selected_power = ff_q_bfv_zero_valuation_selected_power_repeat_decoded * S ((S (ff_i_bfv_zero_valuation_selected_power_repeat)) * ff_c_bfv_zero_valuation_selected_power) + (p)))) /\ (exists ff_u_bfv_zero_valuation_selected_power_product ff_v_bfv_zero_valuation_selected_power_product. ((((exists ff_h_bfv_zero_valuation_selected_power_product_start. ff_h_bfv_zero_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_zero_valuation_selected_power_product)) /\ exists ff_q_bfv_zero_valuation_selected_power_product_start. ff_u_bfv_zero_valuation_selected_power_product = ff_q_bfv_zero_valuation_selected_power_product_start * S ((S (0)) * ff_v_bfv_zero_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_zero_valuation_selected_power_product_terminal. ff_h_bfv_zero_valuation_selected_power_product_terminal + S (bpv_result_bfv_zero_valuation_selected) = S ((S (e)) * ff_v_bfv_zero_valuation_selected_power_product)) /\ exists ff_q_bfv_zero_valuation_selected_power_product_terminal. ff_u_bfv_zero_valuation_selected_power_product = ff_q_bfv_zero_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_bfv_zero_valuation_selected_power_product) + (bpv_result_bfv_zero_valuation_selected))) /\ forall ff_i_bfv_zero_valuation_selected_power_product. (exists ff_lt_bfv_zero_valuation_selected_power_product_bound. ff_lt_bfv_zero_valuation_selected_power_product_bound + S ff_i_bfv_zero_valuation_selected_power_product = e) -> exists ff_p_bfv_zero_valuation_selected_power_product ff_r_bfv_zero_valuation_selected_power_product ff_s_bfv_zero_valuation_selected_power_product. ((((exists ff_h_bfv_zero_valuation_selected_power_product_factor. ff_h_bfv_zero_valuation_selected_power_product_factor + S (ff_p_bfv_zero_valuation_selected_power_product) = S ((S (ff_i_bfv_zero_valuation_selected_power_product)) * ff_c_bfv_zero_valuation_selected_power)) /\ exists ff_q_bfv_zero_valuation_selected_power_product_factor. ff_b_bfv_zero_valuation_selected_power = ff_q_bfv_zero_valuation_selected_power_product_factor * S ((S (ff_i_bfv_zero_valuation_selected_power_product)) * ff_c_bfv_zero_valuation_selected_power) + (ff_p_bfv_zero_valuation_selected_power_product))) /\ ((((exists ff_h_bfv_zero_valuation_selected_power_product_partial. ff_h_bfv_zero_valuation_selected_power_product_partial + S (ff_r_bfv_zero_valuation_selected_power_product) = S ((S (ff_i_bfv_zero_valuation_selected_power_product)) * ff_v_bfv_zero_valuation_selected_power_product)) /\ exists ff_q_bfv_zero_valuation_selected_power_product_partial. ff_u_bfv_zero_valuation_selected_power_product = ff_q_bfv_zero_valuation_selected_power_product_partial * S ((S (ff_i_bfv_zero_valuation_selected_power_product)) * ff_v_bfv_zero_valuation_selected_power_product) + (ff_r_bfv_zero_valuation_selected_power_product))) /\ ((((exists ff_h_bfv_zero_valuation_selected_power_product_successor. ff_h_bfv_zero_valuation_selected_power_product_successor + S (ff_s_bfv_zero_valuation_selected_power_product) = S ((S (S ff_i_bfv_zero_valuation_selected_power_product)) * ff_v_bfv_zero_valuation_selected_power_product)) /\ exists ff_q_bfv_zero_valuation_selected_power_product_successor. ff_u_bfv_zero_valuation_selected_power_product = ff_q_bfv_zero_valuation_selected_power_product_successor * S ((S (S ff_i_bfv_zero_valuation_selected_power_product)) * ff_v_bfv_zero_valuation_selected_power_product) + (ff_s_bfv_zero_valuation_selected_power_product))) /\ ff_s_bfv_zero_valuation_selected_power_product = ff_r_bfv_zero_valuation_selected_power_product * ff_p_bfv_zero_valuation_selected_power_product)))))))) /\ (exists bpv_factor_bfv_zero_valuation_selected_divides. bfv_factorial_bfv_zero = bpv_result_bfv_zero_valuation_selected * bpv_factor_bfv_zero_valuation_selected_divides)))) /\ forall bpv_candidate_bfv_zero_valuation. (exists bpv_gap_bfv_zero_valuation_candidate_bound. bpv_gap_bfv_zero_valuation_candidate_bound + bpv_candidate_bfv_zero_valuation = bfv_factorial_bfv_zero) -> (exists bpv_result_bfv_zero_valuation_candidate. ((exists ff_b_bfv_zero_valuation_candidate_power ff_c_bfv_zero_valuation_candidate_power. ((forall ff_i_bfv_zero_valuation_candidate_power_repeat. (exists ff_lt_bfv_zero_valuation_candidate_power_repeat_bound. ff_lt_bfv_zero_valuation_candidate_power_repeat_bound + S ff_i_bfv_zero_valuation_candidate_power_repeat = bpv_candidate_bfv_zero_valuation) -> (((exists ff_h_bfv_zero_valuation_candidate_power_repeat_decoded. ff_h_bfv_zero_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_zero_valuation_candidate_power_repeat)) * ff_c_bfv_zero_valuation_candidate_power)) /\ exists ff_q_bfv_zero_valuation_candidate_power_repeat_decoded. ff_b_bfv_zero_valuation_candidate_power = ff_q_bfv_zero_valuation_candidate_power_repeat_decoded * S ((S (ff_i_bfv_zero_valuation_candidate_power_repeat)) * ff_c_bfv_zero_valuation_candidate_power) + (p)))) /\ (exists ff_u_bfv_zero_valuation_candidate_power_product ff_v_bfv_zero_valuation_candidate_power_product. ((((exists ff_h_bfv_zero_valuation_candidate_power_product_start. ff_h_bfv_zero_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_zero_valuation_candidate_power_product)) /\ exists ff_q_bfv_zero_valuation_candidate_power_product_start. ff_u_bfv_zero_valuation_candidate_power_product = ff_q_bfv_zero_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bfv_zero_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bfv_zero_valuation_candidate_power_product_terminal. ff_h_bfv_zero_valuation_candidate_power_product_terminal + S (bpv_result_bfv_zero_valuation_candidate) = S ((S (bpv_candidate_bfv_zero_valuation)) * ff_v_bfv_zero_valuation_candidate_power_product)) /\ exists ff_q_bfv_zero_valuation_candidate_power_product_terminal. ff_u_bfv_zero_valuation_candidate_power_product = ff_q_bfv_zero_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_bfv_zero_valuation)) * ff_v_bfv_zero_valuation_candidate_power_product) + (bpv_result_bfv_zero_valuation_candidate))) /\ forall ff_i_bfv_zero_valuation_candidate_power_product. (exists ff_lt_bfv_zero_valuation_candidate_power_product_bound. ff_lt_bfv_zero_valuation_candidate_power_product_bound + S ff_i_bfv_zero_valuation_candidate_power_product = bpv_candidate_bfv_zero_valuation) -> exists ff_p_bfv_zero_valuation_candidate_power_product ff_r_bfv_zero_valuation_candidate_power_product ff_s_bfv_zero_valuation_candidate_power_product. ((((exists ff_h_bfv_zero_valuation_candidate_power_product_factor. ff_h_bfv_zero_valuation_candidate_power_product_factor + S (ff_p_bfv_zero_valuation_candidate_power_product) = S ((S (ff_i_bfv_zero_valuation_candidate_power_product)) * ff_c_bfv_zero_valuation_candidate_power)) /\ exists ff_q_bfv_zero_valuation_candidate_power_product_factor. ff_b_bfv_zero_valuation_candidate_power = ff_q_bfv_zero_valuation_candidate_power_product_factor * S ((S (ff_i_bfv_zero_valuation_candidate_power_product)) * ff_c_bfv_zero_valuation_candidate_power) + (ff_p_bfv_zero_valuation_candidate_power_product))) /\ ((((exists ff_h_bfv_zero_valuation_candidate_power_product_partial. ff_h_bfv_zero_valuation_candidate_power_product_partial + S (ff_r_bfv_zero_valuation_candidate_power_product) = S ((S (ff_i_bfv_zero_valuation_candidate_power_product)) * ff_v_bfv_zero_valuation_candidate_power_product)) /\ exists ff_q_bfv_zero_valuation_candidate_power_product_partial. ff_u_bfv_zero_valuation_candidate_power_product = ff_q_bfv_zero_valuation_candidate_power_product_partial * S ((S (ff_i_bfv_zero_valuation_candidate_power_product)) * ff_v_bfv_zero_valuation_candidate_power_product) + (ff_r_bfv_zero_valuation_candidate_power_product))) /\ ((((exists ff_h_bfv_zero_valuation_candidate_power_product_successor. ff_h_bfv_zero_valuation_candidate_power_product_successor + S (ff_s_bfv_zero_valuation_candidate_power_product) = S ((S (S ff_i_bfv_zero_valuation_candidate_power_product)) * ff_v_bfv_zero_valuation_candidate_power_product)) /\ exists ff_q_bfv_zero_valuation_candidate_power_product_successor. ff_u_bfv_zero_valuation_candidate_power_product = ff_q_bfv_zero_valuation_candidate_power_product_successor * S ((S (S ff_i_bfv_zero_valuation_candidate_power_product)) * ff_v_bfv_zero_valuation_candidate_power_product) + (ff_s_bfv_zero_valuation_candidate_power_product))) /\ ff_s_bfv_zero_valuation_candidate_power_product = ff_r_bfv_zero_valuation_candidate_power_product * ff_p_bfv_zero_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_bfv_zero_valuation_candidate_divides. bfv_factorial_bfv_zero = bpv_result_bfv_zero_valuation_candidate * bpv_factor_bfv_zero_valuation_candidate_divides))) -> (exists bpv_gap_bfv_zero_valuation_maximal. bpv_gap_bfv_zero_valuation_maximal + bpv_candidate_bfv_zero_valuation = e)))) -> e = 0

Proof neighborhood

Direct theorem prerequisites

BT0091 factorial_zero BT00RL prime_power_valuation_one_zero

Direct theorem dependents

BT00T1 prime_factorial_valuation_eq_legendre_sum

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

21 script commands · 4 reading checkpoints · 1 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 (2)
factorial zeroprime power valuation one zero
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro e
  4. L4
    intro hn
  5. L5
    intro hp
  6. L6
    intro hvaluation
02Separate the logical casesL7–8

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

  1. L7
    cases hvaluation
  2. L8
    cases hvaluation_witness
03Establish hfactorial_valueL9–18

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

  1. L9
    have hfactorial_value : x = 1
  2. L10
    specialize factorial_zero n
  3. L11
    specialize factorial_zero x
  4. L12
    apply factorial_zero
  5. L13
    exact hn
  6. L14
    exact hvaluation_witness_left
  7. L15
    specialize prime_power_valuation_one_zero p
  8. L16
    specialize prime_power_valuation_one_zero x
  9. L17
    specialize prime_power_valuation_one_zero e
  10. L18
    apply prime_power_valuation_one_zero
04Use earlier factsL19–21

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

  1. L19
    exact hfactorial_value
  2. L20
    exact hp
  3. L21
    exact hvaluation_witness_right

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro e
  4. 0004intro hn
  5. 0005intro hp
  6. 0006intro hvaluation
  7. 0007cases hvaluation
  8. 0008cases hvaluation_witness
  9. 0009have hfactorial_value : x = 1
  10. 0010specialize factorial_zero n
  11. 0011specialize factorial_zero x
  12. 0012apply factorial_zero
  13. 0013exact hn
  14. 0014exact hvaluation_witness_left
  15. 0015specialize prime_power_valuation_one_zero p
  16. 0016specialize prime_power_valuation_one_zero x
  17. 0017specialize prime_power_valuation_one_zero e
  18. 0018apply prime_power_valuation_one_zero
  19. 0019exact hfactorial_value
  20. 0020exact hp
  21. 0021exact hvaluation_witness_right