PA008P

prime_scaled_inverse_target_nonzero

Alpha v34 checked-use theorem · independently closed; not Stable

A scaled inverse of a nonzero bounded target cannot be 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.

Exact expanded PA statement

forall p a x y. ((~(p = 1) /\ forall esi_prime_left_target_nonzero_prime esi_prime_right_target_nonzero_prime. p = esi_prime_left_target_nonzero_prime * esi_prime_right_target_nonzero_prime -> esi_prime_left_target_nonzero_prime = 1 \/ esi_prime_right_target_nonzero_prime = 1)) -> ~(a = 0) -> (exists esi_strict_gap_target_nonzero_target_bound. esi_strict_gap_target_nonzero_target_bound + S a = p) -> (exists esi_mod_left_target_nonzero_product esi_mod_right_target_nonzero_product. (x * y) + p * esi_mod_left_target_nonzero_product = (a) + p * esi_mod_right_target_nonzero_product) -> ~(y = 0)

Structural proof guide

Generated structural guide

A scaled inverse of a nonzero bounded target cannot be zero.

Use the direct prerequisites prime_is_succ_succ, mod_eq_bounded_unique as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (4), equality transport (1), certified simplification (1).

Referenced ingredients

PA0061 prime_is_succ_succ PA002U mod_eq_bounded_unique

Proof neighborhood

Direct dependencies

PA0061 prime_is_succ_succ PA002U mod_eq_bounded_unique

Direct dependents

PA008Q prime_scaled_inverse_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

44 script commands · 15 reading checkpoints · 4 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.

Named ingredients (2)
prime is succ succmod eq bounded unique
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro hp
  6. L6
    intro ha0
  7. L7
    intro hap
  8. L8
    intro hxy
  9. L9
    intro hy0
02Establish hp2L10–13

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

  1. L10
    have hp2 : exists k. p = S (S k)
  2. L11
    specialize prime_is_succ_succ p
  3. L12
    apply prime_is_succ_succ
  4. L13
    exact hp
03Separate the logical casesL14–14

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

  1. L14
    cases hp2
04Establish h0pL15–15

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

  1. L15
    have h0p : exists h. h + S 0 = p
05Construct an explicit witnessL16–16

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

  1. L16
    exists S x1
06Calculate and transport equalitiesL17–18

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

  1. L17
    rewrite hp2_witness
  2. L18
    simp
07Establish hzeroaL19–19

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

  1. L19
    have hzeroa : exists esi_mod_left_target_nonzero_zero esi_mod_right_target_nonzero_zero. (0) + p * esi_mod_left_target_nonzero_zero = (a) + p * esi_mod_right_target_nonzero_zero
08Separate the logical casesL20–21

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

  1. L20
    cases hxy
  2. L21
    cases hxy_witness
09Construct an explicit witnessL22–23

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

  1. L22
    exists x2
  2. L23
    exists x3
10Calculate and transport equalitiesL24–29

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

  1. L24
    trans (x * y) + p * x2
  2. L25
    congr
  3. L26
    symm
  4. L27
    trans x * 0
  5. L28
    congr
  6. L29
    refl
11Use earlier factsL30–31

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

  1. L30
    exact hy0
  2. L31
    apply PA5
12Calculate and transport equalitiesL32–32

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

  1. L32
    refl
13Use earlier factsL33–33

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

  1. L33
    exact hxy_witness_witness
14Establish h0aL34–43

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

  1. L34
    have h0a : 0 = a
  2. L35
    specialize mod_eq_bounded_unique p
  3. L36
    specialize mod_eq_bounded_unique 0
  4. L37
    specialize mod_eq_bounded_unique a
  5. L38
    apply mod_eq_bounded_unique
  6. L39
    exact h0p
  7. L40
    exact hap
  8. L41
    exact hzeroa
  9. L42
    apply ha0
  10. L43
    symm
15Use earlier factsL44–44

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

  1. L44
    exact h0a

Library-wide reading audit

Original exact command ledger · 44 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro hp
  6. 0006intro ha0
  7. 0007intro hap
  8. 0008intro hxy
  9. 0009intro hy0
  10. 0010have hp2 : exists k. p = S (S k)
  11. 0011specialize prime_is_succ_succ p
  12. 0012apply prime_is_succ_succ
  13. 0013exact hp
  14. 0014cases hp2
  15. 0015have h0p : exists h. h + S 0 = p
  16. 0016exists S x1
  17. 0017rewrite hp2_witness
  18. 0018simp
  19. 0019have hzeroa : exists esi_mod_left_target_nonzero_zero esi_mod_right_target_nonzero_zero. (0) + p * esi_mod_left_target_nonzero_zero = (a) + p * esi_mod_right_target_nonzero_zero
  20. 0020cases hxy
  21. 0021cases hxy_witness
  22. 0022exists x2
  23. 0023exists x3
  24. 0024trans (x * y) + p * x2
  25. 0025congr
  26. 0026symm
  27. 0027trans x * 0
  28. 0028congr
  29. 0029refl
  30. 0030exact hy0
  31. 0031apply PA5
  32. 0032refl
  33. 0033exact hxy_witness_witness
  34. 0034have h0a : 0 = a
  35. 0035specialize mod_eq_bounded_unique p
  36. 0036specialize mod_eq_bounded_unique 0
  37. 0037specialize mod_eq_bounded_unique a
  38. 0038apply mod_eq_bounded_unique
  39. 0039exact h0p
  40. 0040exact hap
  41. 0041exact hzeroa
  42. 0042apply ha0
  43. 0043symm
  44. 0044exact h0a