PA0026 · theorem

binary_crt

Stable checked-use theorem · independently closed

Constructive binary CRT for positive coprime natural moduli using balanced congruence.

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

∀ m. ∀ n. ∀ a. ∀ b. ¬m = 0 → ¬n = 0 → Coprime(m,n) → ∃ x. ModEq(m,x,a) ∧ ModEq(n,x,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

PD0005 Coprime PD0008 ModEq

3 occurrences

In local proof propositions

PD0008 ModEq

27 occurrences

Exact expanded native-PA statement
forall m n a b. ~(m = 0) -> ~(n = 0) -> (forall d. (exists u. m = d * u) -> (exists v. n = d * v) -> d = 1) -> exists x. (exists u v. x + m * u = a + m * v) /\ (exists r s. x + n * r = b + n * s)

Proof neighborhood

Direct theorem prerequisites

PA001V nonzero_is_succ PA001M coprime_balanced_bezout PA001W bezout_mod_left PA001X bezout_mod_right PA0020 mod_eq_mul_left PA000A mul_add PA0002 mul_one PA0021 dvd_to_mod_zero PA000B mul_assoc PA000H mul_comm PA0022 mod_eq_add PA0023 mod_eq_refl PA0024 mod_eq_trans PA0025 mod_eq_predecessor_cancel PA0001 zero_add

Direct theorem dependents

PA0028 binary_crt_fold_step

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

276 script commands · 82 reading checkpoints · 35 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 (15)
nonzero is succcoprime balanced bezoutbezout mod leftbezout mod rightmod eq mul leftmul addmul onedvd to mod zeromul assocmul commmod eq addmod eq reflmod eq transmod eq predecessor cancelzero add
01Fix variables and assumptionsL1–7

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro hm
  6. L6
    intro hn
  7. L7
    intro hcop
02Establish hmsL8–11

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

  1. L8
    have hms : exists k. m = S k
  2. L9
    specialize nonzero_is_succ m
  3. L10
    apply nonzero_is_succ
  4. L11
    exact hm
03Establish hnsL12–15

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

  1. L12
    have hns : exists k. n = S k
  2. L13
    specialize nonzero_is_succ n
  3. L14
    apply nonzero_is_succ
  4. L15
    exact hn
04Establish hbezL16–20

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

  1. L16
    have hbez : exists xp yp xn yn. m * xp + n * yp = 1 + (m * xn + n * yn)
  2. L17
    specialize coprime_balanced_bezout m
  3. L18
    specialize coprime_balanced_bezout n
  4. L19
    apply coprime_balanced_bezout
  5. L20
    exact hcop
05Separate the logical casesL21–26

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

  1. L21
    cases hms
  2. L22
    cases hns
  3. L23
    cases hbez
  4. L24
    cases hbez_witness
  5. L25
    cases hbez_witness_witness
  6. L26
    cases hbez_witness_witness_witness
06Establish hblL27–35

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

  1. L27
    have hbl : ModEq(m,n · x3,1 + n · x5)Definitions: ModEq(m,n · x3,1 + n · x5)Original native command in the exact edition
  2. L28
    specialize bezout_mod_left m
  3. L29
    specialize bezout_mod_left n
  4. L30
    specialize bezout_mod_left x2
  5. L31
    specialize bezout_mod_left x3
  6. L32
    specialize bezout_mod_left x4
  7. L33
    specialize bezout_mod_left x5
  8. L34
    apply bezout_mod_left
  9. L35
    exact hbez_witness_witness_witness_witness
07Establish hbrL36–44

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

  1. L36
    have hbr : ModEq(n,m · x2,1 + m · x4)Definitions: ModEq(n,m · x2,1 + m · x4)Original native command in the exact edition
  2. L37
    specialize bezout_mod_right m
  3. L38
    specialize bezout_mod_right n
  4. L39
    specialize bezout_mod_right x2
  5. L40
    specialize bezout_mod_right x3
  6. L41
    specialize bezout_mod_right x4
  7. L42
    specialize bezout_mod_right x5
  8. L43
    apply bezout_mod_right
  9. L44
    exact hbez_witness_witness_witness_witness
08Establish hal0L45–51

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

  1. L45
    have hal0 : ModEq(m,a · (n · x3),a · (1 + n · x5))Definitions: ModEq(m,a · (n · x3),a · (1 + n · x5))Original native command in the exact edition
  2. L46
    specialize mod_eq_mul_left m
  3. L47
    specialize mod_eq_mul_left (n * x3)
  4. L48
    specialize mod_eq_mul_left (1 + n * x5)
  5. L49
    specialize mod_eq_mul_left a
  6. L50
    apply mod_eq_mul_left
  7. L51
    exact hbl
09Establish halL52–52

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

  1. L52
    have hal : ModEq(m,a · (n · x3),a + a · (n · x5))Definitions: ModEq(m,a · (n · x3),a + a · (n · x5))Original native command in the exact edition
10Establish haexpandL53–60

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

  1. L53
    have haexpand : a * (1 + n * x5) = a + a * (n * x5)
  2. L54
    trans a * 1 + a * (n * x5)
  3. L55
    apply mul_add
  4. L56
    congr
  5. L57
    apply mul_one
  6. L58
    refl
  7. L59
    rewrite <- haexpand
  8. L60
    exact hal0
11Establish hbmL61–62

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

  1. L61
    have hbm : ModEq(m,b · (m · x2),0)Definitions: ModEq(m,b · (m · x2),0)Original native command in the exact edition
  2. L62
    apply dvd_to_mod_zero
12Construct an explicit witnessL63–63

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

  1. L63
    exists b * x2
13Calculate and transport equalitiesL64–65

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

  1. L64
    trans (b * m) * x2
  2. L65
    symm
14Use earlier factsL66–66

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

  1. L66
    apply mul_assoc
15Calculate and transport equalitiesL67–68

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

  1. L67
    trans (m * b) * x2
  2. L68
    congr
16Use earlier factsL69–69

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

  1. L69
    apply mul_comm
17Calculate and transport equalitiesL70–70

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

  1. L70
    refl
18Use earlier factsL71–71

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

  1. L71
    apply mul_assoc
19Establish hymL72–80

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

  1. L72
    have hym : ModEq(m,a · (n · x3) + b · (m · x2),a + a · (n · x5) + 0)Definitions: ModEq(m,a · (n · x3) + b · (m · x2),a + a · (n · x5) + 0)Original native command in the exact edition
  2. L73
    specialize mod_eq_add m
  3. L74
    specialize mod_eq_add (a * (n * x3))
  4. L75
    specialize mod_eq_add (a + a * (n * x5))
  5. L76
    specialize mod_eq_add (b * (m * x2))
  6. L77
    specialize mod_eq_add 0
  7. L78
    apply mod_eq_add
  8. L79
    exact hal
  9. L80
    exact hbm
20Establish hym_normL81–81

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

  1. L81
    have hym_norm : ModEq(m,a · (n · x3) + b · (m · x2),a + a · (n · x5))Definitions: ModEq(m,a · (n · x3) + b · (m · x2),a + a · (n · x5))Original native command in the exact edition
21Establish hym_zeroL82–86

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

  1. L82
    have hym_zero : (a + a * (n * x5)) + 0 = a + a * (n * x5)
  2. L83
    rewrite PA3
  3. L84
    refl
  4. L85
    rewrite <- hym_zero
  5. L86
    exact hym
22Establish hkmL87–90

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

  1. L87
    have hkm : ModEq(m,x · (a · (n · x5)),x · (a · (n · x5)))Definitions: ModEq(m,x · (a · (n · x5)),x · (a · (n · x5)))Original native command in the exact edition
  2. L88
    specialize mod_eq_refl m
  3. L89
    specialize mod_eq_refl (x * (a * (n * x5)))
  4. L90
    apply mod_eq_refl
23Establish hymkL91–99

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

  1. L91
    have hymk : ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),a + a · (n · x5) + x · (a · (n · x5)))Definitions: ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),a + a · (n · x5) + x · (a · (n · x5)))Original native command in the exact edition
  2. L92
    specialize mod_eq_add m
  3. L93
    specialize mod_eq_add ((a * (n * x3)) + (b * (m * x2)))
  4. L94
    specialize mod_eq_add (a + a * (n * x5))
  5. L95
    specialize mod_eq_add (x * (a * (n * x5)))
  6. L96
    specialize mod_eq_add (x * (a * (n * x5)))
  7. L97
    apply mod_eq_add
  8. L98
    exact hym_norm
  9. L99
    exact hkm
