BT00Q3 · Bertrand theorem

power_divides_decidable

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

Divisibility by a relational power is constructively decidable.

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. ∀ e. ∀ a. PowerDivides(p,e,a) ∨ ¬PowerDivides(p,e,a)

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

PD0044 PowerDivides

2 occurrences

In local proof propositions

PD0003 Dvd PD0020 Pow

3 occurrences

Exact expanded native-PA statement
forall p e a. (exists bpv_result_decision. ((exists ff_b_decision_power ff_c_decision_power. ((forall ff_i_decision_power_repeat. (exists ff_lt_decision_power_repeat_bound. ff_lt_decision_power_repeat_bound + S ff_i_decision_power_repeat = e) -> (((exists ff_h_decision_power_repeat_decoded. ff_h_decision_power_repeat_decoded + S (p) = S ((S (ff_i_decision_power_repeat)) * ff_c_decision_power)) /\ exists ff_q_decision_power_repeat_decoded. ff_b_decision_power = ff_q_decision_power_repeat_decoded * S ((S (ff_i_decision_power_repeat)) * ff_c_decision_power) + (p)))) /\ (exists ff_u_decision_power_product ff_v_decision_power_product. ((((exists ff_h_decision_power_product_start. ff_h_decision_power_product_start + S (1) = S ((S (0)) * ff_v_decision_power_product)) /\ exists ff_q_decision_power_product_start. ff_u_decision_power_product = ff_q_decision_power_product_start * S ((S (0)) * ff_v_decision_power_product) + (1))) /\ ((((exists ff_h_decision_power_product_terminal. ff_h_decision_power_product_terminal + S (bpv_result_decision) = S ((S (e)) * ff_v_decision_power_product)) /\ exists ff_q_decision_power_product_terminal. ff_u_decision_power_product = ff_q_decision_power_product_terminal * S ((S (e)) * ff_v_decision_power_product) + (bpv_result_decision))) /\ forall ff_i_decision_power_product. (exists ff_lt_decision_power_product_bound. ff_lt_decision_power_product_bound + S ff_i_decision_power_product = e) -> exists ff_p_decision_power_product ff_r_decision_power_product ff_s_decision_power_product. ((((exists ff_h_decision_power_product_factor. ff_h_decision_power_product_factor + S (ff_p_decision_power_product) = S ((S (ff_i_decision_power_product)) * ff_c_decision_power)) /\ exists ff_q_decision_power_product_factor. ff_b_decision_power = ff_q_decision_power_product_factor * S ((S (ff_i_decision_power_product)) * ff_c_decision_power) + (ff_p_decision_power_product))) /\ ((((exists ff_h_decision_power_product_partial. ff_h_decision_power_product_partial + S (ff_r_decision_power_product) = S ((S (ff_i_decision_power_product)) * ff_v_decision_power_product)) /\ exists ff_q_decision_power_product_partial. ff_u_decision_power_product = ff_q_decision_power_product_partial * S ((S (ff_i_decision_power_product)) * ff_v_decision_power_product) + (ff_r_decision_power_product))) /\ ((((exists ff_h_decision_power_product_successor. ff_h_decision_power_product_successor + S (ff_s_decision_power_product) = S ((S (S ff_i_decision_power_product)) * ff_v_decision_power_product)) /\ exists ff_q_decision_power_product_successor. ff_u_decision_power_product = ff_q_decision_power_product_successor * S ((S (S ff_i_decision_power_product)) * ff_v_decision_power_product) + (ff_s_decision_power_product))) /\ ff_s_decision_power_product = ff_r_decision_power_product * ff_p_decision_power_product)))))))) /\ (exists bpv_factor_decision_divides. a = bpv_result_decision * bpv_factor_decision_divides))) \/ ~(exists bpv_result_decision. ((exists ff_b_decision_power ff_c_decision_power. ((forall ff_i_decision_power_repeat. (exists ff_lt_decision_power_repeat_bound. ff_lt_decision_power_repeat_bound + S ff_i_decision_power_repeat = e) -> (((exists ff_h_decision_power_repeat_decoded. ff_h_decision_power_repeat_decoded + S (p) = S ((S (ff_i_decision_power_repeat)) * ff_c_decision_power)) /\ exists ff_q_decision_power_repeat_decoded. ff_b_decision_power = ff_q_decision_power_repeat_decoded * S ((S (ff_i_decision_power_repeat)) * ff_c_decision_power) + (p)))) /\ (exists ff_u_decision_power_product ff_v_decision_power_product. ((((exists ff_h_decision_power_product_start. ff_h_decision_power_product_start + S (1) = S ((S (0)) * ff_v_decision_power_product)) /\ exists ff_q_decision_power_product_start. ff_u_decision_power_product = ff_q_decision_power_product_start * S ((S (0)) * ff_v_decision_power_product) + (1))) /\ ((((exists ff_h_decision_power_product_terminal. ff_h_decision_power_product_terminal + S (bpv_result_decision) = S ((S (e)) * ff_v_decision_power_product)) /\ exists ff_q_decision_power_product_terminal. ff_u_decision_power_product = ff_q_decision_power_product_terminal * S ((S (e)) * ff_v_decision_power_product) + (bpv_result_decision))) /\ forall ff_i_decision_power_product. (exists ff_lt_decision_power_product_bound. ff_lt_decision_power_product_bound + S ff_i_decision_power_product = e) -> exists ff_p_decision_power_product ff_r_decision_power_product ff_s_decision_power_product. ((((exists ff_h_decision_power_product_factor. ff_h_decision_power_product_factor + S (ff_p_decision_power_product) = S ((S (ff_i_decision_power_product)) * ff_c_decision_power)) /\ exists ff_q_decision_power_product_factor. ff_b_decision_power = ff_q_decision_power_product_factor * S ((S (ff_i_decision_power_product)) * ff_c_decision_power) + (ff_p_decision_power_product))) /\ ((((exists ff_h_decision_power_product_partial. ff_h_decision_power_product_partial + S (ff_r_decision_power_product) = S ((S (ff_i_decision_power_product)) * ff_v_decision_power_product)) /\ exists ff_q_decision_power_product_partial. ff_u_decision_power_product = ff_q_decision_power_product_partial * S ((S (ff_i_decision_power_product)) * ff_v_decision_power_product) + (ff_r_decision_power_product))) /\ ((((exists ff_h_decision_power_product_successor. ff_h_decision_power_product_successor + S (ff_s_decision_power_product) = S ((S (S ff_i_decision_power_product)) * ff_v_decision_power_product)) /\ exists ff_q_decision_power_product_successor. ff_u_decision_power_product = ff_q_decision_power_product_successor * S ((S (S ff_i_decision_power_product)) * ff_v_decision_power_product) + (ff_s_decision_power_product))) /\ ff_s_decision_power_product = ff_r_decision_power_product * ff_p_decision_power_product)))))))) /\ (exists bpv_factor_decision_divides. a = bpv_result_decision * bpv_factor_decision_divides)))

