BT002U · Bertrand theorem

gcd_exists_up_to

Stable checked-use theorem · independently kernel verified

Bounded induction constructs a relational gcd whenever the right input is at most the bound.

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

∀ B. ∀ b. Le(b,B) → ∀ x. ∃ y. IsGCD(y,x,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 PD0006 IsGCD

2 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0006 IsGCD PD0007 DivRem

7 occurrences

Exact expanded native-PA statement
forall B b. (exists t. t + b = B) -> forall a. exists d. (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

Proof neighborhood

Direct theorem prerequisites

BT0028 multiple_refl BT000Y le_zero BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT001P division_remainder_exists BT002S is_gcd_euclid_forward

Direct theorem dependents

BT002V gcd_exists_relational

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

74 script commands · 28 reading checkpoints · 9 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 (6)
multiple reflle zerole eq or ltle of succ le succdivision remainder existsis gcd euclid forward
01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
  2. L3
    intro b
  3. L4
    intro hb
  4. L5
    intro a
03Establish hb0L6–8

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

  1. L6
    have hb0 : b = 0
  2. L7
    apply le_zero
  3. L8
    exact hb
04Construct an explicit witnessL9–9

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

  1. L9
    exists a
05Separate the logical casesL10–11

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

  1. L10
    split
  2. L11
    split
06Use earlier factsL12–13

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

  1. L12
    specialize multiple_refl a
  2. L13
    exact multiple_refl
07Construct an explicit witnessL14–14

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

  1. L14
    exists 0
08Calculate and transport equalitiesL15–15

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

  1. L15
    trans 0
09Use earlier factsL16–16

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

  1. L16
    exact hb0
10Calculate and transport equalitiesL17–17

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

  1. L17
    symm
11Use earlier factsL18–18

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

  1. L18
    apply PA5
12Fix variables and assumptionsL19–21

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

  1. L19
    intro c
  2. L20
    intro hca
  3. L21
    intro hcb
13Use earlier factsL22–22

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

  1. L22
    exact hca
14Fix variables and assumptionsL23–25

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

  1. L23
    intro b
  2. L24
    intro hb
  3. L25
    intro a
15Use earlier factsL26–27

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

  1. L26
    specialize le_eq_or_lt b
  2. L27
    specialize le_eq_or_lt (S B)
16Establish hsplitL28–30

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

  1. L28
    have hsplit : b = S B ∨ Lt(b,S B)Definitions: Lt(b,S B)Original native command in the exact edition
  2. L29
    apply le_eq_or_lt
  3. L30
    exact hb
17Separate the logical casesL31–31

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

  1. L31
    cases hsplit
18Establish hb0L32–38

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

  1. L32
    have hb0 : ~(b = 0)
  2. L33
    intro hzero
  3. L34
    apply PA1
  4. L35
    trans b
  5. L36
    symm
  6. L37
    exact hsplit_left
  7. L38
    exact hzero
19Establish hdivL39–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.

  1. L39
    have hdiv : ∃ q. ∃ r. DivRem(a,b,q,r)Definitions: DivRem(a,b,q,r)Original native command in the exact edition
  2. L40
    apply division_remainder_exists
  3. L41
    exact hb0
20Separate the logical casesL42–44

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

  1. L42
    cases hdiv
  2. L43
    cases hdiv_witness
  3. L44
    cases hdiv_witness_witness
21Establish hrBL45–48

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

  1. L45
  2. L46
    apply le_of_succ_le_succ
  3. L47
    rewrite hsplit_left at hdiv_witness_witness_right
  4. L48
    exact hdiv_witness_witness_right
22Establish hsmallL49–50

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

  1. L49
    have hsmall : ∃ d. IsGCD(d,b,x1)Definitions: IsGCD(d,b,x1)Original native command in the exact edition
  2. L50
    specialize IH x1
23Establish hallL51–55

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

  1. L51
    have hall : ∀ z. ∃ d. IsGCD(d,z,x1)Definitions: IsGCD(d,z,x1)Original native command in the exact edition
  2. L52
    apply IH
  3. L53
    exact hrB
  4. L54
    specialize hall b
  5. L55
    exact hall
24Separate the logical casesL56–56

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

  1. L56
    cases hsmall
25Construct an explicit witnessL57–57

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

  1. L57
    exists x2
26Use earlier factsL58–65

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

  1. L58
    specialize is_gcd_euclid_forward x2
  2. L59
    specialize is_gcd_euclid_forward a
  3. L60
    specialize is_gcd_euclid_forward b
  4. L61
    specialize is_gcd_euclid_forward x
  5. L62
    specialize is_gcd_euclid_forward x1
  6. L63
    apply is_gcd_euclid_forward
  7. L64
    exact hdiv_witness_witness_left
  8. L65
    exact hsmall_witness
27Establish hbBL66–69

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

  1. L66
  2. L67
    apply le_of_succ_le_succ
  3. L68
    exact hsplit_right
  4. L69
    specialize IH b
28Establish hallL70–74

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

  1. L70
    have hall : ∀ z. ∃ d. IsGCD(d,z,b)Definitions: IsGCD(d,z,b)Original native command in the exact edition
  2. L71
    apply IH
  3. L72
    exact hbB
  4. L73
    specialize hall a
  5. L74
    exact hall

Library-wide reading audit

Original defined command ledger · 74 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro b
  4. 0004intro hb
  5. 0005intro a
  6. 0006have hb0 : b = 0
  7. 0007apply le_zero
  8. 0008exact hb
  9. 0009exists a
  10. 0010split
  11. 0011split
  12. 0012specialize multiple_refl a
  13. 0013exact multiple_refl
  14. 0014exists 0
  15. 0015trans 0
  16. 0016exact hb0
  17. 0017symm
  18. 0018apply PA5
  19. 0019intro c
  20. 0020intro hca
  21. 0021intro hcb
  22. 0022exact hca
  23. 0023intro b
  24. 0024intro hb
  25. 0025intro a
  26. 0026specialize le_eq_or_lt b
  27. 0027specialize le_eq_or_lt (S B)
  28. 0028have hsplit : b = S B ∨ Lt(b,S B)
    Exact native replay linehave hsplit : b = S B \/ exists k. k + S b = S B
  29. 0029apply le_eq_or_lt
  30. 0030exact hb
  31. 0031cases hsplit
  32. 0032have hb0 : ~(b = 0)
  33. 0033intro hzero
  34. 0034apply PA1
  35. 0035trans b
  36. 0036symm
  37. 0037exact hsplit_left
  38. 0038exact hzero
  39. 0039have hdiv : ∃ q. ∃ r. DivRem(a,b,q,r)
    Exact native replay linehave hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
  40. 0040apply division_remainder_exists
  41. 0041exact hb0
  42. 0042cases hdiv
  43. 0043cases hdiv_witness
  44. 0044cases hdiv_witness_witness
  45. 0045have hrB : Le(x1,B)
    Exact native replay linehave hrB : exists k. k + x1 = B
  46. 0046apply le_of_succ_le_succ
  47. 0047rewrite hsplit_left at hdiv_witness_witness_right
  48. 0048exact hdiv_witness_witness_right
  49. 0049have hsmall : ∃ d. IsGCD(d,b,x1)
    Exact native replay linehave hsmall : exists d. (((exists u. b = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. b = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
  50. 0050specialize IH x1
  51. 0051have hall : ∀ z. ∃ d. IsGCD(d,z,x1)
    Exact native replay linehave hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w)
  52. 0052apply IH
  53. 0053exact hrB
  54. 0054specialize hall b
  55. 0055exact hall
  56. 0056cases hsmall
  57. 0057exists x2
  58. 0058specialize is_gcd_euclid_forward x2
  59. 0059specialize is_gcd_euclid_forward a
  60. 0060specialize is_gcd_euclid_forward b
  61. 0061specialize is_gcd_euclid_forward x
  62. 0062specialize is_gcd_euclid_forward x1
  63. 0063apply is_gcd_euclid_forward
  64. 0064exact hdiv_witness_witness_left
  65. 0065exact hsmall_witness
  66. 0066have hbB : Le(b,B)
    Exact native replay linehave hbB : exists k. k + b = B
  67. 0067apply le_of_succ_le_succ
  68. 0068exact hsplit_right
  69. 0069specialize IH b
  70. 0070have hall : ∀ z. ∃ d. IsGCD(d,z,b)
    Exact native replay linehave hall : forall z. exists d. (((exists u. z = d * u) /\ (exists v. b = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. b = c * t) -> exists w. d = c * w)
  71. 0071apply IH
  72. 0072exact hbB
  73. 0073specialize hall a
  74. 0074exact hall