24Establish hcancelmL100–106

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

  1. L100
    have hcancelm : ModEq(S x,a + a · (n · x5) + x · (a · (n · x5)),a)Definitions: ModEq(S x,a + a · (n · x5) + x · (a · (n · x5)),a)Original native command in the exact edition
  2. L101
    specialize mod_eq_predecessor_cancel x
  3. L102
    specialize mod_eq_predecessor_cancel a
  4. L103
    specialize mod_eq_predecessor_cancel (a * (n * x5))
  5. L104
    apply mod_eq_predecessor_cancel
  6. L105
    rewrite <- hms_witness at hcancelm
  7. L106
    rewrite <- hms_witness at hcancelm
25Establish hbasemL107–114

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

  1. L107
    have hbasem : ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),a)Definitions: ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),a)Original native command in the exact edition
  2. L108
    specialize mod_eq_trans m
  3. L109
    specialize mod_eq_trans (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  4. L110
    specialize mod_eq_trans ((a + a * (n * x5)) + (x * (a * (n * x5))))
  5. L111
    specialize mod_eq_trans a
  6. L112
    apply mod_eq_trans
  7. L113
    exact hymk
  8. L114
    exact hcancelm
26Establish hknznmL115–116

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

  1. L115
    have hknznm : ModEq(m,x1 · (b · (m · x4)),0)Definitions: ModEq(m,x1 · (b · (m · x4)),0)Original native command in the exact edition
  2. L116
    apply dvd_to_mod_zero
27Construct an explicit witnessL117–117

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

  1. L117
    exists x1 * (b * x4)
28Calculate and transport equalitiesL118–121

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

  1. L118
    trans x1 * ((b * m) * x4)
  2. L119
    congr
  3. L120
    refl
  4. L121
    symm
29Use earlier factsL122–122

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

  1. L122
    apply mul_assoc
30Calculate and transport equalitiesL123–126

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

  1. L123
    trans x1 * ((m * b) * x4)
  2. L124
    congr
  3. L125
    refl
  4. L126
    congr
31Use earlier factsL127–127

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

  1. L127
    apply mul_comm
32Calculate and transport equalitiesL128–131

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

  1. L128
    refl
  2. L129
    trans x1 * (m * (b * x4))
  3. L130
    congr
  4. L131
    refl
33Use earlier factsL132–132

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

  1. L132
    apply mul_assoc
34Calculate and transport equalitiesL133–134

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

  1. L133
    trans (x1 * m) * (b * x4)
  2. L134
    symm
35Use earlier factsL135–135

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

  1. L135
    apply mul_assoc
36Calculate and transport equalitiesL136–137

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

  1. L136
    trans (m * x1) * (b * x4)
  2. L137
    congr
37Use earlier factsL138–138

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

  1. L138
    apply mul_comm
38Calculate and transport equalitiesL139–139

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

  1. L139
    refl
39Use earlier factsL140–140

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

  1. L140
    apply mul_assoc
40Establish hfinalm0L141–149

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

  1. L141
    have hfinalm0 : ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),a + 0)Definitions: ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),a + 0)Original native command in the exact edition
  2. L142
    specialize mod_eq_add m
  3. L143
    specialize mod_eq_add (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  4. L144
    specialize mod_eq_add a
  5. L145
    specialize mod_eq_add (x1 * (b * (m * x4)))
  6. L146
    specialize mod_eq_add 0
  7. L147
    apply mod_eq_add
  8. L148
    exact hbasem
  9. L149
    exact hknznm
41Establish hazeromL150–150

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

  1. L150
    have hazerom : ModEq(m,a + 0,a)Definitions: ModEq(m,a + 0,a)Original native command in the exact edition
42Construct an explicit witnessL151–152

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

  1. L151
    exists 0
  2. L152
    exists 0
43Calculate and transport equalitiesL153–153

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

  1. L153
    simp
44Establish hfinalmL154–161

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

  1. L154
    have hfinalm : ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),a)Definitions: ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),a)Original native command in the exact edition
  2. L155
    specialize mod_eq_trans m
  3. L156
    specialize mod_eq_trans ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4))))
  4. L157
    specialize mod_eq_trans (a + 0)
  5. L158
    specialize mod_eq_trans a
  6. L159
    apply mod_eq_trans
  7. L160
    exact hfinalm0
  8. L161
    exact hazerom
