BT00TY · Bertrand theorem

mul_lt_mul_right_nonzero

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Right multiplication by a nonzero natural preserves strict order.

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.

Statement with defined notation

∀ a. ∀ b. ∀ c. Lt(a,b) → ¬c = 0 → Lt(a · c,b · c)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt

2 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

3 occurrences

Exact expanded native-PA statement
forall a b c. (exists bcf_lt_gap_mlmrn_source. bcf_lt_gap_mlmrn_source + S (a) = b) -> ~(c = 0) -> (exists bcf_lt_gap_mlmrn_result. bcf_lt_gap_mlmrn_result + S (a * c) = b * c)

Proof neighborhood

Direct theorem prerequisites

BT0006 mul_comm BT001N mul_lt_mul_succ_left_nonzero BT001M mul_le_mul_right BT001D lt_of_lt_of_le

Direct theorem dependents

BT00U0 four_power_central_recurrence_step BT00U3 four_pow_central_seed_package

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

34 script commands · 7 reading checkpoints · 5 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (4)
mul commmul lt mul succ left nonzeromul le mul rightlt of lt of le
01Fix variables and assumptionsL1–5

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro hab
  5. L5
    intro hc
02Establish hrawL6–10

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

  1. L6
    have hraw : Lt(c · a,c · S a)Definitions: Lt(c · a,c · S a)Original native command in the exact edition
  2. L7
    specialize mul_lt_mul_succ_left_nonzero c
  3. L8
    specialize mul_lt_mul_succ_left_nonzero a
  4. L9
    apply mul_lt_mul_succ_left_nonzero
  5. L10
    exact hc
03Establish hleft_commL11–14

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

  1. L11
    have hleft_comm : c * a = a * c
  2. L12
    specialize mul_comm c
  3. L13
    specialize mul_comm a
  4. L14
    exact mul_comm
04Establish hright_commL15–20

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

  1. L15
    have hright_comm : c * S a = S a * c
  2. L16
    specialize mul_comm c
  3. L17
    specialize mul_comm (S a)
  4. L18
    exact mul_comm
  5. L19
    rewrite hleft_comm at hraw
  6. L20
    rewrite hright_comm at hraw
05Establish hstepL21–22

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

  1. L21
    have hstep : Lt(a · c,S a · c)Definitions: Lt(a · c,S a · c)Original native command in the exact edition
  2. L22
    exact hraw
06Establish htailL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul right.

  1. L23
    have htail : Le(S a · c,b · c)Definitions: Le(S a · c,b · c)Original native command in the exact edition
  2. L24
    specialize mul_le_mul_right (S a)
  3. L25
    specialize mul_le_mul_right b
  4. L26
    specialize mul_le_mul_right c
  5. L27
    apply mul_le_mul_right
  6. L28
    exact hab
  7. L29
    specialize lt_of_lt_of_le (a * c)
  8. L30
    specialize lt_of_lt_of_le (S a * c)
  9. L31
    specialize lt_of_lt_of_le (b * c)
  10. L32
    apply lt_of_lt_of_le
07Use earlier factsL33–34

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

  1. L33
    exact hstep
  2. L34
    exact htail

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hab
  5. 0005intro hc
  6. 0006have hraw : Lt(c · a,c · S a)
    Exact native replay linehave hraw : exists bcf_lt_gap_mlmrn_raw_step. bcf_lt_gap_mlmrn_raw_step + S (c * a) = c * S a
  7. 0007specialize mul_lt_mul_succ_left_nonzero c
  8. 0008specialize mul_lt_mul_succ_left_nonzero a
  9. 0009apply mul_lt_mul_succ_left_nonzero
  10. 0010exact hc
  11. 0011have hleft_comm : c * a = a * c
  12. 0012specialize mul_comm c
  13. 0013specialize mul_comm a
  14. 0014exact mul_comm
  15. 0015have hright_comm : c * S a = S a * c
  16. 0016specialize mul_comm c
  17. 0017specialize mul_comm (S a)
  18. 0018exact mul_comm
  19. 0019rewrite hleft_comm at hraw
  20. 0020rewrite hright_comm at hraw
  21. 0021have hstep : Lt(a · c,S a · c)
    Exact native replay linehave hstep : exists bcf_lt_gap_mlmrn_step. bcf_lt_gap_mlmrn_step + S (a * c) = S a * c
  22. 0022exact hraw
  23. 0023have htail : Le(S a · c,b · c)
    Exact native replay linehave htail : exists bcf_le_gap_mlmrn_tail. bcf_le_gap_mlmrn_tail + (S a * c) = b * c
  24. 0024specialize mul_le_mul_right (S a)
  25. 0025specialize mul_le_mul_right b
  26. 0026specialize mul_le_mul_right c
  27. 0027apply mul_le_mul_right
  28. 0028exact hab
  29. 0029specialize lt_of_lt_of_le (a * c)
  30. 0030specialize lt_of_lt_of_le (S a * c)
  31. 0031specialize lt_of_lt_of_le (b * c)
  32. 0032apply lt_of_lt_of_le
  33. 0033exact hstep
  34. 0034exact htail