BT00TD · Bertrand theorem

choose_out_of_range_zero

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

An out-of-range Choose value 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

∀ n. ∀ k. ∀ z. Lt(n,k) → Choose(n,k,z) → z = 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

PD0002 Lt PD0041 Choose

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall n k z. (exists bcf_lt_gap_bcloor_bound. bcf_lt_gap_bcloor_bound + S (n) = k) -> (((exists bcf_lt_gap_bcloor_choose_out_of_range. bcf_lt_gap_bcloor_choose_out_of_range + S (n) = k) /\ z = 0) \/ ((exists bcf_le_gap_bcloor_choose_in_range. bcf_le_gap_bcloor_choose_in_range + (k) = n) /\ (exists bcf_row_code_code_bcloor_choose bcf_row_code_scale_bcloor_choose bcf_row_scale_code_bcloor_choose bcf_row_scale_scale_bcloor_choose bcf_row_code_bcloor_choose bcf_row_scale_bcloor_choose. ((forall bcf_row_index_bcloor_choose_table. (exists bcf_lt_gap_bcloor_choose_table_row_bound. bcf_lt_gap_bcloor_choose_table_row_bound + S (bcf_row_index_bcloor_choose_table) = S (n)) -> exists bcf_row_code_bcloor_choose_table bcf_row_scale_bcloor_choose_table. ((((exists bcf_height_bcloor_choose_table_decoded_row_code. bcf_height_bcloor_choose_table_decoded_row_code + S (bcf_row_code_bcloor_choose_table) = S ((S (bcf_row_index_bcloor_choose_table)) * bcf_row_code_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_table_decoded_row_code. bcf_row_code_code_bcloor_choose = bcf_quotient_bcloor_choose_table_decoded_row_code * S ((S (bcf_row_index_bcloor_choose_table)) * bcf_row_code_scale_bcloor_choose) + (bcf_row_code_bcloor_choose_table))) /\ ((((exists bcf_height_bcloor_choose_table_decoded_row_scale. bcf_height_bcloor_choose_table_decoded_row_scale + S (bcf_row_scale_bcloor_choose_table) = S ((S (bcf_row_index_bcloor_choose_table)) * bcf_row_scale_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_table_decoded_row_scale. bcf_row_scale_code_bcloor_choose = bcf_quotient_bcloor_choose_table_decoded_row_scale * S ((S (bcf_row_index_bcloor_choose_table)) * bcf_row_scale_scale_bcloor_choose) + (bcf_row_scale_bcloor_choose_table))) /\ ((bcf_row_index_bcloor_choose_table = 0 /\ (forall bcf_index_bcloor_choose_table_zero_row. (exists bcf_lt_gap_bcloor_choose_table_zero_row_bound. bcf_lt_gap_bcloor_choose_table_zero_row_bound + S (bcf_index_bcloor_choose_table_zero_row) = S (n)) -> exists bcf_value_bcloor_choose_table_zero_row. ((((exists bcf_height_bcloor_choose_table_zero_row_entry. bcf_height_bcloor_choose_table_zero_row_entry + S (bcf_value_bcloor_choose_table_zero_row) = S ((S (bcf_index_bcloor_choose_table_zero_row)) * bcf_row_scale_bcloor_choose_table)) /\ exists bcf_quotient_bcloor_choose_table_zero_row_entry. bcf_row_code_bcloor_choose_table = bcf_quotient_bcloor_choose_table_zero_row_entry * S ((S (bcf_index_bcloor_choose_table_zero_row)) * bcf_row_scale_bcloor_choose_table) + (bcf_value_bcloor_choose_table_zero_row))) /\ ((bcf_index_bcloor_choose_table_zero_row = 0 /\ bcf_value_bcloor_choose_table_zero_row = 1) \/ exists bcf_predecessor_bcloor_choose_table_zero_row. bcf_index_bcloor_choose_table_zero_row = S bcf_predecessor_bcloor_choose_table_zero_row /\ bcf_value_bcloor_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bcloor_choose_table bcf_previous_code_bcloor_choose_table bcf_previous_scale_bcloor_choose_table. bcf_row_index_bcloor_choose_table = S bcf_predecessor_bcloor_choose_table /\ ((((exists bcf_height_bcloor_choose_table_decoded_previous_code. bcf_height_bcloor_choose_table_decoded_previous_code + S (bcf_previous_code_bcloor_choose_table) = S ((S (bcf_predecessor_bcloor_choose_table)) * bcf_row_code_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_table_decoded_previous_code. bcf_row_code_code_bcloor_choose = bcf_quotient_bcloor_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bcloor_choose_table)) * bcf_row_code_scale_bcloor_choose) + (bcf_previous_code_bcloor_choose_table))) /\ ((((exists bcf_height_bcloor_choose_table_decoded_previous_scale. bcf_height_bcloor_choose_table_decoded_previous_scale + S (bcf_previous_scale_bcloor_choose_table) = S ((S (bcf_predecessor_bcloor_choose_table)) * bcf_row_scale_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_table_decoded_previous_scale. bcf_row_scale_code_bcloor_choose = bcf_quotient_bcloor_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bcloor_choose_table)) * bcf_row_scale_scale_bcloor_choose) + (bcf_previous_scale_bcloor_choose_table))) /\ (forall bcf_index_bcloor_choose_table_row_step. (exists bcf_lt_gap_bcloor_choose_table_row_step_bound. bcf_lt_gap_bcloor_choose_table_row_step_bound + S (bcf_index_bcloor_choose_table_row_step) = S (n)) -> exists bcf_value_bcloor_choose_table_row_step. ((((exists bcf_height_bcloor_choose_table_row_step_entry. bcf_height_bcloor_choose_table_row_step_entry + S (bcf_value_bcloor_choose_table_row_step) = S ((S (bcf_index_bcloor_choose_table_row_step)) * bcf_row_scale_bcloor_choose_table)) /\ exists bcf_quotient_bcloor_choose_table_row_step_entry. bcf_row_code_bcloor_choose_table = bcf_quotient_bcloor_choose_table_row_step_entry * S ((S (bcf_index_bcloor_choose_table_row_step)) * bcf_row_scale_bcloor_choose_table) + (bcf_value_bcloor_choose_table_row_step))) /\ ((bcf_index_bcloor_choose_table_row_step = 0 /\ bcf_value_bcloor_choose_table_row_step = 1) \/ exists bcf_predecessor_bcloor_choose_table_row_step bcf_left_bcloor_choose_table_row_step bcf_right_bcloor_choose_table_row_step. bcf_index_bcloor_choose_table_row_step = S bcf_predecessor_bcloor_choose_table_row_step /\ ((((exists bcf_height_bcloor_choose_table_row_step_previous_left. bcf_height_bcloor_choose_table_row_step_previous_left + S (bcf_left_bcloor_choose_table_row_step) = S ((S (bcf_predecessor_bcloor_choose_table_row_step)) * bcf_previous_scale_bcloor_choose_table)) /\ exists bcf_quotient_bcloor_choose_table_row_step_previous_left. bcf_previous_code_bcloor_choose_table = bcf_quotient_bcloor_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bcloor_choose_table_row_step)) * bcf_previous_scale_bcloor_choose_table) + (bcf_left_bcloor_choose_table_row_step))) /\ ((((exists bcf_height_bcloor_choose_table_row_step_previous_right. bcf_height_bcloor_choose_table_row_step_previous_right + S (bcf_right_bcloor_choose_table_row_step) = S ((S (S (bcf_predecessor_bcloor_choose_table_row_step))) * bcf_previous_scale_bcloor_choose_table)) /\ exists bcf_quotient_bcloor_choose_table_row_step_previous_right. bcf_previous_code_bcloor_choose_table = bcf_quotient_bcloor_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcloor_choose_table_row_step))) * bcf_previous_scale_bcloor_choose_table) + (bcf_right_bcloor_choose_table_row_step))) /\ bcf_value_bcloor_choose_table_row_step = bcf_left_bcloor_choose_table_row_step + bcf_right_bcloor_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bcloor_choose_decoded_row_code. bcf_height_bcloor_choose_decoded_row_code + S (bcf_row_code_bcloor_choose) = S ((S (n)) * bcf_row_code_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_decoded_row_code. bcf_row_code_code_bcloor_choose = bcf_quotient_bcloor_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcloor_choose) + (bcf_row_code_bcloor_choose))) /\ ((((exists bcf_height_bcloor_choose_decoded_row_scale. bcf_height_bcloor_choose_decoded_row_scale + S (bcf_row_scale_bcloor_choose) = S ((S (n)) * bcf_row_scale_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_decoded_row_scale. bcf_row_scale_code_bcloor_choose = bcf_quotient_bcloor_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcloor_choose) + (bcf_row_scale_bcloor_choose))) /\ (((exists bcf_height_bcloor_choose_decoded_value. bcf_height_bcloor_choose_decoded_value + S (z) = S ((S (k)) * bcf_row_scale_bcloor_choose)) /\ exists bcf_quotient_bcloor_choose_decoded_value. bcf_row_code_bcloor_choose = bcf_quotient_bcloor_choose_decoded_value * S ((S (k)) * bcf_row_scale_bcloor_choose) + (z))))))))) -> z = 0

Proof neighborhood

Direct theorem prerequisites

BT001I lt_not_le

Direct theorem dependents

BT00TJ choose_succ_succ

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

15 script commands · 5 reading checkpoints · 0 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 (1)
lt not le
01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro k
  3. L3
    intro z
  4. L4
    intro hbound
  5. L5
    intro hchoose
02Separate the logical casesL6–7

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

  1. L6
    cases hchoose
  2. L7
    cases hchoose_left
03Use earlier factsL8–8

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

  1. L8
    exact hchoose_left_right
04Separate the logical casesL9–10

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

  1. L9
    cases hchoose_right
  2. L10
    exfalso
05Use earlier factsL11–15

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

  1. L11
    specialize lt_not_le n
  2. L12
    specialize lt_not_le k
  3. L13
    apply lt_not_le
  4. L14
    exact hbound
  5. L15
    exact hchoose_right_left

Library-wide reading audit

Original defined command ledger · 15 lines
  1. 0001intro n
  2. 0002intro k
  3. 0003intro z
  4. 0004intro hbound
  5. 0005intro hchoose
  6. 0006cases hchoose
  7. 0007cases hchoose_left
  8. 0008exact hchoose_left_right
  9. 0009cases hchoose_right
  10. 0010exfalso
  11. 0011specialize lt_not_le n
  12. 0012specialize lt_not_le k
  13. 0013apply lt_not_le
  14. 0014exact hbound
  15. 0015exact hchoose_right_left