45Establish hbn0L162–168

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

  1. L162
    have hbn0 : ModEq(n,b · (m · x2),b · (1 + m · x4))Definitions: ModEq(n,b · (m · x2),b · (1 + m · x4))Original native command in the exact edition
  2. L163
    specialize mod_eq_mul_left n
  3. L164
    specialize mod_eq_mul_left (m * x2)
  4. L165
    specialize mod_eq_mul_left (1 + m * x4)
  5. L166
    specialize mod_eq_mul_left b
  6. L167
    apply mod_eq_mul_left
  7. L168
    exact hbr
46Establish hbnL169–169

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

  1. L169
    have hbn : ModEq(n,b · (m · x2),b + b · (m · x4))Definitions: ModEq(n,b · (m · x2),b + b · (m · x4))Original native command in the exact edition
47Establish hbexpandL170–177

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

  1. L170
    have hbexpand : b * (1 + m * x4) = b + b * (m * x4)
  2. L171
    trans b * 1 + b * (m * x4)
  3. L172
    apply mul_add
  4. L173
    congr
  5. L174
    apply mul_one
  6. L175
    refl
  7. L176
    rewrite <- hbexpand
  8. L177
    exact hbn0
48Establish hanL178–179

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

  1. L178
    have han : ModEq(n,a · (n · x3),0)Definitions: ModEq(n,a · (n · x3),0)Original native command in the exact edition
  2. L179
    apply dvd_to_mod_zero
49Construct an explicit witnessL180–180

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

  1. L180
    exists a * x3
50Calculate and transport equalitiesL181–182

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

  1. L181
    trans (a * n) * x3
  2. L182
    symm
51Use earlier factsL183–183

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

  1. L183
    apply mul_assoc
