PA002N · theorem

le_scaled_nonzero

Stable checked-use theorem · independently closed

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. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

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

PA002L one_le_of_ne_zero PA002M mul_le_mul_right PA000M one_mul

Direct theorem dependents

PA002Q new_value_lt_scaled_base PA002T beta_value_lt_scaled_base

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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