PA008P

prime_scaled_inverse_target_nonzero

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

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

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-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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