52Calculate and transport equalitiesL184–185

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

  1. L184
    trans (n * a) * x3
  2. L185
    congr
53Use earlier factsL186–186

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

  1. L186
    apply mul_comm
54Calculate and transport equalitiesL187–187

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

  1. L187
    refl
55Use earlier factsL188–188

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

  1. L188
    apply mul_assoc
56Establish hyn0L189–197

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

  1. L189
    have hyn0 : ModEq(n,a · (n · x3) + b · (m · x2),0 + (b + b · (m · x4)))Definitions: ModEq(n,a · (n · x3) + b · (m · x2),0 + (b + b · (m · x4)))Original native command in the exact edition
  2. L190
    specialize mod_eq_add n
  3. L191
    specialize mod_eq_add (a * (n * x3))
  4. L192
    specialize mod_eq_add 0
  5. L193
    specialize mod_eq_add (b * (m * x2))
  6. L194
    specialize mod_eq_add (b + b * (m * x4))
  7. L195
    apply mod_eq_add
  8. L196
    exact han
  9. L197
    exact hbn
57Establish hyn_normL198–198

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

  1. L198
    have hyn_norm : ModEq(n,a · (n · x3) + b · (m · x2),b + b · (m · x4))Definitions: ModEq(n,a · (n · x3) + b · (m · x2),b + b · (m · x4))Original native command in the exact edition
58Establish hyn_zeroL199–203

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

  1. L199
    have hyn_zero : 0 + (b + b * (m * x4)) = b + b * (m * x4)
  2. L200
    specialize zero_add (b + b * (m * x4))
  3. L201
    exact zero_add
  4. L202
    rewrite <- hyn_zero
  5. L203
    exact hyn0
59Establish hkmzL204–205

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

  1. L204
    have hkmz : ModEq(n,x · (a · (n · x5)),0)Definitions: ModEq(n,x · (a · (n · x5)),0)Original native command in the exact edition
  2. L205
    apply dvd_to_mod_zero
60Construct an explicit witnessL206–206

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

  1. L206
    exists x * (a * x5)
61Calculate and transport equalitiesL207–210

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

  1. L207
    trans x * ((a * n) * x5)
  2. L208
    congr
  3. L209
    refl
  4. L210
    symm
62Use earlier factsL211–211

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

  1. L211
    apply mul_assoc
63Calculate and transport equalitiesL212–215

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

  1. L212
    trans x * ((n * a) * x5)
  2. L213
    congr
  3. L214
    refl
  4. L215
    congr
64Use earlier factsL216–216

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

  1. L216
    apply mul_comm
65Calculate and transport equalitiesL217–220

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

  1. L217
    refl
  2. L218
    trans x * (n * (a * x5))
  3. L219
    congr
  4. L220
    refl
66Use earlier factsL221–221

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

  1. L221
    apply mul_assoc
67Calculate and transport equalitiesL222–223

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

  1. L222
    trans (x * n) * (a * x5)
  2. L223
    symm
68Use earlier factsL224–224

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

  1. L224
    apply mul_assoc
69Calculate and transport equalitiesL225–226

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

  1. L225
    trans (n * x) * (a * x5)
  2. L226
    congr
70Use earlier factsL227–227

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

  1. L227
    apply mul_comm
71Calculate and transport equalitiesL228–228

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

  1. L228
    refl
72Use earlier factsL229–229

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

  1. L229
    apply mul_assoc
73Establish hyn1L230–238

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

  1. L230
    have hyn1 : ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),b + b · (m · x4) + 0)Definitions: ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),b + b · (m · x4) + 0)Original native command in the exact edition
  2. L231
    specialize mod_eq_add n
  3. L232
    specialize mod_eq_add ((a * (n * x3)) + (b * (m * x2)))
  4. L233
    specialize mod_eq_add (b + b * (m * x4))
  5. L234
    specialize mod_eq_add (x * (a * (n * x5)))
  6. L235
    specialize mod_eq_add 0
  7. L236
    apply mod_eq_add
  8. L237
    exact hyn_norm
  9. L238
    exact hkmz
74Establish hyn1_normL239–239

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

  1. L239
    have hyn1_norm : ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),b + b · (m · x4))Definitions: ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),b + b · (m · x4))Original native command in the exact edition
75Establish hyn1_zeroL240–244

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

  1. L240
    have hyn1_zero : (b + b * (m * x4)) + 0 = b + b * (m * x4)
  2. L241
    rewrite PA3
  3. L242
    refl
  4. L243
    rewrite <- hyn1_zero
  5. L244
    exact hyn1
76Establish hknL245–248

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

  1. L245
    have hkn : ModEq(n,x1 · (b · (m · x4)),x1 · (b · (m · x4)))Definitions: ModEq(n,x1 · (b · (m · x4)),x1 · (b · (m · x4)))Original native command in the exact edition
  2. L246
    specialize mod_eq_refl n
  3. L247
    specialize mod_eq_refl (x1 * (b * (m * x4)))
  4. L248
    apply mod_eq_refl
