PV0011

prime_valuation_strict_cofactor_exists

Every positive nonunit has an actual full prime-power cofactor strictly smaller than itself; the exponent, power and nondivisibility are all constructed.

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.

This is a shared constructive tool, not an additional major blueprint goal. The list covers every prime divisor, has no repeated primes, and contains actual prime-power values. One uses the empty support; zero is excluded.

Exact theorem in conservative defined notation

∀ n. ¬n = 0 → ¬n = 1 → ∃ x. ∃ y. ∃ z. ∃ m. Prime(x) ∧ (¬y = 0 ∧ (BoundedPowerValuation(x,n,n,y) ∧ (Pow(x,y,z) ∧ (n = z · m ∧ (¬m = 0 ∧ (¬Dvd(x,m) ∧ Lt(m,n)))))))

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

Definition DAG

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

Actual proof prerequisites

prime_divisor_exists · checked external prerequisitepower_valuation_exists · checked external prerequisiteprime_divisor_power_valuation_nonzero · checked external prerequisitepower_valuation_exact_cofactor · checked external prerequisitepow_positive_exponent_base_dividesdivisor_one · checked external prerequisiteproper_factor_lt · checked external prerequisitemul_comm · checked external prerequisite
Original expanded first-order statement 
forall n. ~(n = 0) -> ~(n = 1) -> exists p e P u. (((~((p) = 1) /\ forall pvs_left_strict_cofactorprime pvs_right_strict_cofactorprime. (p) = pvs_left_strict_cofactorprime * pvs_right_strict_cofactorprime -> pvs_left_strict_cofactorprime = 1 \/ pvs_right_strict_cofactorprime = 1) /\ (((~(e = 0)) /\ (((((exists bpd_gap_pvs_strict_cofactorvaluation_selected_bound. bpd_gap_pvs_strict_cofactorvaluation_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_strict_cofactorvaluation_selected. ((exists bpvi_b_pvs_strict_cofactorvaluation_selected_power bpvi_c_pvs_strict_cofactorvaluation_selected_power. ((forall bpvi_i_pvs_strict_cofactorvaluation_selected_power. (exists bpvi_repeat_gap_pvs_strict_cofactorvaluation_selected_power. bpvi_repeat_gap_pvs_strict_cofactorvaluation_selected_power + S bpvi_i_pvs_strict_cofactorvaluation_selected_power = e) -> (((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_repeat. bpvi_h_pvs_strict_cofactorvaluation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_strict_cofactorvaluation_selected_power)) * bpvi_c_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_repeat. bpvi_b_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_strict_cofactorvaluation_selected_power)) * bpvi_c_pvs_strict_cofactorvaluation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_strict_cofactorvaluation_selected_power bpvi_v_pvs_strict_cofactorvaluation_selected_power. ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_start. bpvi_h_pvs_strict_cofactorvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_start. bpvi_u_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_terminal. bpvi_h_pvs_strict_cofactorvaluation_selected_power_terminal + S (bpvi_result_pvs_strict_cofactorvaluation_selected) = S ((S (e)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_terminal. bpvi_u_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power) + (bpvi_result_pvs_strict_cofactorvaluation_selected))) /\ forall bpvi_j_pvs_strict_cofactorvaluation_selected_power. (exists bpvi_product_gap_pvs_strict_cofactorvaluation_selected_power. bpvi_product_gap_pvs_strict_cofactorvaluation_selected_power + S bpvi_j_pvs_strict_cofactorvaluation_selected_power = e) -> exists bpvi_factor_pvs_strict_cofactorvaluation_selected_power bpvi_partial_pvs_strict_cofactorvaluation_selected_power bpvi_successor_pvs_strict_cofactorvaluation_selected_power. ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_factor. bpvi_h_pvs_strict_cofactorvaluation_selected_power_factor + S (bpvi_factor_pvs_strict_cofactorvaluation_selected_power) = S ((S (bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_c_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_factor. bpvi_b_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_factor * S ((S (bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_c_pvs_strict_cofactorvaluation_selected_power) + (bpvi_factor_pvs_strict_cofactorvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_partial. bpvi_h_pvs_strict_cofactorvaluation_selected_power_partial + S (bpvi_partial_pvs_strict_cofactorvaluation_selected_power) = S ((S (bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_partial. bpvi_u_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_partial * S ((S (bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power) + (bpvi_partial_pvs_strict_cofactorvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_selected_power_successor. bpvi_h_pvs_strict_cofactorvaluation_selected_power_successor + S (bpvi_successor_pvs_strict_cofactorvaluation_selected_power) = S ((S (S bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_selected_power_successor. bpvi_u_pvs_strict_cofactorvaluation_selected_power = bpvi_q_pvs_strict_cofactorvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_strict_cofactorvaluation_selected_power)) * bpvi_v_pvs_strict_cofactorvaluation_selected_power) + (bpvi_successor_pvs_strict_cofactorvaluation_selected_power))) /\ bpvi_successor_pvs_strict_cofactorvaluation_selected_power = bpvi_partial_pvs_strict_cofactorvaluation_selected_power * bpvi_factor_pvs_strict_cofactorvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_strict_cofactorvaluation_selected. n = bpvi_result_pvs_strict_cofactorvaluation_selected * bpvi_divisor_factor_pvs_strict_cofactorvaluation_selected))) /\ forall bpd_candidate_pvs_strict_cofactorvaluation. (exists bpd_gap_pvs_strict_cofactorvaluation_candidate_bound. bpd_gap_pvs_strict_cofactorvaluation_candidate_bound + (bpd_candidate_pvs_strict_cofactorvaluation) = (n)) -> (exists bpvi_result_pvs_strict_cofactorvaluation_candidate. ((exists bpvi_b_pvs_strict_cofactorvaluation_candidate_power bpvi_c_pvs_strict_cofactorvaluation_candidate_power. ((forall bpvi_i_pvs_strict_cofactorvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_strict_cofactorvaluation_candidate_power. bpvi_repeat_gap_pvs_strict_cofactorvaluation_candidate_power + S bpvi_i_pvs_strict_cofactorvaluation_candidate_power = bpd_candidate_pvs_strict_cofactorvaluation) -> (((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_repeat. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_c_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_repeat. bpvi_b_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_c_pvs_strict_cofactorvaluation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_strict_cofactorvaluation_candidate_power bpvi_v_pvs_strict_cofactorvaluation_candidate_power. ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_start. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_start. bpvi_u_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_terminal. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_terminal + S (bpvi_result_pvs_strict_cofactorvaluation_candidate) = S ((S (bpd_candidate_pvs_strict_cofactorvaluation)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_terminal. bpvi_u_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_strict_cofactorvaluation)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power) + (bpvi_result_pvs_strict_cofactorvaluation_candidate))) /\ forall bpvi_j_pvs_strict_cofactorvaluation_candidate_power. (exists bpvi_product_gap_pvs_strict_cofactorvaluation_candidate_power. bpvi_product_gap_pvs_strict_cofactorvaluation_candidate_power + S bpvi_j_pvs_strict_cofactorvaluation_candidate_power = bpd_candidate_pvs_strict_cofactorvaluation) -> exists bpvi_factor_pvs_strict_cofactorvaluation_candidate_power bpvi_partial_pvs_strict_cofactorvaluation_candidate_power bpvi_successor_pvs_strict_cofactorvaluation_candidate_power. ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_factor. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_factor + S (bpvi_factor_pvs_strict_cofactorvaluation_candidate_power) = S ((S (bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_c_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_factor. bpvi_b_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_c_pvs_strict_cofactorvaluation_candidate_power) + (bpvi_factor_pvs_strict_cofactorvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_partial. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_partial + S (bpvi_partial_pvs_strict_cofactorvaluation_candidate_power) = S ((S (bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_partial. bpvi_u_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power) + (bpvi_partial_pvs_strict_cofactorvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_strict_cofactorvaluation_candidate_power_successor. bpvi_h_pvs_strict_cofactorvaluation_candidate_power_successor + S (bpvi_successor_pvs_strict_cofactorvaluation_candidate_power) = S ((S (S bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power)) /\ exists bpvi_q_pvs_strict_cofactorvaluation_candidate_power_successor. bpvi_u_pvs_strict_cofactorvaluation_candidate_power = bpvi_q_pvs_strict_cofactorvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_strict_cofactorvaluation_candidate_power)) * bpvi_v_pvs_strict_cofactorvaluation_candidate_power) + (bpvi_successor_pvs_strict_cofactorvaluation_candidate_power))) /\ bpvi_successor_pvs_strict_cofactorvaluation_candidate_power = bpvi_partial_pvs_strict_cofactorvaluation_candidate_power * bpvi_factor_pvs_strict_cofactorvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_strict_cofactorvaluation_candidate. n = bpvi_result_pvs_strict_cofactorvaluation_candidate * bpvi_divisor_factor_pvs_strict_cofactorvaluation_candidate)) -> (exists bpd_gap_pvs_strict_cofactorvaluation_maximal. bpd_gap_pvs_strict_cofactorvaluation_maximal + (bpd_candidate_pvs_strict_cofactorvaluation) = (e))) /\ (((exists pa_b_pvs_strict_cofactorpower pa_c_pvs_strict_cofactorpower. ((forall pa_i_pvs_strict_cofactorpower_repeat. (exists pa_lt_pvs_strict_cofactorpower_repeat_bound. pa_lt_pvs_strict_cofactorpower_repeat_bound + S pa_i_pvs_strict_cofactorpower_repeat = e) -> (((exists pa_h_pvs_strict_cofactorpower_repeat_decoded. pa_h_pvs_strict_cofactorpower_repeat_decoded + S (p) = S ((S (pa_i_pvs_strict_cofactorpower_repeat)) * pa_c_pvs_strict_cofactorpower)) /\ exists pa_q_pvs_strict_cofactorpower_repeat_decoded. pa_b_pvs_strict_cofactorpower = pa_q_pvs_strict_cofactorpower_repeat_decoded * S ((S (pa_i_pvs_strict_cofactorpower_repeat)) * pa_c_pvs_strict_cofactorpower) + (p)))) /\ (exists pa_u_pvs_strict_cofactorpower_product pa_v_pvs_strict_cofactorpower_product. ((((exists pa_h_pvs_strict_cofactorpower_product_start. pa_h_pvs_strict_cofactorpower_product_start + S (1) = S ((S (0)) * pa_v_pvs_strict_cofactorpower_product)) /\ exists pa_q_pvs_strict_cofactorpower_product_start. pa_u_pvs_strict_cofactorpower_product = pa_q_pvs_strict_cofactorpower_product_start * S ((S (0)) * pa_v_pvs_strict_cofactorpower_product) + (1))) /\ ((((exists pa_h_pvs_strict_cofactorpower_product_terminal. pa_h_pvs_strict_cofactorpower_product_terminal + S (P) = S ((S (e)) * pa_v_pvs_strict_cofactorpower_product)) /\ exists pa_q_pvs_strict_cofactorpower_product_terminal. pa_u_pvs_strict_cofactorpower_product = pa_q_pvs_strict_cofactorpower_product_terminal * S ((S (e)) * pa_v_pvs_strict_cofactorpower_product) + (P))) /\ forall pa_i_pvs_strict_cofactorpower_product. (exists pa_lt_pvs_strict_cofactorpower_product_bound. pa_lt_pvs_strict_cofactorpower_product_bound + S pa_i_pvs_strict_cofactorpower_product = e) -> exists pa_p_pvs_strict_cofactorpower_product pa_r_pvs_strict_cofactorpower_product pa_s_pvs_strict_cofactorpower_product. ((((exists pa_h_pvs_strict_cofactorpower_product_factor. pa_h_pvs_strict_cofactorpower_product_factor + S (pa_p_pvs_strict_cofactorpower_product) = S ((S (pa_i_pvs_strict_cofactorpower_product)) * pa_c_pvs_strict_cofactorpower)) /\ exists pa_q_pvs_strict_cofactorpower_product_factor. pa_b_pvs_strict_cofactorpower = pa_q_pvs_strict_cofactorpower_product_factor * S ((S (pa_i_pvs_strict_cofactorpower_product)) * pa_c_pvs_strict_cofactorpower) + (pa_p_pvs_strict_cofactorpower_product))) /\ ((((exists pa_h_pvs_strict_cofactorpower_product_partial. pa_h_pvs_strict_cofactorpower_product_partial + S (pa_r_pvs_strict_cofactorpower_product) = S ((S (pa_i_pvs_strict_cofactorpower_product)) * pa_v_pvs_strict_cofactorpower_product)) /\ exists pa_q_pvs_strict_cofactorpower_product_partial. pa_u_pvs_strict_cofactorpower_product = pa_q_pvs_strict_cofactorpower_product_partial * S ((S (pa_i_pvs_strict_cofactorpower_product)) * pa_v_pvs_strict_cofactorpower_product) + (pa_r_pvs_strict_cofactorpower_product))) /\ ((((exists pa_h_pvs_strict_cofactorpower_product_successor. pa_h_pvs_strict_cofactorpower_product_successor + S (pa_s_pvs_strict_cofactorpower_product) = S ((S (S pa_i_pvs_strict_cofactorpower_product)) * pa_v_pvs_strict_cofactorpower_product)) /\ exists pa_q_pvs_strict_cofactorpower_product_successor. pa_u_pvs_strict_cofactorpower_product = pa_q_pvs_strict_cofactorpower_product_successor * S ((S (S pa_i_pvs_strict_cofactorpower_product)) * pa_v_pvs_strict_cofactorpower_product) + (pa_s_pvs_strict_cofactorpower_product))) /\ pa_s_pvs_strict_cofactorpower_product = pa_r_pvs_strict_cofactorpower_product * pa_p_pvs_strict_cofactorpower_product)))))))) /\ ((((n) = (P) * (u)) /\ (((~(u = 0)) /\ (((~(exists pvs_factor_strict_cofactornondivisor. (u) = (p) * pvs_factor_strict_cofactornondivisor)) /\ (exists pvs_gap_strict_cofactordescent. pvs_gap_strict_cofactordescent + S (u) = (n))))))))))))))))

Complete tactic proof in conservative notation

All 81 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

81 script commands · 30 reading checkpoints · 6 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)
pow positive exponent base divides
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro hn
  3. L3
    intro hunit
02Establish hpL4–8

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

  1. L4
    have hp : ∃ p. Prime(p) ∧ Dvd(p,n)Definitions: Prime(p)Dvd(p,n)Original native command in the exact edition
  2. L5
    specialize prime_divisor_exists (n)
  3. L6
    apply prime_divisor_exists
  4. L7
    exact hn
  5. L8
    exact hunit
03Separate the logical casesL9–10

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

  1. L9
    cases hp
  2. L10
    cases hp_witness
04Establish heL11–14

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

  1. L11
    have he : ∃ e. BoundedPowerValuation(x,n,n,e)Definitions: BoundedPowerValuation(x,n,n,e)Original native command in the exact edition
  2. L12
    specialize power_valuation_exists (x)
  3. L13
    specialize power_valuation_exists (n)
  4. L14
    apply power_valuation_exists
05Separate the logical casesL15–15

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

  1. L15
    cases he
06Establish henzL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime divisor power valuation nonzero.

  1. L16
    have henz : ~(x1 = 0)
  2. L17
    intro hezero
  3. L18
    specialize prime_divisor_power_valuation_nonzero (x)
  4. L19
    specialize prime_divisor_power_valuation_nonzero (n)
  5. L20
    specialize prime_divisor_power_valuation_nonzero (x1)
  6. L21
    apply prime_divisor_power_valuation_nonzero
  7. L22
    exact hp_witness_left
  8. L23
    exact hn
  9. L24
    exact he_witness
  10. L25
    exact hp_witness_right
07Use earlier factsL26–26

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

  1. L26
    exact hezero
08Establish hcL27–34

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

  1. L27
    have hc : ∃ P. ∃ u. Pow(x,x1,P) ∧ (n = P · u ∧ (¬u = 0 ∧ ¬Dvd(x,u)))Definitions: Pow(x,x1,P)Dvd(x,u)Original native command in the exact edition
  2. L28
    specialize power_valuation_exact_cofactor (x)
  3. L29
    specialize power_valuation_exact_cofactor (n)
  4. L30
    specialize power_valuation_exact_cofactor (x1)
  5. L31
    apply power_valuation_exact_cofactor
  6. L32
    exact hp_witness_left
  7. L33
    exact hn
  8. L34
    exact he_witness
09Separate the logical casesL35–39

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

  1. L35
    cases hc
  2. L36
    cases hc_witness
  3. L37
    cases hc_witness_witness
  4. L38
    cases hc_witness_witness_right
  5. L39
    cases hc_witness_witness_right_right
10Establish hpnonunitL40–41

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

  1. L40
    have hpnonunit : ~(x2 = 1)
  2. L41
    intro hPone
11Establish hbaseL42–49

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

  1. L42
  2. L43
    specialize pow_positive_exponent_base_divides (x)
  3. L44
    specialize pow_positive_exponent_base_divides (x1)
  4. L45
    specialize pow_positive_exponent_base_divides (x2)
  5. L46
    apply pow_positive_exponent_base_divides
  6. L47
    exact henz
  7. L48
    exact hc_witness_witness_left
  8. L49
    rewrite hPone at hbase
12Separate the logical casesL50–50

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

  1. L50
    cases hp_witness_left
13Use earlier factsL51–54

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

  1. L51
    apply hp_witness_left_left
  2. L52
    specialize divisor_one (x)
  3. L53
    apply divisor_one
  4. L54
    exact hbase
14Construct an explicit witnessL55–58

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

  1. L55
    exists x
  2. L56
    exists x1
  3. L57
    exists x2
  4. L58
    exists x3
15Separate the logical casesL59–59

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

  1. L59
    split
16Use earlier factsL60–60

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

  1. L60
    exact hp_witness_left
17Separate the logical casesL61–61

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

  1. L61
    split
18Use earlier factsL62–62

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

  1. L62
    exact henz
19Separate the logical casesL63–63

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

  1. L63
    split
20Use earlier factsL64–64

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

  1. L64
    exact he_witness
21Separate the logical casesL65–65

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

  1. L65
    split
22Use earlier factsL66–66

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

  1. L66
    exact hc_witness_witness_left
23Separate the logical casesL67–67

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

  1. L67
    split
24Use earlier factsL68–68

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

  1. L68
    exact hc_witness_witness_right_left
25Separate the logical casesL69–69

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

  1. L69
    split
26Use earlier factsL70–70

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

  1. L70
    exact hc_witness_witness_right_right_left
27Separate the logical casesL71–71

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

  1. L71
    split
28Use earlier factsL72–77

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

  1. L72
    exact hc_witness_witness_right_right_right
  2. L73
    specialize proper_factor_lt (n)
  3. L74
    specialize proper_factor_lt (x3)
  4. L75
    specialize proper_factor_lt (x2)
  5. L76
    apply proper_factor_lt
  6. L77
    exact hn
29Calculate and transport equalitiesL78–78

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

  1. L78
    trans x2 * x3
30Use earlier factsL79–81

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

  1. L79
    exact hc_witness_witness_right_left
  2. L80
    apply mul_comm
  3. L81
    exact hpnonunit

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003intro hunit
  4. 0004have hp : ∃ p. Prime(p) ∧ Dvd(p,n)
  5. 0005specialize prime_divisor_exists (n)
  6. 0006apply prime_divisor_exists
  7. 0007exact hn
  8. 0008exact hunit
  9. 0009cases hp
  10. 0010cases hp_witness
  11. 0011have he : ∃ e. BoundedPowerValuation(x,n,n,e)
  12. 0012specialize power_valuation_exists (x)
  13. 0013specialize power_valuation_exists (n)
  14. 0014apply power_valuation_exists
  15. 0015cases he
  16. 0016have henz : ~(x1 = 0)
  17. 0017intro hezero
  18. 0018specialize prime_divisor_power_valuation_nonzero (x)
  19. 0019specialize prime_divisor_power_valuation_nonzero (n)
  20. 0020specialize prime_divisor_power_valuation_nonzero (x1)
  21. 0021apply prime_divisor_power_valuation_nonzero
  22. 0022exact hp_witness_left
  23. 0023exact hn
  24. 0024exact he_witness
  25. 0025exact hp_witness_right
  26. 0026exact hezero
  27. 0027have hc : ∃ P. ∃ u. Pow(x,x1,P) ∧ (n = P · u ∧ (¬u = 0 ∧ ¬Dvd(x,u)))
  28. 0028specialize power_valuation_exact_cofactor (x)
  29. 0029specialize power_valuation_exact_cofactor (n)
  30. 0030specialize power_valuation_exact_cofactor (x1)
  31. 0031apply power_valuation_exact_cofactor
  32. 0032exact hp_witness_left
  33. 0033exact hn
  34. 0034exact he_witness
  35. 0035cases hc
  36. 0036cases hc_witness
  37. 0037cases hc_witness_witness
  38. 0038cases hc_witness_witness_right
  39. 0039cases hc_witness_witness_right_right
  40. 0040have hpnonunit : ~(x2 = 1)
  41. 0041intro hPone
  42. 0042have hbase : Dvd(x,x2)
  43. 0043specialize pow_positive_exponent_base_divides (x)
  44. 0044specialize pow_positive_exponent_base_divides (x1)
  45. 0045specialize pow_positive_exponent_base_divides (x2)
  46. 0046apply pow_positive_exponent_base_divides
  47. 0047exact henz
  48. 0048exact hc_witness_witness_left
  49. 0049rewrite hPone at hbase
  50. 0050cases hp_witness_left
  51. 0051apply hp_witness_left_left
  52. 0052specialize divisor_one (x)
  53. 0053apply divisor_one
  54. 0054exact hbase
  55. 0055exists x
  56. 0056exists x1
  57. 0057exists x2
  58. 0058exists x3
  59. 0059split
  60. 0060exact hp_witness_left
  61. 0061split
  62. 0062exact henz
  63. 0063split
  64. 0064exact he_witness
  65. 0065split
  66. 0066exact hc_witness_witness_left
  67. 0067split
  68. 0068exact hc_witness_witness_right_left
  69. 0069split
  70. 0070exact hc_witness_witness_right_right_left
  71. 0071split
  72. 0072exact hc_witness_witness_right_right_right
  73. 0073specialize proper_factor_lt (n)
  74. 0074specialize proper_factor_lt (x3)
  75. 0075specialize proper_factor_lt (x2)
  76. 0076apply proper_factor_lt
  77. 0077exact hn
  78. 0078trans x2 * x3
  79. 0079exact hc_witness_witness_right_left
  80. 0080apply mul_comm
  81. 0081exact hpnonunit