PA00A4

prime_inverse_index_exists

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

Every nonzero prime residue index has a bounded inverse index.

Exact expanded PA statement

forall p n i. p = S n -> ((~(p = 1) /\ forall wip_prime_left_exists_prime wip_prime_right_exists_prime. p = wip_prime_left_exists_prime * wip_prime_right_exists_prime -> wip_prime_left_exists_prime = 1 \/ wip_prime_right_exists_prime = 1)) -> (exists wip_strict_gap_exists_index_bound. wip_strict_gap_exists_index_bound + S i = n) -> exists j. (((exists wip_strict_gap_exists_result_left_bound. wip_strict_gap_exists_result_left_bound + S i = n) /\ ((exists wip_strict_gap_exists_result_right_bound. wip_strict_gap_exists_result_right_bound + S j = n) /\ (exists wip_mod_left_exists_result_inverse wip_mod_right_exists_result_inverse. (S i) * S j + p * wip_mod_left_exists_result_inverse = 1 + p * wip_mod_right_exists_result_inverse))))

Structural proof guide

Generated structural guide

Every nonzero prime residue index has a bounded inverse index.

Use the direct prerequisites succ_ne_zero, succ_le_succ, prime_bounded_nonzero_mod_inverse, nonzero_is_succ, le_of_succ_le_succ as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (5), equality transport (4).

Referenced ingredients

PA0005 succ_ne_zero PA002K succ_le_succ PA0063 prime_bounded_nonzero_mod_inverse PA001V nonzero_is_succ PA000V le_of_succ_le_succ

Proof neighborhood

Direct dependencies

PA0005 succ_ne_zero PA002K succ_le_succ PA0063 prime_bounded_nonzero_mod_inverse PA001V nonzero_is_succ PA000V le_of_succ_le_succ

Direct dependents

PA00A5 prime_inverse_prefix_extend

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 n
  3. 0003intro i
  4. 0004intro hpn
  5. 0005intro hp
  6. 0006intro hi
  7. 0007have hsi0 : ~(S i = 0)
  8. 0008specialize succ_ne_zero i
  9. 0009exact succ_ne_zero
  10. 0010have hsip : exists wip_successor_gap_exists_residue_bound. wip_successor_gap_exists_residue_bound + S (S i) = p
  11. 0011rewrite hpn
  12. 0012specialize succ_le_succ (S i)
  13. 0013specialize succ_le_succ n
  14. 0014apply succ_le_succ
  15. 0015exact hi
  16. 0016have hinv : exists wip_inverse_exists_raw. (~(wip_inverse_exists_raw = 0) /\ ((exists wip_strict_gap_exists_raw_bound. wip_strict_gap_exists_raw_bound + S wip_inverse_exists_raw = p) /\ (exists wip_mod_left_exists_raw_congruence wip_mod_right_exists_raw_congruence. (S i) * wip_inverse_exists_raw + p * wip_mod_left_exists_raw_congruence = 1 + p * wip_mod_right_exists_raw_congruence)))
  17. 0017specialize prime_bounded_nonzero_mod_inverse p
  18. 0018specialize prime_bounded_nonzero_mod_inverse (S i)
  19. 0019apply prime_bounded_nonzero_mod_inverse
  20. 0020exact hp
  21. 0021exact hsi0
  22. 0022exact hsip
  23. 0023cases hinv
  24. 0024cases hinv_witness
  25. 0025cases hinv_witness_right
  26. 0026have hpred : exists j. x = S j
  27. 0027specialize nonzero_is_succ x
  28. 0028apply nonzero_is_succ
  29. 0029exact hinv_witness_left
  30. 0030cases hpred
  31. 0031have hjn : exists wip_strict_gap_exists_output_bound. wip_strict_gap_exists_output_bound + S x1 = n
  32. 0032specialize le_of_succ_le_succ (S x1)
  33. 0033specialize le_of_succ_le_succ n
  34. 0034apply le_of_succ_le_succ
  35. 0035rewrite <- hpred_witness
  36. 0036rewrite <- hpn
  37. 0037exact hinv_witness_right_left
  38. 0038exists x1
  39. 0039split
  40. 0040exact hi
  41. 0041split
  42. 0042exact hjn
  43. 0043rewrite hpred_witness at hinv_witness_right_right
  44. 0044exact hinv_witness_right_right