77Establish hynkL249–257

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

  1. L249
    have hynk : ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),b + b · (m · x4) + x1 · (b · (m · x4)))Definitions: ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),b + b · (m · x4) + x1 · (b · (m · x4)))Original native command in the exact edition
  2. L250
    specialize mod_eq_add n
  3. L251
    specialize mod_eq_add (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  4. L252
    specialize mod_eq_add (b + b * (m * x4))
  5. L253
    specialize mod_eq_add (x1 * (b * (m * x4)))
  6. L254
    specialize mod_eq_add (x1 * (b * (m * x4)))
  7. L255
    apply mod_eq_add
  8. L256
    exact hyn1_norm
  9. L257
    exact hkn
78Establish hcancelnL258–264

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

  1. L258
    have hcanceln : ModEq(S x1,b + b · (m · x4) + x1 · (b · (m · x4)),b)Definitions: ModEq(S x1,b + b · (m · x4) + x1 · (b · (m · x4)),b)Original native command in the exact edition
  2. L259
    specialize mod_eq_predecessor_cancel x1
  3. L260
    specialize mod_eq_predecessor_cancel b
  4. L261
    specialize mod_eq_predecessor_cancel (b * (m * x4))
  5. L262
    apply mod_eq_predecessor_cancel
  6. L263
    rewrite <- hns_witness at hcanceln
  7. L264
    rewrite <- hns_witness at hcanceln
79Establish hfinalnL265–272

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

  1. L265
    have hfinaln : ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),b)Definitions: ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),b)Original native command in the exact edition
  2. L266
    specialize mod_eq_trans n
  3. L267
    specialize mod_eq_trans ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4))))
  4. L268
    specialize mod_eq_trans ((b + b * (m * x4)) + (x1 * (b * (m * x4))))
  5. L269
    specialize mod_eq_trans b
  6. L270
    apply mod_eq_trans
  7. L271
    exact hynk
  8. L272
    exact hcanceln
80Construct an explicit witnessL273–273

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

  1. L273
    exists (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))
81Separate the logical casesL274–274

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

  1. L274
    split
82Use earlier factsL275–276

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

  1. L275
    exact hfinalm
  2. L276
    exact hfinaln

Library-wide reading audit

