PA00BP

odd_prime_one_not_mod_predecessor

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

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

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

Read the argument

Proof checkpoints

36 script commands · 16 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 (4)
double predecessor ne oneprime is succ succmod eq bounded uniquezero add
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro h
  4. L4
    intro hpn
  5. L5
    intro hp
  6. L6
    intro heven
  7. L7
    intro hone_mod
02Establish hp_shapeL8–11

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

  1. L8
    have hp_shape : exists k. p = S (S k)
  2. L9
    specialize prime_is_succ_succ p
  3. L10
    apply prime_is_succ_succ
  4. L11
    exact hp
03Separate the logical casesL12–12

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

  1. L12
    cases hp_shape
04Establish h1pL13–13

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

  1. L13
    have h1p : exists gap. gap + S 1 = p
05Construct an explicit witnessL14–14

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

  1. L14
    exists x
06Calculate and transport equalitiesL15–16

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

  1. L15
    rewrite hp_shape_witness
  2. L16
    simp
07Establish hnpL17–17

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

  1. L17
    have hnp : exists gap. gap + S n = p
08Construct an explicit witnessL18–18

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

  1. L18
    exists 0
09Calculate and transport equalitiesL19–19

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

  1. L19
    trans S n
10Use earlier factsL20–20

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

  1. L20
    apply zero_add
11Calculate and transport equalitiesL21–21

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

  1. L21
    symm
12Use earlier factsL22–22

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

  1. L22
    exact hpn
13Establish h1nL23–32

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

  1. L23
    have h1n : 1 = n
  2. L24
    specialize mod_eq_bounded_unique p
  3. L25
    specialize mod_eq_bounded_unique 1
  4. L26
    specialize mod_eq_bounded_unique n
  5. L27
    apply mod_eq_bounded_unique
  6. L28
    exact h1p
  7. L29
    exact hnp
  8. L30
    exact hone_mod
  9. L31
    specialize double_predecessor_ne_one n
  10. L32
    specialize double_predecessor_ne_one h
14Use earlier factsL33–34

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

  1. L33
    apply double_predecessor_ne_one
  2. L34
    exact heven
15Calculate and transport equalitiesL35–35

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

  1. L35
    symm
16Use earlier factsL36–36

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

  1. L36
    exact h1n

Library-wide reading audit

Original exact command ledger · 36 lines
  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