SK0019

prime_valuation_divisible_power_root_bounded

Construct a k-th root from divisibility of every prime valuation by strict full-prime-power descent; every quotient and recursive root is actually derived.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

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.

For n>1 the exponent gcd and a real beta table classify and witness all positive root degrees. The unit n=1 has a separate uniform certificate for every positive degree. Zero is excluded. NaturalSquarefreeDecomposition is deliberately distinct from the unrelated polynomial definition.

Exact theorem in conservative defined notation

∀ B. ∀ n. ∀ k. ¬n = 0 → ¬k = 0 → PrimeValuationsDivisible(n,k) → Lt(n,B) → ∃ x. Pow(x,k,n)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PrimeValuationsDivisible(n,k) · 1Lt(a,b) · 2Dvd(d,n) · 2Prime(p) · 1Pow(a,e,z) · 4BoundedPowerValuation(p,n,b,e) · 1

Actual proof prerequisites

factor_permutation_below_zero_impossible · checked external prerequisiteeq_decidable · checked external prerequisitepower_value_eq_transportpower_one_base_existsprime_valuation_strict_cofactor_exists · checked external prerequisitepower_divisible_exponent_rootprime_valuation_divisibility_cofactorlt_of_lt_of_le · checked external prerequisitele_of_succ_le_succ · checked external prerequisitepower_product_construct
Original expanded first-order statement 
forall B n k. ~(n = 0) -> ~(k = 0) -> (forall ppf_prime_root_divisibility ppf_exponent_root_divisibility. (~((ppf_prime_root_divisibility) = 1) /\ forall pvs_left_root_divisibilitydomain pvs_right_root_divisibilitydomain. (ppf_prime_root_divisibility) = pvs_left_root_divisibilitydomain * pvs_right_root_divisibilitydomain -> pvs_left_root_divisibilitydomain = 1 \/ pvs_right_root_divisibilitydomain = 1) -> (((exists bpd_gap_pvs_root_divisibilityvaluation_selected_bound. bpd_gap_pvs_root_divisibilityvaluation_selected_bound + (ppf_exponent_root_divisibility) = (n)) /\ (exists bpvi_result_pvs_root_divisibilityvaluation_selected. ((exists bpvi_b_pvs_root_divisibilityvaluation_selected_power bpvi_c_pvs_root_divisibilityvaluation_selected_power. ((forall bpvi_i_pvs_root_divisibilityvaluation_selected_power. (exists bpvi_repeat_gap_pvs_root_divisibilityvaluation_selected_power. bpvi_repeat_gap_pvs_root_divisibilityvaluation_selected_power + S bpvi_i_pvs_root_divisibilityvaluation_selected_power = ppf_exponent_root_divisibility) -> (((exists bpvi_h_pvs_root_divisibilityvaluation_selected_power_repeat. bpvi_h_pvs_root_divisibilityvaluation_selected_power_repeat + S (ppf_prime_root_divisibility) = S ((S (bpvi_i_pvs_root_divisibilityvaluation_selected_power)) * bpvi_c_pvs_root_divisibilityvaluation_selected_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_selected_power_repeat. bpvi_b_pvs_root_divisibilityvaluation_selected_power = bpvi_q_pvs_root_divisibilityvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_root_divisibilityvaluation_selected_power)) * bpvi_c_pvs_root_divisibilityvaluation_selected_power) + (ppf_prime_root_divisibility)))) /\ (exists bpvi_u_pvs_root_divisibilityvaluation_selected_power bpvi_v_pvs_root_divisibilityvaluation_selected_power. ((((exists bpvi_h_pvs_root_divisibilityvaluation_selected_power_start. bpvi_h_pvs_root_divisibilityvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_root_divisibilityvaluation_selected_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_selected_power_start. bpvi_u_pvs_root_divisibilityvaluation_selected_power = bpvi_q_pvs_root_divisibilityvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_root_divisibilityvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_root_divisibilityvaluation_selected_power_terminal. bpvi_h_pvs_root_divisibilityvaluation_selected_power_terminal + S (bpvi_result_pvs_root_divisibilityvaluation_selected) = S ((S (ppf_exponent_root_divisibility)) * bpvi_v_pvs_root_divisibilityvaluation_selected_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_selected_power_terminal. bpvi_u_pvs_root_divisibilityvaluation_selected_power = bpvi_q_pvs_root_divisibilityvaluation_selected_power_terminal * S ((S (ppf_exponent_root_divisibility)) * bpvi_v_pvs_root_divisibilityvaluation_selected_power) + (bpvi_result_pvs_root_divisibilityvaluation_selected))) /\ forall bpvi_j_pvs_root_divisibilityvaluation_selected_power. (exists bpvi_product_gap_pvs_root_divisibilityvaluation_selected_power. bpvi_product_gap_pvs_root_divisibilityvaluation_selected_power + S bpvi_j_pvs_root_divisibilityvaluation_selected_power = ppf_exponent_root_divisibility) -> exists bpvi_factor_pvs_root_divisibilityvaluation_selected_power bpvi_partial_pvs_root_divisibilityvaluation_selected_power bpvi_successor_pvs_root_divisibilityvaluation_selected_power. ((((exists bpvi_h_pvs_root_divisibilityvaluation_selected_power_factor. bpvi_h_pvs_root_divisibilityvaluation_selected_power_factor + S (bpvi_factor_pvs_root_divisibilityvaluation_selected_power) = S ((S (bpvi_j_pvs_root_divisibilityvaluation_selected_power)) * bpvi_c_pvs_root_divisibilityvaluation_selected_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_selected_power_factor. bpvi_b_pvs_root_divisibilityvaluation_selected_power = bpvi_q_pvs_root_divisibilityvaluation_selected_power_factor * S ((S (bpvi_j_pvs_root_divisibilityvaluation_selected_power)) * bpvi_c_pvs_root_divisibilityvaluation_selected_power) + (bpvi_factor_pvs_root_divisibilityvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_root_divisibilityvaluation_selected_power_partial. bpvi_h_pvs_root_divisibilityvaluation_selected_power_partial + S (bpvi_partial_pvs_root_divisibilityvaluation_selected_power) = S ((S (bpvi_j_pvs_root_divisibilityvaluation_selected_power)) * bpvi_v_pvs_root_divisibilityvaluation_selected_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_selected_power_partial. bpvi_u_pvs_root_divisibilityvaluation_selected_power = bpvi_q_pvs_root_divisibilityvaluation_selected_power_partial * S ((S (bpvi_j_pvs_root_divisibilityvaluation_selected_power)) * bpvi_v_pvs_root_divisibilityvaluation_selected_power) + (bpvi_partial_pvs_root_divisibilityvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_root_divisibilityvaluation_selected_power_successor. bpvi_h_pvs_root_divisibilityvaluation_selected_power_successor + S (bpvi_successor_pvs_root_divisibilityvaluation_selected_power) = S ((S (S bpvi_j_pvs_root_divisibilityvaluation_selected_power)) * bpvi_v_pvs_root_divisibilityvaluation_selected_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_selected_power_successor. bpvi_u_pvs_root_divisibilityvaluation_selected_power = bpvi_q_pvs_root_divisibilityvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_root_divisibilityvaluation_selected_power)) * bpvi_v_pvs_root_divisibilityvaluation_selected_power) + (bpvi_successor_pvs_root_divisibilityvaluation_selected_power))) /\ bpvi_successor_pvs_root_divisibilityvaluation_selected_power = bpvi_partial_pvs_root_divisibilityvaluation_selected_power * bpvi_factor_pvs_root_divisibilityvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_root_divisibilityvaluation_selected. n = bpvi_result_pvs_root_divisibilityvaluation_selected * bpvi_divisor_factor_pvs_root_divisibilityvaluation_selected))) /\ forall bpd_candidate_pvs_root_divisibilityvaluation. (exists bpd_gap_pvs_root_divisibilityvaluation_candidate_bound. bpd_gap_pvs_root_divisibilityvaluation_candidate_bound + (bpd_candidate_pvs_root_divisibilityvaluation) = (n)) -> (exists bpvi_result_pvs_root_divisibilityvaluation_candidate. ((exists bpvi_b_pvs_root_divisibilityvaluation_candidate_power bpvi_c_pvs_root_divisibilityvaluation_candidate_power. ((forall bpvi_i_pvs_root_divisibilityvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_root_divisibilityvaluation_candidate_power. bpvi_repeat_gap_pvs_root_divisibilityvaluation_candidate_power + S bpvi_i_pvs_root_divisibilityvaluation_candidate_power = bpd_candidate_pvs_root_divisibilityvaluation) -> (((exists bpvi_h_pvs_root_divisibilityvaluation_candidate_power_repeat. bpvi_h_pvs_root_divisibilityvaluation_candidate_power_repeat + S (ppf_prime_root_divisibility) = S ((S (bpvi_i_pvs_root_divisibilityvaluation_candidate_power)) * bpvi_c_pvs_root_divisibilityvaluation_candidate_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_candidate_power_repeat. bpvi_b_pvs_root_divisibilityvaluation_candidate_power = bpvi_q_pvs_root_divisibilityvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_root_divisibilityvaluation_candidate_power)) * bpvi_c_pvs_root_divisibilityvaluation_candidate_power) + (ppf_prime_root_divisibility)))) /\ (exists bpvi_u_pvs_root_divisibilityvaluation_candidate_power bpvi_v_pvs_root_divisibilityvaluation_candidate_power. ((((exists bpvi_h_pvs_root_divisibilityvaluation_candidate_power_start. bpvi_h_pvs_root_divisibilityvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_root_divisibilityvaluation_candidate_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_candidate_power_start. bpvi_u_pvs_root_divisibilityvaluation_candidate_power = bpvi_q_pvs_root_divisibilityvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_root_divisibilityvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_root_divisibilityvaluation_candidate_power_terminal. bpvi_h_pvs_root_divisibilityvaluation_candidate_power_terminal + S (bpvi_result_pvs_root_divisibilityvaluation_candidate) = S ((S (bpd_candidate_pvs_root_divisibilityvaluation)) * bpvi_v_pvs_root_divisibilityvaluation_candidate_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_candidate_power_terminal. bpvi_u_pvs_root_divisibilityvaluation_candidate_power = bpvi_q_pvs_root_divisibilityvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_root_divisibilityvaluation)) * bpvi_v_pvs_root_divisibilityvaluation_candidate_power) + (bpvi_result_pvs_root_divisibilityvaluation_candidate))) /\ forall bpvi_j_pvs_root_divisibilityvaluation_candidate_power. (exists bpvi_product_gap_pvs_root_divisibilityvaluation_candidate_power. bpvi_product_gap_pvs_root_divisibilityvaluation_candidate_power + S bpvi_j_pvs_root_divisibilityvaluation_candidate_power = bpd_candidate_pvs_root_divisibilityvaluation) -> exists bpvi_factor_pvs_root_divisibilityvaluation_candidate_power bpvi_partial_pvs_root_divisibilityvaluation_candidate_power bpvi_successor_pvs_root_divisibilityvaluation_candidate_power. ((((exists bpvi_h_pvs_root_divisibilityvaluation_candidate_power_factor. bpvi_h_pvs_root_divisibilityvaluation_candidate_power_factor + S (bpvi_factor_pvs_root_divisibilityvaluation_candidate_power) = S ((S (bpvi_j_pvs_root_divisibilityvaluation_candidate_power)) * bpvi_c_pvs_root_divisibilityvaluation_candidate_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_candidate_power_factor. bpvi_b_pvs_root_divisibilityvaluation_candidate_power = bpvi_q_pvs_root_divisibilityvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_root_divisibilityvaluation_candidate_power)) * bpvi_c_pvs_root_divisibilityvaluation_candidate_power) + (bpvi_factor_pvs_root_divisibilityvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_root_divisibilityvaluation_candidate_power_partial. bpvi_h_pvs_root_divisibilityvaluation_candidate_power_partial + S (bpvi_partial_pvs_root_divisibilityvaluation_candidate_power) = S ((S (bpvi_j_pvs_root_divisibilityvaluation_candidate_power)) * bpvi_v_pvs_root_divisibilityvaluation_candidate_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_candidate_power_partial. bpvi_u_pvs_root_divisibilityvaluation_candidate_power = bpvi_q_pvs_root_divisibilityvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_root_divisibilityvaluation_candidate_power)) * bpvi_v_pvs_root_divisibilityvaluation_candidate_power) + (bpvi_partial_pvs_root_divisibilityvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_root_divisibilityvaluation_candidate_power_successor. bpvi_h_pvs_root_divisibilityvaluation_candidate_power_successor + S (bpvi_successor_pvs_root_divisibilityvaluation_candidate_power) = S ((S (S bpvi_j_pvs_root_divisibilityvaluation_candidate_power)) * bpvi_v_pvs_root_divisibilityvaluation_candidate_power)) /\ exists bpvi_q_pvs_root_divisibilityvaluation_candidate_power_successor. bpvi_u_pvs_root_divisibilityvaluation_candidate_power = bpvi_q_pvs_root_divisibilityvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_root_divisibilityvaluation_candidate_power)) * bpvi_v_pvs_root_divisibilityvaluation_candidate_power) + (bpvi_successor_pvs_root_divisibilityvaluation_candidate_power))) /\ bpvi_successor_pvs_root_divisibilityvaluation_candidate_power = bpvi_partial_pvs_root_divisibilityvaluation_candidate_power * bpvi_factor_pvs_root_divisibilityvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_root_divisibilityvaluation_candidate. n = bpvi_result_pvs_root_divisibilityvaluation_candidate * bpvi_divisor_factor_pvs_root_divisibilityvaluation_candidate)) -> (exists bpd_gap_pvs_root_divisibilityvaluation_maximal. bpd_gap_pvs_root_divisibilityvaluation_maximal + (bpd_candidate_pvs_root_divisibilityvaluation) = (ppf_exponent_root_divisibility))) -> (exists pvs_factor_root_divisibilitydivides. (ppf_exponent_root_divisibility) = (k) * pvs_factor_root_divisibilitydivides)) -> (exists pvs_gap_root_bound. pvs_gap_root_bound + S (n) = (B)) -> exists r. (exists pa_b_pvs_root_result pa_c_pvs_root_result. ((forall pa_i_pvs_root_result_repeat. (exists pa_lt_pvs_root_result_repeat_bound. pa_lt_pvs_root_result_repeat_bound + S pa_i_pvs_root_result_repeat = k) -> (((exists pa_h_pvs_root_result_repeat_decoded. pa_h_pvs_root_result_repeat_decoded + S (r) = S ((S (pa_i_pvs_root_result_repeat)) * pa_c_pvs_root_result)) /\ exists pa_q_pvs_root_result_repeat_decoded. pa_b_pvs_root_result = pa_q_pvs_root_result_repeat_decoded * S ((S (pa_i_pvs_root_result_repeat)) * pa_c_pvs_root_result) + (r)))) /\ (exists pa_u_pvs_root_result_product pa_v_pvs_root_result_product. ((((exists pa_h_pvs_root_result_product_start. pa_h_pvs_root_result_product_start + S (1) = S ((S (0)) * pa_v_pvs_root_result_product)) /\ exists pa_q_pvs_root_result_product_start. pa_u_pvs_root_result_product = pa_q_pvs_root_result_product_start * S ((S (0)) * pa_v_pvs_root_result_product) + (1))) /\ ((((exists pa_h_pvs_root_result_product_terminal. pa_h_pvs_root_result_product_terminal + S (n) = S ((S (k)) * pa_v_pvs_root_result_product)) /\ exists pa_q_pvs_root_result_product_terminal. pa_u_pvs_root_result_product = pa_q_pvs_root_result_product_terminal * S ((S (k)) * pa_v_pvs_root_result_product) + (n))) /\ forall pa_i_pvs_root_result_product. (exists pa_lt_pvs_root_result_product_bound. pa_lt_pvs_root_result_product_bound + S pa_i_pvs_root_result_product = k) -> exists pa_p_pvs_root_result_product pa_r_pvs_root_result_product pa_s_pvs_root_result_product. ((((exists pa_h_pvs_root_result_product_factor. pa_h_pvs_root_result_product_factor + S (pa_p_pvs_root_result_product) = S ((S (pa_i_pvs_root_result_product)) * pa_c_pvs_root_result)) /\ exists pa_q_pvs_root_result_product_factor. pa_b_pvs_root_result = pa_q_pvs_root_result_product_factor * S ((S (pa_i_pvs_root_result_product)) * pa_c_pvs_root_result) + (pa_p_pvs_root_result_product))) /\ ((((exists pa_h_pvs_root_result_product_partial. pa_h_pvs_root_result_product_partial + S (pa_r_pvs_root_result_product) = S ((S (pa_i_pvs_root_result_product)) * pa_v_pvs_root_result_product)) /\ exists pa_q_pvs_root_result_product_partial. pa_u_pvs_root_result_product = pa_q_pvs_root_result_product_partial * S ((S (pa_i_pvs_root_result_product)) * pa_v_pvs_root_result_product) + (pa_r_pvs_root_result_product))) /\ ((((exists pa_h_pvs_root_result_product_successor. pa_h_pvs_root_result_product_successor + S (pa_s_pvs_root_result_product) = S ((S (S pa_i_pvs_root_result_product)) * pa_v_pvs_root_result_product)) /\ exists pa_q_pvs_root_result_product_successor. pa_u_pvs_root_result_product = pa_q_pvs_root_result_product_successor * S ((S (S pa_i_pvs_root_result_product)) * pa_v_pvs_root_result_product) + (pa_s_pvs_root_result_product))) /\ pa_s_pvs_root_result_product = pa_r_pvs_root_result_product * pa_p_pvs_root_result_product))))))))

Complete tactic proof in conservative notation

All 111 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

111 script commands · 26 reading checkpoints · 5 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 (5)
power value eq transportpower one base existspower divisible exponent rootprime valuation divisibility cofactorpower product construct
01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–8

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
  2. L3
    intro n
  3. L4
    intro k
  4. L5
    intro hn
  5. L6
    intro hk
  6. L7
    intro hvalues
  7. L8
    intro hbound
03Separate the logical casesL9–9

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

  1. L9
    exfalso
04Use earlier factsL10–12

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

  1. L10
    specialize factor_permutation_below_zero_impossible (n)
  2. L11
    apply factor_permutation_below_zero_impossible
  3. L12
    exact hbound
05Fix variables and assumptionsL13–18

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

  1. L13
    intro n
  2. L14
    intro k
  3. L15
    intro hn
  4. L16
    intro hk
  5. L17
    intro hvalues
  6. L18
    intro hbound
06Establish hcaseL19–22

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

  1. L19
    have hcase : n = 1 \/ ~(n = 1)
  2. L20
    specialize eq_decidable (n)
  3. L21
    specialize eq_decidable (1)
  4. L22
    apply eq_decidable
07Separate the logical casesL23–23

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

  1. L23
    cases hcase
08Construct an explicit witnessL24–24

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

  1. L24
    exists 1
09Use earlier factsL25–29

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

  1. L25
    specialize power_value_eq_transport (1)
  2. L26
    specialize power_value_eq_transport (k)
  3. L27
    specialize power_value_eq_transport (1)
  4. L28
    specialize power_value_eq_transport (n)
  5. L29
    apply power_value_eq_transport
10Calculate and transport equalitiesL30–30

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L30
    symm
11Use earlier factsL31–33

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

  1. L31
    exact hcase_left
  2. L32
    specialize power_one_base_exists (k)
  3. L33
    apply power_one_base_exists
12Establish hfactorL34–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime valuation strict cofactor exists.

  1. L34
    have hfactor : ∃ p. ∃ e. ∃ P. ∃ u. Prime(p) ∧ (¬e = 0 ∧ (BoundedPowerValuation(p,n,n,e) ∧ (Pow(p,e,P) ∧ (n = P · u ∧ (¬u = 0 ∧ (¬Dvd(p,u) ∧ Lt(u,n)))))))Definitions: Prime(p)BoundedPowerValuation(p,n,n,e)Pow(p,e,P)Dvd(p,u)Lt(u,n)Original native command in the exact edition
  2. L35
    specialize prime_valuation_strict_cofactor_exists (n)
  3. L36
    apply prime_valuation_strict_cofactor_exists
  4. L37
    exact hn
  5. L38
    exact hcase_right
13Separate the logical casesL39–48

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

  1. L39
    cases hfactor
  2. L40
    cases hfactor_witness
  3. L41
    cases hfactor_witness_witness
  4. L42
    cases hfactor_witness_witness_witness
  5. L43
    cases hfactor_witness_witness_witness_witness
  6. L44
    cases hfactor_witness_witness_witness_witness_right
  7. L45
    cases hfactor_witness_witness_witness_witness_right_right
  8. L46
    cases hfactor_witness_witness_witness_witness_right_right_right
  9. L47
    cases hfactor_witness_witness_witness_witness_right_right_right_right
  10. L48
    cases hfactor_witness_witness_witness_witness_right_right_right_right_right
14Separate the logical casesL49–49

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

  1. L49
    cases hfactor_witness_witness_witness_witness_right_right_right_right_right_right
15Establish hquotientL50–55

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

  1. L50
    have hquotient : Dvd(k,x1)Definitions: Dvd(k,x1)Original native command in the exact edition
  2. L51
    specialize hvalues (x)
  3. L52
    specialize hvalues (x1)
  4. L53
    apply hvalues
  5. L54
    exact hfactor_witness_witness_witness_witness_left
  6. L55
    exact hfactor_witness_witness_witness_witness_right_right_left
16Separate the logical casesL56–56

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

  1. L56
    cases hquotient
17Establish hpowerrootL57–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power divisible exponent root.

  1. L57
    have hpowerroot : ∃ r. Pow(r,k,x2)Definitions: Pow(r,k,x2)Original native command in the exact edition
  2. L58
    specialize power_divisible_exponent_root (x)
  3. L59
    specialize power_divisible_exponent_root (x1)
  4. L60
    specialize power_divisible_exponent_root (k)
  5. L61
    specialize power_divisible_exponent_root (x4)
  6. L62
    specialize power_divisible_exponent_root (x2)
  7. L63
    apply power_divisible_exponent_root
  8. L64
    exact hquotient_witness
  9. L65
    exact hfactor_witness_witness_witness_witness_right_right_right_left
18Separate the logical casesL66–66

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

  1. L66
    cases hpowerroot
19Establish hrecL67–76

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

  1. L67
    have hrec : ∃ r. Pow(r,k,x3)Definitions: Pow(r,k,x3)Original native command in the exact edition
  2. L68
    specialize IH (x3)
  3. L69
    specialize IH (k)
  4. L70
    apply IH
  5. L71
    exact hfactor_witness_witness_witness_witness_right_right_right_right_right_left
  6. L72
    exact hk
  7. L73
    specialize prime_valuation_divisibility_cofactor (n)
  8. L74
    specialize prime_valuation_divisibility_cofactor (k)
  9. L75
    specialize prime_valuation_divisibility_cofactor (x)
  10. L76
    specialize prime_valuation_divisibility_cofactor (x1)
20Use earlier factsL77–86

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

  1. L77
    specialize prime_valuation_divisibility_cofactor (x2)
  2. L78
    specialize prime_valuation_divisibility_cofactor (x3)
  3. L79
    apply prime_valuation_divisibility_cofactor
  4. L80
    exact hfactor_witness_witness_witness_witness_left
  5. L81
    exact hfactor_witness_witness_witness_witness_right_right_right_right_right_left
  6. L82
    exact hfactor_witness_witness_witness_witness_right_right_right_right_left
  7. L83
    exact hfactor_witness_witness_witness_witness_right_right_right_left
  8. L84
    exact hfactor_witness_witness_witness_witness_right_right_right_right_right_right_left
  9. L85
    exact hvalues
  10. L86
    specialize lt_of_lt_of_le (x3)
21Use earlier factsL87–94

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

  1. L87
    specialize lt_of_lt_of_le (n)
  2. L88
    specialize lt_of_lt_of_le (B)
  3. L89
    apply lt_of_lt_of_le
  4. L90
    exact hfactor_witness_witness_witness_witness_right_right_right_right_right_right_right
  5. L91
    specialize le_of_succ_le_succ (n)
  6. L92
    specialize le_of_succ_le_succ (B)
  7. L93
    apply le_of_succ_le_succ
  8. L94
    exact hbound
22Separate the logical casesL95–95

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

  1. L95
    cases hrec
23Construct an explicit witnessL96–96

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

  1. L96
    exists x5 * x6
24Use earlier factsL97–101

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

  1. L97
    specialize power_value_eq_transport (x5 * x6)
  2. L98
    specialize power_value_eq_transport (k)
  3. L99
    specialize power_value_eq_transport (x2 * x3)
  4. L100
    specialize power_value_eq_transport (n)
  5. L101
    apply power_value_eq_transport
25Calculate and transport equalitiesL102–102

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L102
    symm
26Use earlier factsL103–111

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

  1. L103
    exact hfactor_witness_witness_witness_witness_right_right_right_right_left
  2. L104
    specialize power_product_construct (x5)
  3. L105
    specialize power_product_construct (x6)
  4. L106
    specialize power_product_construct (k)
  5. L107
    specialize power_product_construct (x2)
  6. L108
    specialize power_product_construct (x3)
  7. L109
    apply power_product_construct
  8. L110
    exact hpowerroot_witness
  9. L111
    exact hrec_witness

Library-wide reading audit

Original defined command ledger · 111 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro n
  4. 0004intro k
  5. 0005intro hn
  6. 0006intro hk
  7. 0007intro hvalues
  8. 0008intro hbound
  9. 0009exfalso
  10. 0010specialize factor_permutation_below_zero_impossible (n)
  11. 0011apply factor_permutation_below_zero_impossible
  12. 0012exact hbound
  13. 0013intro n
  14. 0014intro k
  15. 0015intro hn
  16. 0016intro hk
  17. 0017intro hvalues
  18. 0018intro hbound
  19. 0019have hcase : n = 1 \/ ~(n = 1)
  20. 0020specialize eq_decidable (n)
  21. 0021specialize eq_decidable (1)
  22. 0022apply eq_decidable
  23. 0023cases hcase
  24. 0024exists 1
  25. 0025specialize power_value_eq_transport (1)
  26. 0026specialize power_value_eq_transport (k)
  27. 0027specialize power_value_eq_transport (1)
  28. 0028specialize power_value_eq_transport (n)
  29. 0029apply power_value_eq_transport
  30. 0030symm
  31. 0031exact hcase_left
  32. 0032specialize power_one_base_exists (k)
  33. 0033apply power_one_base_exists
  34. 0034have hfactor : ∃ p. ∃ e. ∃ P. ∃ u. Prime(p) ∧ (¬e = 0 ∧ (BoundedPowerValuation(p,n,n,e) ∧ (Pow(p,e,P) ∧ (n = P · u ∧ (¬u = 0 ∧ (¬Dvd(p,u) ∧ Lt(u,n)))))))
  35. 0035specialize prime_valuation_strict_cofactor_exists (n)
  36. 0036apply prime_valuation_strict_cofactor_exists
  37. 0037exact hn
  38. 0038exact hcase_right
  39. 0039cases hfactor
  40. 0040cases hfactor_witness
  41. 0041cases hfactor_witness_witness
  42. 0042cases hfactor_witness_witness_witness
  43. 0043cases hfactor_witness_witness_witness_witness
  44. 0044cases hfactor_witness_witness_witness_witness_right
  45. 0045cases hfactor_witness_witness_witness_witness_right_right
  46. 0046cases hfactor_witness_witness_witness_witness_right_right_right
  47. 0047cases hfactor_witness_witness_witness_witness_right_right_right_right
  48. 0048cases hfactor_witness_witness_witness_witness_right_right_right_right_right
  49. 0049cases hfactor_witness_witness_witness_witness_right_right_right_right_right_right
  50. 0050have hquotient : Dvd(k,x1)
  51. 0051specialize hvalues (x)
  52. 0052specialize hvalues (x1)
  53. 0053apply hvalues
  54. 0054exact hfactor_witness_witness_witness_witness_left
  55. 0055exact hfactor_witness_witness_witness_witness_right_right_left
  56. 0056cases hquotient
  57. 0057have hpowerroot : ∃ r. Pow(r,k,x2)
  58. 0058specialize power_divisible_exponent_root (x)
  59. 0059specialize power_divisible_exponent_root (x1)
  60. 0060specialize power_divisible_exponent_root (k)
  61. 0061specialize power_divisible_exponent_root (x4)
  62. 0062specialize power_divisible_exponent_root (x2)
  63. 0063apply power_divisible_exponent_root
  64. 0064exact hquotient_witness
  65. 0065exact hfactor_witness_witness_witness_witness_right_right_right_left
  66. 0066cases hpowerroot
  67. 0067have hrec : ∃ r. Pow(r,k,x3)
  68. 0068specialize IH (x3)
  69. 0069specialize IH (k)
  70. 0070apply IH
  71. 0071exact hfactor_witness_witness_witness_witness_right_right_right_right_right_left
  72. 0072exact hk
  73. 0073specialize prime_valuation_divisibility_cofactor (n)
  74. 0074specialize prime_valuation_divisibility_cofactor (k)
  75. 0075specialize prime_valuation_divisibility_cofactor (x)
  76. 0076specialize prime_valuation_divisibility_cofactor (x1)
  77. 0077specialize prime_valuation_divisibility_cofactor (x2)
  78. 0078specialize prime_valuation_divisibility_cofactor (x3)
  79. 0079apply prime_valuation_divisibility_cofactor
  80. 0080exact hfactor_witness_witness_witness_witness_left
  81. 0081exact hfactor_witness_witness_witness_witness_right_right_right_right_right_left
  82. 0082exact hfactor_witness_witness_witness_witness_right_right_right_right_left
  83. 0083exact hfactor_witness_witness_witness_witness_right_right_right_left
  84. 0084exact hfactor_witness_witness_witness_witness_right_right_right_right_right_right_left
  85. 0085exact hvalues
  86. 0086specialize lt_of_lt_of_le (x3)
  87. 0087specialize lt_of_lt_of_le (n)
  88. 0088specialize lt_of_lt_of_le (B)
  89. 0089apply lt_of_lt_of_le
  90. 0090exact hfactor_witness_witness_witness_witness_right_right_right_right_right_right_right
  91. 0091specialize le_of_succ_le_succ (n)
  92. 0092specialize le_of_succ_le_succ (B)
  93. 0093apply le_of_succ_le_succ
  94. 0094exact hbound
  95. 0095cases hrec
  96. 0096exists x5 * x6
  97. 0097specialize power_value_eq_transport (x5 * x6)
  98. 0098specialize power_value_eq_transport (k)
  99. 0099specialize power_value_eq_transport (x2 * x3)
  100. 0100specialize power_value_eq_transport (n)
  101. 0101apply power_value_eq_transport
  102. 0102symm
  103. 0103exact hfactor_witness_witness_witness_witness_right_right_right_right_left
  104. 0104specialize power_product_construct (x5)
  105. 0105specialize power_product_construct (x6)
  106. 0106specialize power_product_construct (k)
  107. 0107specialize power_product_construct (x2)
  108. 0108specialize power_product_construct (x3)
  109. 0109apply power_product_construct
  110. 0110exact hpowerroot_witness
  111. 0111exact hrec_witness