Proof neighborhood

Direct theorem prerequisites

BT0080 pow_exists BT003C multiple_decidable BT0082 pow_functional

Direct theorem dependents

BT00Q5 bounded_power_valuation_search

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

33 script commands · 13 reading checkpoints · 3 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)
pow existsmultiple decidablepow functional
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro e
  3. L3
    intro a
02Establish hpowerL4–7

Establish this local claim before using it. It is not an additional assumption.

  1. L4
    have hpower : ∃ r. Pow(p,e,r)Definitions: Pow(p,e,r)Original native command in the exact edition
  2. L5
    specialize pow_exists p
  3. L6
    specialize pow_exists e
  4. L7
    exact pow_exists
03Separate the logical casesL8–8

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

  1. L8
    cases hpower
04Establish hdivL9–12

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hdiv : Dvd(x,a) ∨ ¬Dvd(x,a)Definitions: Dvd(x,a)Original native command in the exact edition
  2. L10
    specialize multiple_decidable x
  3. L11
    specialize multiple_decidable a
  4. L12
    exact multiple_decidable
05Separate the logical casesL13–14

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

  1. L13
    cases hdiv
  2. L14
    left
06Construct an explicit witnessL15–15

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists x
07Separate the logical casesL16–16

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

  1. L16
    split
08Use earlier factsL17–18

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

  1. L17
    exact hpower_witness
  2. L18
    exact hdiv_left
09Separate the logical casesL19–19

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

  1. L19
    right
10Fix variables and assumptionsL20–20

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

  1. L20
    intro hother
11Separate the logical casesL21–22

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

  1. L21
    cases hother
  2. L22
    cases hother_witness
12Establish heqL23–32

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

  1. L23
    have heq : x1 = x
  2. L24
    specialize pow_functional p
  3. L25
    specialize pow_functional e
  4. L26
    specialize pow_functional x1
  5. L27
    specialize pow_functional x
  6. L28
    apply pow_functional
  7. L29
    exact hother_witness_left
  8. L30
    exact hpower_witness
  9. L31
    apply hdiv_right
  10. L32
    rewrite heq at hother_witness_right
13Use earlier factsL33–33

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

  1. L33
    exact hother_witness_right

Library-wide reading audit

