JT005E

jordan_prime_power_tuple_primitive_of_not_all_divisible

Every nonunit common divisor has an actual prime divisor; prime-power support then forces a forbidden common factor p.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ e. ∀ n. ∀ b. ∀ c. ∀ k. Prime(p) → Pow(p,e,n) → ¬JordanTupleAllDivisible(p,b,c,k) → JordanPrimitiveTuple(n,b,c,k)

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

Definition DAG

JordanTupleAllDivisible(d,b,c,k) · 1JordanPrimitiveTuple(n,b,c,k) · 1Dvd(d,n) · 2Prime(p) · 2Pow(a,e,z) · 1

Actual proof prerequisites

pow_nonzero_of_one_le · checked external prerequisiteone_le_of_ne_zero · checked external prerequisiteprime_nonzero · checked external prerequisiteeq_decidable · checked external prerequisitemul_zero_left · checked external prerequisiteprime_divisor_exists · checked external prerequisitemultiple_trans · checked external prerequisiteprime_divisor_of_prime_power · checked external prerequisitejordan_tuple_divisor_downward
Original expanded first-order statement 
forall p e n b c k. (~((p) = 1) /\ forall pvs_left_jordan_base pvs_right_jordan_base. (p) = pvs_left_jordan_base * pvs_right_jordan_base -> pvs_left_jordan_base = 1 \/ pvs_right_jordan_base = 1) -> (exists pa_b_pvs_jordan_power pa_c_pvs_jordan_power. ((forall pa_i_pvs_jordan_power_repeat. (exists pa_lt_pvs_jordan_power_repeat_bound. pa_lt_pvs_jordan_power_repeat_bound + S pa_i_pvs_jordan_power_repeat = e) -> (((exists pa_h_pvs_jordan_power_repeat_decoded. pa_h_pvs_jordan_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_jordan_power_repeat)) * pa_c_pvs_jordan_power)) /\ exists pa_q_pvs_jordan_power_repeat_decoded. pa_b_pvs_jordan_power = pa_q_pvs_jordan_power_repeat_decoded * S ((S (pa_i_pvs_jordan_power_repeat)) * pa_c_pvs_jordan_power) + (p)))) /\ (exists pa_u_pvs_jordan_power_product pa_v_pvs_jordan_power_product. ((((exists pa_h_pvs_jordan_power_product_start. pa_h_pvs_jordan_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_jordan_power_product)) /\ exists pa_q_pvs_jordan_power_product_start. pa_u_pvs_jordan_power_product = pa_q_pvs_jordan_power_product_start * S ((S (0)) * pa_v_pvs_jordan_power_product) + (1))) /\ ((((exists pa_h_pvs_jordan_power_product_terminal. pa_h_pvs_jordan_power_product_terminal + S (n) = S ((S (e)) * pa_v_pvs_jordan_power_product)) /\ exists pa_q_pvs_jordan_power_product_terminal. pa_u_pvs_jordan_power_product = pa_q_pvs_jordan_power_product_terminal * S ((S (e)) * pa_v_pvs_jordan_power_product) + (n))) /\ forall pa_i_pvs_jordan_power_product. (exists pa_lt_pvs_jordan_power_product_bound. pa_lt_pvs_jordan_power_product_bound + S pa_i_pvs_jordan_power_product = e) -> exists pa_p_pvs_jordan_power_product pa_r_pvs_jordan_power_product pa_s_pvs_jordan_power_product. ((((exists pa_h_pvs_jordan_power_product_factor. pa_h_pvs_jordan_power_product_factor + S (pa_p_pvs_jordan_power_product) = S ((S (pa_i_pvs_jordan_power_product)) * pa_c_pvs_jordan_power)) /\ exists pa_q_pvs_jordan_power_product_factor. pa_b_pvs_jordan_power = pa_q_pvs_jordan_power_product_factor * S ((S (pa_i_pvs_jordan_power_product)) * pa_c_pvs_jordan_power) + (pa_p_pvs_jordan_power_product))) /\ ((((exists pa_h_pvs_jordan_power_product_partial. pa_h_pvs_jordan_power_product_partial + S (pa_r_pvs_jordan_power_product) = S ((S (pa_i_pvs_jordan_power_product)) * pa_v_pvs_jordan_power_product)) /\ exists pa_q_pvs_jordan_power_product_partial. pa_u_pvs_jordan_power_product = pa_q_pvs_jordan_power_product_partial * S ((S (pa_i_pvs_jordan_power_product)) * pa_v_pvs_jordan_power_product) + (pa_r_pvs_jordan_power_product))) /\ ((((exists pa_h_pvs_jordan_power_product_successor. pa_h_pvs_jordan_power_product_successor + S (pa_s_pvs_jordan_power_product) = S ((S (S pa_i_pvs_jordan_power_product)) * pa_v_pvs_jordan_power_product)) /\ exists pa_q_pvs_jordan_power_product_successor. pa_u_pvs_jordan_power_product = pa_q_pvs_jordan_power_product_successor * S ((S (S pa_i_pvs_jordan_power_product)) * pa_v_pvs_jordan_power_product) + (pa_s_pvs_jordan_power_product))) /\ pa_s_pvs_jordan_power_product = pa_r_pvs_jordan_power_product * pa_p_pvs_jordan_power_product)))))))) -> (~(forall jt_index_power_all_divisible jt_value_power_all_divisible. (exists jt_gap_power_all_divisibleindex. jt_gap_power_all_divisibleindex+S (jt_index_power_all_divisible)=(k)) -> (((exists fs_h_jt_power_all_divisibleat. fs_h_jt_power_all_divisibleat + S (jt_value_power_all_divisible) = S ((S (jt_index_power_all_divisible)) * c)) /\ exists fs_q_jt_power_all_divisibleat. b = fs_q_jt_power_all_divisibleat * S ((S (jt_index_power_all_divisible)) * c) + (jt_value_power_all_divisible))) -> (exists jt_factor_power_all_divisibledivides. (jt_value_power_all_divisible)=(p)*jt_factor_power_all_divisibledivides))) -> forall jt_divisor_power_primitive. (exists jt_factor_power_primitivemodulus. (n)=(jt_divisor_power_primitive)*jt_factor_power_primitivemodulus) -> (forall jt_index_power_primitivecoordinates jt_value_power_primitivecoordinates. (exists jt_gap_power_primitivecoordinatesindex. jt_gap_power_primitivecoordinatesindex+S (jt_index_power_primitivecoordinates)=(k)) -> (((exists fs_h_jt_power_primitivecoordinatesat. fs_h_jt_power_primitivecoordinatesat + S (jt_value_power_primitivecoordinates) = S ((S (jt_index_power_primitivecoordinates)) * c)) /\ exists fs_q_jt_power_primitivecoordinatesat. b = fs_q_jt_power_primitivecoordinatesat * S ((S (jt_index_power_primitivecoordinates)) * c) + (jt_value_power_primitivecoordinates))) -> (exists jt_factor_power_primitivecoordinatesdivides. (jt_value_power_primitivecoordinates)=(jt_divisor_power_primitive)*jt_factor_power_primitivecoordinatesdivides)) -> jt_divisor_power_primitive=1