Original defined command ledger · 276 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro hm
  6. 0006intro hn
  7. 0007intro hcop
  8. 0008have hms : exists k. m = S k
  9. 0009specialize nonzero_is_succ m
  10. 0010apply nonzero_is_succ
  11. 0011exact hm
  12. 0012have hns : exists k. n = S k
  13. 0013specialize nonzero_is_succ n
  14. 0014apply nonzero_is_succ
  15. 0015exact hn
  16. 0016have hbez : exists xp yp xn yn. m * xp + n * yp = 1 + (m * xn + n * yn)
  17. 0017specialize coprime_balanced_bezout m
  18. 0018specialize coprime_balanced_bezout n
  19. 0019apply coprime_balanced_bezout
  20. 0020exact hcop
  21. 0021cases hms
  22. 0022cases hns
  23. 0023cases hbez
  24. 0024cases hbez_witness
  25. 0025cases hbez_witness_witness
  26. 0026cases hbez_witness_witness_witness
  27. 0027have hbl : ModEq(m,n · x3,1 + n · x5)
    Exact native replay linehave hbl : exists u v. n * x3 + m * u = (1 + n * x5) + m * v
  28. 0028specialize bezout_mod_left m
  29. 0029specialize bezout_mod_left n
  30. 0030specialize bezout_mod_left x2
  31. 0031specialize bezout_mod_left x3
  32. 0032specialize bezout_mod_left x4
  33. 0033specialize bezout_mod_left x5
  34. 0034apply bezout_mod_left
  35. 0035exact hbez_witness_witness_witness_witness
  36. 0036have hbr : ModEq(n,m · x2,1 + m · x4)
    Exact native replay linehave hbr : exists u v. m * x2 + n * u = (1 + m * x4) + n * v
  37. 0037specialize bezout_mod_right m
  38. 0038specialize bezout_mod_right n
  39. 0039specialize bezout_mod_right x2
  40. 0040specialize bezout_mod_right x3
  41. 0041specialize bezout_mod_right x4
  42. 0042specialize bezout_mod_right x5
  43. 0043apply bezout_mod_right
  44. 0044exact hbez_witness_witness_witness_witness
  45. 0045have hal0 : ModEq(m,a · (n · x3),a · (1 + n · x5))
    Exact native replay linehave hal0 : exists u v. (a * (n * x3)) + m * u = (a * (1 + n * x5)) + m * v
  46. 0046specialize mod_eq_mul_left m
  47. 0047specialize mod_eq_mul_left (n * x3)
  48. 0048specialize mod_eq_mul_left (1 + n * x5)
  49. 0049specialize mod_eq_mul_left a
  50. 0050apply mod_eq_mul_left
  51. 0051exact hbl
  52. 0052have hal : ModEq(m,a · (n · x3),a + a · (n · x5))
    Exact native replay linehave hal : exists u v. (a * (n * x3)) + m * u = (a + a * (n * x5)) + m * v
  53. 0053have haexpand : a * (1 + n * x5) = a + a * (n * x5)
  54. 0054trans a * 1 + a * (n * x5)
  55. 0055apply mul_add
  56. 0056congr
  57. 0057apply mul_one
  58. 0058refl
  59. 0059rewrite <- haexpand
  60. 0060exact hal0
  61. 0061have hbm : ModEq(m,b · (m · x2),0)
    Exact native replay linehave hbm : exists u v. (b * (m * x2)) + m * u = 0 + m * v
  62. 0062apply dvd_to_mod_zero
  63. 0063exists b * x2
  64. 0064trans (b * m) * x2
  65. 0065symm
  66. 0066apply mul_assoc
  67. 0067trans (m * b) * x2
  68. 0068congr
  69. 0069apply mul_comm
  70. 0070refl
  71. 0071apply mul_assoc
  72. 0072have hym : ModEq(m,a · (n · x3) + b · (m · x2),a + a · (n · x5) + 0)
    Exact native replay linehave hym : exists u v. ((a * (n * x3)) + (b * (m * x2))) + m * u = ((a + a * (n * x5)) + 0) + m * v
  73. 0073specialize mod_eq_add m
  74. 0074specialize mod_eq_add (a * (n * x3))
  75. 0075specialize mod_eq_add (a + a * (n * x5))
  76. 0076specialize mod_eq_add (b * (m * x2))
  77. 0077specialize mod_eq_add 0
  78. 0078apply mod_eq_add
  79. 0079exact hal
  80. 0080exact hbm
  81. 0081have hym_norm : ModEq(m,a · (n · x3) + b · (m · x2),a + a · (n · x5))
    Exact native replay linehave hym_norm : exists u v. ((a * (n * x3)) + (b * (m * x2))) + m * u = (a + a * (n * x5)) + m * v
  82. 0082have hym_zero : (a + a * (n * x5)) + 0 = a + a * (n * x5)
  83. 0083rewrite PA3
  84. 0084refl
  85. 0085rewrite <- hym_zero
  86. 0086exact hym
  87. 0087have hkm : ModEq(m,x · (a · (n · x5)),x · (a · (n · x5)))
    Exact native replay linehave hkm : exists u v. (x * (a * (n * x5))) + m * u = (x * (a * (n * x5))) + m * v
  88. 0088specialize mod_eq_refl m
  89. 0089specialize mod_eq_refl (x * (a * (n * x5)))
  90. 0090apply mod_eq_refl
  91. 0091have hymk : ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),a + a · (n · x5) + x · (a · (n · x5)))
    Exact native replay linehave hymk : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + m * u = ((a + a * (n * x5)) + (x * (a * (n * x5)))) + m * v
  92. 0092specialize mod_eq_add m
  93. 0093specialize mod_eq_add ((a * (n * x3)) + (b * (m * x2)))
  94. 0094specialize mod_eq_add (a + a * (n * x5))
  95. 0095specialize mod_eq_add (x * (a * (n * x5)))
  96. 0096specialize mod_eq_add (x * (a * (n * x5)))
  97. 0097apply mod_eq_add
  98. 0098exact hym_norm
  99. 0099exact hkm
  100. 0100have hcancelm : ModEq(S x,a + a · (n · x5) + x · (a · (n · x5)),a)
    Exact native replay linehave hcancelm : exists u v. ((a + a * (n * x5)) + x * (a * (n * x5))) + S x * u = a + S x * v
  101. 0101specialize mod_eq_predecessor_cancel x
  102. 0102specialize mod_eq_predecessor_cancel a
  103. 0103specialize mod_eq_predecessor_cancel (a * (n * x5))
  104. 0104apply mod_eq_predecessor_cancel
  105. 0105rewrite <- hms_witness at hcancelm
  106. 0106rewrite <- hms_witness at hcancelm
  107. 0107have hbasem : ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),a)
    Exact native replay linehave hbasem : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + m * u = a + m * v
  108. 0108specialize mod_eq_trans m
  109. 0109specialize mod_eq_trans (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  110. 0110specialize mod_eq_trans ((a + a * (n * x5)) + (x * (a * (n * x5))))
  111. 0111specialize mod_eq_trans a
  112. 0112apply mod_eq_trans
  113. 0113exact hymk
  114. 0114exact hcancelm
  115. 0115have hknznm : ModEq(m,x1 · (b · (m · x4)),0)
    Exact native replay linehave hknznm : exists u v. (x1 * (b * (m * x4))) + m * u = 0 + m * v
  116. 0116apply dvd_to_mod_zero
  117. 0117exists x1 * (b * x4)
  118. 0118trans x1 * ((b * m) * x4)
  119. 0119congr
  120. 0120refl
  121. 0121symm
  122. 0122apply mul_assoc
  123. 0123trans x1 * ((m * b) * x4)
  124. 0124congr
  125. 0125refl
  126. 0126congr
  127. 0127apply mul_comm
  128. 0128refl
  129. 0129trans x1 * (m * (b * x4))
  130. 0130congr
  131. 0131refl
  132. 0132apply mul_assoc
  133. 0133trans (x1 * m) * (b * x4)
  134. 0134symm
  135. 0135apply mul_assoc
  136. 0136trans (m * x1) * (b * x4)
  137. 0137congr
  138. 0138apply mul_comm
  139. 0139refl
  140. 0140apply mul_assoc
  141. 0141have hfinalm0 : ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),a + 0)
    Exact native replay linehave hfinalm0 : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + m * u = (a + 0) + m * v
  142. 0142specialize mod_eq_add m
  143. 0143specialize mod_eq_add (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  144. 0144specialize mod_eq_add a
  145. 0145specialize mod_eq_add (x1 * (b * (m * x4)))
  146. 0146specialize mod_eq_add 0
  147. 0147apply mod_eq_add
  148. 0148exact hbasem
  149. 0149exact hknznm
  150. 0150have hazerom : ModEq(m,a + 0,a)
    Exact native replay linehave hazerom : exists u v. (a + 0) + m * u = a + m * v
  151. 0151exists 0
  152. 0152exists 0
  153. 0153simp
  154. 0154have hfinalm : ModEq(m,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),a)
    Exact native replay linehave hfinalm : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + m * u = a + m * v
  155. 0155specialize mod_eq_trans m
  156. 0156specialize mod_eq_trans ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4))))
  157. 0157specialize mod_eq_trans (a + 0)
  158. 0158specialize mod_eq_trans a
  159. 0159apply mod_eq_trans
  160. 0160exact hfinalm0
  161. 0161exact hazerom
  162. 0162have hbn0 : ModEq(n,b · (m · x2),b · (1 + m · x4))
    Exact native replay linehave hbn0 : exists u v. (b * (m * x2)) + n * u = (b * (1 + m * x4)) + n * v
  163. 0163specialize mod_eq_mul_left n
  164. 0164specialize mod_eq_mul_left (m * x2)
  165. 0165specialize mod_eq_mul_left (1 + m * x4)
  166. 0166specialize mod_eq_mul_left b
  167. 0167apply mod_eq_mul_left
  168. 0168exact hbr
  169. 0169have hbn : ModEq(n,b · (m · x2),b + b · (m · x4))
    Exact native replay linehave hbn : exists u v. (b * (m * x2)) + n * u = (b + b * (m * x4)) + n * v
  170. 0170have hbexpand : b * (1 + m * x4) = b + b * (m * x4)
  171. 0171trans b * 1 + b * (m * x4)
  172. 0172apply mul_add
  173. 0173congr
  174. 0174apply mul_one
  175. 0175refl
  176. 0176rewrite <- hbexpand
  177. 0177exact hbn0
  178. 0178have han : ModEq(n,a · (n · x3),0)
    Exact native replay linehave han : exists u v. (a * (n * x3)) + n * u = 0 + n * v
  179. 0179apply dvd_to_mod_zero
  180. 0180exists a * x3
  181. 0181trans (a * n) * x3
  182. 0182symm
  183. 0183apply mul_assoc
  184. 0184trans (n * a) * x3
  185. 0185congr
  186. 0186apply mul_comm
  187. 0187refl
  188. 0188apply mul_assoc
  189. 0189have hyn0 : ModEq(n,a · (n · x3) + b · (m · x2),0 + (b + b · (m · x4)))
    Exact native replay linehave hyn0 : exists u v. ((a * (n * x3)) + (b * (m * x2))) + n * u = (0 + (b + b * (m * x4))) + n * v
  190. 0190specialize mod_eq_add n
  191. 0191specialize mod_eq_add (a * (n * x3))
  192. 0192specialize mod_eq_add 0
  193. 0193specialize mod_eq_add (b * (m * x2))
  194. 0194specialize mod_eq_add (b + b * (m * x4))
  195. 0195apply mod_eq_add
  196. 0196exact han
  197. 0197exact hbn
  198. 0198have hyn_norm : ModEq(n,a · (n · x3) + b · (m · x2),b + b · (m · x4))
    Exact native replay linehave hyn_norm : exists u v. ((a * (n * x3)) + (b * (m * x2))) + n * u = (b + b * (m * x4)) + n * v
  199. 0199have hyn_zero : 0 + (b + b * (m * x4)) = b + b * (m * x4)
  200. 0200specialize zero_add (b + b * (m * x4))
  201. 0201exact zero_add
  202. 0202rewrite <- hyn_zero
  203. 0203exact hyn0
  204. 0204have hkmz : ModEq(n,x · (a · (n · x5)),0)
    Exact native replay linehave hkmz : exists u v. (x * (a * (n * x5))) + n * u = 0 + n * v
  205. 0205apply dvd_to_mod_zero
  206. 0206exists x * (a * x5)
  207. 0207trans x * ((a * n) * x5)
  208. 0208congr
  209. 0209refl
  210. 0210symm
  211. 0211apply mul_assoc
  212. 0212trans x * ((n * a) * x5)
  213. 0213congr
  214. 0214refl
  215. 0215congr
  216. 0216apply mul_comm
  217. 0217refl
  218. 0218trans x * (n * (a * x5))
  219. 0219congr
  220. 0220refl
  221. 0221apply mul_assoc
  222. 0222trans (x * n) * (a * x5)
  223. 0223symm
  224. 0224apply mul_assoc
  225. 0225trans (n * x) * (a * x5)
  226. 0226congr
  227. 0227apply mul_comm
  228. 0228refl
  229. 0229apply mul_assoc
  230. 0230have hyn1 : ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),b + b · (m · x4) + 0)
    Exact native replay linehave hyn1 : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + n * u = ((b + b * (m * x4)) + 0) + n * v
  231. 0231specialize mod_eq_add n
  232. 0232specialize mod_eq_add ((a * (n * x3)) + (b * (m * x2)))
  233. 0233specialize mod_eq_add (b + b * (m * x4))
  234. 0234specialize mod_eq_add (x * (a * (n * x5)))
  235. 0235specialize mod_eq_add 0
  236. 0236apply mod_eq_add
  237. 0237exact hyn_norm
  238. 0238exact hkmz
  239. 0239have hyn1_norm : ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)),b + b · (m · x4))
    Exact native replay linehave hyn1_norm : exists u v. (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + n * u = (b + b * (m * x4)) + n * v
  240. 0240have hyn1_zero : (b + b * (m * x4)) + 0 = b + b * (m * x4)
  241. 0241rewrite PA3
  242. 0242refl
  243. 0243rewrite <- hyn1_zero
  244. 0244exact hyn1
  245. 0245have hkn : ModEq(n,x1 · (b · (m · x4)),x1 · (b · (m · x4)))
    Exact native replay linehave hkn : exists u v. (x1 * (b * (m * x4))) + n * u = (x1 * (b * (m * x4))) + n * v
  246. 0246specialize mod_eq_refl n
  247. 0247specialize mod_eq_refl (x1 * (b * (m * x4)))
  248. 0248apply mod_eq_refl
  249. 0249have hynk : ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),b + b · (m · x4) + x1 · (b · (m · x4)))
    Exact native replay linehave hynk : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + n * u = ((b + b * (m * x4)) + (x1 * (b * (m * x4)))) + n * v
  250. 0250specialize mod_eq_add n
  251. 0251specialize mod_eq_add (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5))))
  252. 0252specialize mod_eq_add (b + b * (m * x4))
  253. 0253specialize mod_eq_add (x1 * (b * (m * x4)))
  254. 0254specialize mod_eq_add (x1 * (b * (m * x4)))
  255. 0255apply mod_eq_add
  256. 0256exact hyn1_norm
  257. 0257exact hkn
  258. 0258have hcanceln : ModEq(S x1,b + b · (m · x4) + x1 · (b · (m · x4)),b)
    Exact native replay linehave hcanceln : exists u v. ((b + b * (m * x4)) + x1 * (b * (m * x4))) + S x1 * u = b + S x1 * v
  259. 0259specialize mod_eq_predecessor_cancel x1
  260. 0260specialize mod_eq_predecessor_cancel b
  261. 0261specialize mod_eq_predecessor_cancel (b * (m * x4))
  262. 0262apply mod_eq_predecessor_cancel
  263. 0263rewrite <- hns_witness at hcanceln
  264. 0264rewrite <- hns_witness at hcanceln
  265. 0265have hfinaln : ModEq(n,a · (n · x3) + b · (m · x2) + x · (a · (n · x5)) + x1 · (b · (m · x4)),b)
    Exact native replay linehave hfinaln : exists u v. ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))) + n * u = b + n * v
  266. 0266specialize mod_eq_trans n
  267. 0267specialize mod_eq_trans ((((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4))))
  268. 0268specialize mod_eq_trans ((b + b * (m * x4)) + (x1 * (b * (m * x4))))
  269. 0269specialize mod_eq_trans b
  270. 0270apply mod_eq_trans
  271. 0271exact hynk
  272. 0272exact hcanceln
  273. 0273exists (((a * (n * x3)) + (b * (m * x2))) + (x * (a * (n * x5)))) + (x1 * (b * (m * x4)))
  274. 0274split
  275. 0275exact hfinalm
  276. 0276exact hfinaln