Original defined command ledger · 33 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro a
  4. 0004have hpower : ∃ r. Pow(p,e,r)
    Exact native replay linehave hpower : exists r. (exists ff_b_decision_witness ff_c_decision_witness. ((forall ff_i_decision_witness_repeat. (exists ff_lt_decision_witness_repeat_bound. ff_lt_decision_witness_repeat_bound + S ff_i_decision_witness_repeat = e) -> (((exists ff_h_decision_witness_repeat_decoded. ff_h_decision_witness_repeat_decoded + S (p) = S ((S (ff_i_decision_witness_repeat)) * ff_c_decision_witness)) /\ exists ff_q_decision_witness_repeat_decoded. ff_b_decision_witness = ff_q_decision_witness_repeat_decoded * S ((S (ff_i_decision_witness_repeat)) * ff_c_decision_witness) + (p)))) /\ (exists ff_u_decision_witness_product ff_v_decision_witness_product. ((((exists ff_h_decision_witness_product_start. ff_h_decision_witness_product_start + S (1) = S ((S (0)) * ff_v_decision_witness_product)) /\ exists ff_q_decision_witness_product_start. ff_u_decision_witness_product = ff_q_decision_witness_product_start * S ((S (0)) * ff_v_decision_witness_product) + (1))) /\ ((((exists ff_h_decision_witness_product_terminal. ff_h_decision_witness_product_terminal + S (r) = S ((S (e)) * ff_v_decision_witness_product)) /\ exists ff_q_decision_witness_product_terminal. ff_u_decision_witness_product = ff_q_decision_witness_product_terminal * S ((S (e)) * ff_v_decision_witness_product) + (r))) /\ forall ff_i_decision_witness_product. (exists ff_lt_decision_witness_product_bound. ff_lt_decision_witness_product_bound + S ff_i_decision_witness_product = e) -> exists ff_p_decision_witness_product ff_r_decision_witness_product ff_s_decision_witness_product. ((((exists ff_h_decision_witness_product_factor. ff_h_decision_witness_product_factor + S (ff_p_decision_witness_product) = S ((S (ff_i_decision_witness_product)) * ff_c_decision_witness)) /\ exists ff_q_decision_witness_product_factor. ff_b_decision_witness = ff_q_decision_witness_product_factor * S ((S (ff_i_decision_witness_product)) * ff_c_decision_witness) + (ff_p_decision_witness_product))) /\ ((((exists ff_h_decision_witness_product_partial. ff_h_decision_witness_product_partial + S (ff_r_decision_witness_product) = S ((S (ff_i_decision_witness_product)) * ff_v_decision_witness_product)) /\ exists ff_q_decision_witness_product_partial. ff_u_decision_witness_product = ff_q_decision_witness_product_partial * S ((S (ff_i_decision_witness_product)) * ff_v_decision_witness_product) + (ff_r_decision_witness_product))) /\ ((((exists ff_h_decision_witness_product_successor. ff_h_decision_witness_product_successor + S (ff_s_decision_witness_product) = S ((S (S ff_i_decision_witness_product)) * ff_v_decision_witness_product)) /\ exists ff_q_decision_witness_product_successor. ff_u_decision_witness_product = ff_q_decision_witness_product_successor * S ((S (S ff_i_decision_witness_product)) * ff_v_decision_witness_product) + (ff_s_decision_witness_product))) /\ ff_s_decision_witness_product = ff_r_decision_witness_product * ff_p_decision_witness_product))))))))
  5. 0005specialize pow_exists p
  6. 0006specialize pow_exists e
  7. 0007exact pow_exists
  8. 0008cases hpower
  9. 0009have hdiv : Dvd(x,a) ∨ ¬Dvd(x,a)
    Exact native replay linehave hdiv : (exists q. a = x * q) \/ ~(exists q. a = x * q)
  10. 0010specialize multiple_decidable x
  11. 0011specialize multiple_decidable a
  12. 0012exact multiple_decidable
  13. 0013cases hdiv
  14. 0014left
  15. 0015exists x
  16. 0016split
  17. 0017exact hpower_witness
  18. 0018exact hdiv_left
  19. 0019right
  20. 0020intro hother
  21. 0021cases hother
  22. 0022cases hother_witness
  23. 0023have heq : x1 = x
  24. 0024specialize pow_functional p
  25. 0025specialize pow_functional e
  26. 0026specialize pow_functional x1
  27. 0027specialize pow_functional x
  28. 0028apply pow_functional
  29. 0029exact hother_witness_left
  30. 0030exact hpower_witness
  31. 0031apply hdiv_right
  32. 0032rewrite heq at hother_witness_right
  33. 0033exact hother_witness_right