Complete tactic proof in conservative notation

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

75 script commands · 21 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 (1)
jordan tuple divisor downward
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro e
  3. L3
    intro n
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro k
  7. L7
    intro hp
  8. L8
    intro hpow
  9. L9
    intro hnot
02Establish hnL10–19

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

  1. L10
    have hn : ~(n=0)
  2. L11
    intro hz
  3. L12
    specialize pow_nonzero_of_one_le (p)
  4. L13
    specialize pow_nonzero_of_one_le (e)
  5. L14
    specialize pow_nonzero_of_one_le (n)
  6. L15
    apply pow_nonzero_of_one_le
  7. L16
    specialize one_le_of_ne_zero (p)
  8. L17
    apply one_le_of_ne_zero
  9. L18
    intro hpzero
  10. L19
    specialize prime_nonzero (p)
03Use earlier factsL20–24

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

  1. L20
    apply prime_nonzero
  2. L21
    exact hp
  3. L22
    exact hpzero
  4. L23
    exact hpow
  5. L24
    exact hz
04Fix variables and assumptionsL25–27

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

  1. L25
    intro d
  2. L26
    intro hd
  3. L27
    intro hall
05Use earlier factsL28–29

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

  1. L28
    specialize eq_decidable d
  2. L29
    specialize eq_decidable 1
06Separate the logical casesL30–30

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

  1. L30
    cases eq_decidable
07Use earlier factsL31–31

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

  1. L31
    exact eq_decidable_left
08Separate the logical casesL32–32

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

  1. L32
    exfalso
09Use earlier factsL33–33

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

  1. L33
    apply hnot
10Establish hdnonzeroL34–36

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

  1. L34
    have hdnonzero : ~(d=0)
  2. L35
    intro hz
  3. L36
    apply hn
11Separate the logical casesL37–37

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

  1. L37
    cases hd
12Calculate and transport equalitiesL38–38

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

  1. L38
    trans d*x
13Use earlier factsL39–39

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

  1. L39
    exact hd_witness
14Calculate and transport equalitiesL40–40

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

  1. L40
    rewrite hz
15Use earlier factsL41–42

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

  1. L41
    specialize mul_zero_left (x)
  2. L42
    apply mul_zero_left
16Establish hprimeL43–47

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

  1. L43
    have hprime : ∃ q. Prime(q) ∧ Dvd(q,d)Definitions: Prime(q)Dvd(q,d)Original native command in the exact edition
  2. L44
    specialize prime_divisor_exists (d)
  3. L45
    apply prime_divisor_exists
  4. L46
    exact hdnonzero
  5. L47
    exact eq_decidable_right
