BT0055 · Bertrand theorem

le_scaled_nonzero

Stable checked-use theorem · independently kernel verified

Scaling by a nonzero natural does not decrease a natural.

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

∀ C. ∀ B. ¬C = 0 → Le(B,C · B)

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

PD0001 Le

1 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

2 occurrences

Exact expanded native-PA statement
forall C B. ~(C = 0) -> exists h. h + B = C * B

Proof neighborhood

Direct theorem prerequisites

BT0010 one_le_of_ne_zero BT001M mul_le_mul_right BT0009 one_mul

Direct theorem dependents

BT0057 beta_value_lt_scaled_base BT0058 new_value_lt_scaled_base

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

16 script commands · 3 reading checkpoints · 2 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 (3)
one le of ne zeromul le mul rightone mul
01Fix variables and assumptionsL1–3

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

  1. L1
    intro C
  2. L2
    intro B
  3. L3
    intro hC
02Establish h1CL4–7

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L4
  2. L5
    specialize one_le_of_ne_zero C
  3. L6
    apply one_le_of_ne_zero
  4. L7
    exact hC
03Establish hscaledL8–16

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

  1. L8
    have hscaled : Le(1 · B,C · B)Definitions: Le(1 · B,C · B)Original native command in the exact edition
  2. L9
    specialize mul_le_mul_right 1
  3. L10
    specialize mul_le_mul_right C
  4. L11
    specialize mul_le_mul_right B
  5. L12
    apply mul_le_mul_right
  6. L13
    exact h1C
  7. L14
    specialize one_mul B
  8. L15
    rewrite one_mul at hscaled
  9. L16
    exact hscaled

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro C
  2. 0002intro B
  3. 0003intro hC
  4. 0004have h1C : Lt(0,C)
    Exact native replay linehave h1C : exists h. h + 1 = C
  5. 0005specialize one_le_of_ne_zero C
  6. 0006apply one_le_of_ne_zero
  7. 0007exact hC
  8. 0008have hscaled : Le(1 · B,C · B)
    Exact native replay linehave hscaled : exists h. h + 1 * B = C * B
  9. 0009specialize mul_le_mul_right 1
  10. 0010specialize mul_le_mul_right C
  11. 0011specialize mul_le_mul_right B
  12. 0012apply mul_le_mul_right
  13. 0013exact h1C
  14. 0014specialize one_mul B
  15. 0015rewrite one_mul at hscaled
  16. 0016exact hscaled