PA00BP

odd_prime_one_not_mod_predecessor

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

For an odd-prime predecessor, the canonical residues one and p-1 are distinct.

Exact expanded PA statement

forall p n h. p = S n -> ((~(p = 1) /\ forall esi_prime_left_ecb_prime esi_prime_right_ecb_prime. p = esi_prime_left_ecb_prime * esi_prime_right_ecb_prime -> esi_prime_left_ecb_prime = 1 \/ esi_prime_right_ecb_prime = 1)) -> n = h + h -> ~(exists wpp_mod_left_ecb_one_mod_predecessor wpp_mod_right_ecb_one_mod_predecessor. (1) + p * wpp_mod_left_ecb_one_mod_predecessor = (n) + p * wpp_mod_right_ecb_one_mod_predecessor)

Structural proof guide

Generated structural guide

For an odd-prime predecessor, the canonical residues one and p-1 are distinct.

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

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

Referenced ingredients

PA00BO double_predecessor_ne_one PA0061 prime_is_succ_succ PA002U mod_eq_bounded_unique PA0001 zero_add

Proof neighborhood

Direct dependencies

PA00BO double_predecessor_ne_one PA0061 prime_is_succ_succ PA002U mod_eq_bounded_unique PA0001 zero_add

Direct dependents

PA00BQ bounded_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff PA00BV arbitrary_gauss_lemma_complete

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 h
  4. 0004intro hpn
  5. 0005intro hp
  6. 0006intro heven
  7. 0007intro hone_mod
  8. 0008have hp_shape : exists k. p = S (S k)
  9. 0009specialize prime_is_succ_succ p
  10. 0010apply prime_is_succ_succ
  11. 0011exact hp
  12. 0012cases hp_shape
  13. 0013have h1p : exists gap. gap + S 1 = p
  14. 0014exists x
  15. 0015rewrite hp_shape_witness
  16. 0016simp
  17. 0017have hnp : exists gap. gap + S n = p
  18. 0018exists 0
  19. 0019trans S n
  20. 0020apply zero_add
  21. 0021symm
  22. 0022exact hpn
  23. 0023have h1n : 1 = n
  24. 0024specialize mod_eq_bounded_unique p
  25. 0025specialize mod_eq_bounded_unique 1
  26. 0026specialize mod_eq_bounded_unique n
  27. 0027apply mod_eq_bounded_unique
  28. 0028exact h1p
  29. 0029exact hnp
  30. 0030exact hone_mod
  31. 0031specialize double_predecessor_ne_one n
  32. 0032specialize double_predecessor_ne_one h
  33. 0033apply double_predecessor_ne_one
  34. 0034exact heven
  35. 0035symm
  36. 0036exact h1n