17Separate the logical casesL48–49

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

  1. L48
    cases hprime
  2. L49
    cases hprime_witness
18Establish hqnL50–56

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

  1. L50
  2. L51
    specialize multiple_trans (d)
  3. L52
    specialize multiple_trans (x)
  4. L53
    specialize multiple_trans (n)
  5. L54
    apply multiple_trans
  6. L55
    exact hd
  7. L56
    exact hprime_witness_right
19Establish hqpL57–66

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

  1. L57
    have hqp : x=p
  2. L58
    specialize prime_divisor_of_prime_power (p)
  3. L59
    specialize prime_divisor_of_prime_power (x)
  4. L60
    specialize prime_divisor_of_prime_power (e)
  5. L61
    specialize prime_divisor_of_prime_power (n)
  6. L62
    apply prime_divisor_of_prime_power
  7. L63
    exact hp
  8. L64
    exact hprime_witness_left
  9. L65
    exact hpow
  10. L66
    exact hqn
20Calculate and transport equalitiesL67–67

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

  1. L67
    rewrite <- hqp
21Use earlier factsL68–75

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

  1. L68
    specialize jordan_tuple_divisor_downward (x)
  2. L69
    specialize jordan_tuple_divisor_downward (d)
  3. L70
    specialize jordan_tuple_divisor_downward (b)
  4. L71
    specialize jordan_tuple_divisor_downward (c)
  5. L72
    specialize jordan_tuple_divisor_downward (k)
  6. L73
    apply jordan_tuple_divisor_downward
  7. L74
    exact hprime_witness_right
  8. L75
    exact hall

Library-wide reading audit

Original defined command ledger · 75 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro k
  7. 0007intro hp
  8. 0008intro hpow
  9. 0009intro hnot
  10. 0010have hn : ~(n=0)
  11. 0011intro hz
  12. 0012specialize pow_nonzero_of_one_le (p)
  13. 0013specialize pow_nonzero_of_one_le (e)
  14. 0014specialize pow_nonzero_of_one_le (n)
  15. 0015apply pow_nonzero_of_one_le
  16. 0016specialize one_le_of_ne_zero (p)
  17. 0017apply one_le_of_ne_zero
  18. 0018intro hpzero
  19. 0019specialize prime_nonzero (p)
  20. 0020apply prime_nonzero
  21. 0021exact hp
  22. 0022exact hpzero
  23. 0023exact hpow
  24. 0024exact hz
  25. 0025intro d
  26. 0026intro hd
  27. 0027intro hall
  28. 0028specialize eq_decidable d
  29. 0029specialize eq_decidable 1
  30. 0030cases eq_decidable
  31. 0031exact eq_decidable_left
  32. 0032exfalso
  33. 0033apply hnot
  34. 0034have hdnonzero : ~(d=0)
  35. 0035intro hz
  36. 0036apply hn
  37. 0037cases hd
  38. 0038trans d*x
  39. 0039exact hd_witness
  40. 0040rewrite hz
  41. 0041specialize mul_zero_left (x)
  42. 0042apply mul_zero_left
  43. 0043have hprime : ∃ q. Prime(q) ∧ Dvd(q,d)
  44. 0044specialize prime_divisor_exists (d)
  45. 0045apply prime_divisor_exists
  46. 0046exact hdnonzero
  47. 0047exact eq_decidable_right
  48. 0048cases hprime
  49. 0049cases hprime_witness
  50. 0050have hqn : Dvd(x,n)
  51. 0051specialize multiple_trans (d)
  52. 0052specialize multiple_trans (x)
  53. 0053specialize multiple_trans (n)
  54. 0054apply multiple_trans
  55. 0055exact hd
  56. 0056exact hprime_witness_right
  57. 0057have hqp : x=p
  58. 0058specialize prime_divisor_of_prime_power (p)
  59. 0059specialize prime_divisor_of_prime_power (x)
  60. 0060specialize prime_divisor_of_prime_power (e)
  61. 0061specialize prime_divisor_of_prime_power (n)
  62. 0062apply prime_divisor_of_prime_power
  63. 0063exact hp
  64. 0064exact hprime_witness_left
  65. 0065exact hpow
  66. 0066exact hqn
  67. 0067rewrite <- hqp
  68. 0068specialize jordan_tuple_divisor_downward (x)
  69. 0069specialize jordan_tuple_divisor_downward (d)
  70. 0070specialize jordan_tuple_divisor_downward (b)
  71. 0071specialize jordan_tuple_divisor_downward (c)
  72. 0072specialize jordan_tuple_divisor_downward (k)
  73. 0073apply jordan_tuple_divisor_downward
  74. 0074exact hprime_witness_right
  75. 0075exact hall