GC000C

crt_merge_compatible_prefix_canonical_exists_unique

Every arbitrary finite positive non-coprime congruence system satisfying the exact operational gcd-merge invariant has its genuine LCM and exactly one strictly bounded solution.

Alpha v34 checked-use · first admitted v25 · independently kernel and Lean verified; not Stable

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.

Historical partial components only: this chapter proves canonical solutions under successive-merge compatibility and in the pairwise-compatible dominating-last case. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible finite lists, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. CRTPositiveModuliPrefix(b,c,l) → CRTMergeCompatiblePrefix(r,s,b,c,l) → ∃ x. ∃ y. CRTCanonicalPrefixSolution(r,s,b,c,l,x,y) ∧ (∀ z. CRTCanonicalPrefixSolution(r,s,b,c,l,z,y) → z = x)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

CRTPositiveModuliPrefix(b,c,l) · 1CRTCanonicalPrefixSolution(r,s,b,c,l,x,M) · 2CRTMergeCompatiblePrefix(r,s,b,c,l) · 1

Actual proof prerequisites

crt_merge_compatible_prefix_solution_existscrt_prefix_lcm_exists_unique · checked external prerequisitecrt_positive_prefix_lcm_nonzerocrt_prefix_solution_canonical_remainder · checked external prerequisitecrt_canonical_prefix_solution_unique · checked external prerequisite
Original expanded first-order statement 
forall r s b c l. (forall gcrt_positive_index_gcomp_canonical_positive gcrt_positive_value_gcomp_canonical_positive. (exists ff_lt_gcrt_gcomp_canonical_positive_bound. ff_lt_gcrt_gcomp_canonical_positive_bound + S gcrt_positive_index_gcomp_canonical_positive = l) -> (((exists ff_h_gcrt_gcomp_canonical_positive_entry. ff_h_gcrt_gcomp_canonical_positive_entry + S (gcrt_positive_value_gcomp_canonical_positive) = S ((S (gcrt_positive_index_gcomp_canonical_positive)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_positive_entry. b = ff_q_gcrt_gcomp_canonical_positive_entry * S ((S (gcrt_positive_index_gcomp_canonical_positive)) * c) + (gcrt_positive_value_gcomp_canonical_positive))) -> ~(gcrt_positive_value_gcomp_canonical_positive = 0)) -> (forall gcomp_merge_index_gcomp_canonical_merge gcomp_merge_solution_gcomp_canonical_merge gcomp_merge_lcm_gcomp_canonical_merge gcomp_merge_residue_gcomp_canonical_merge gcomp_merge_modulus_gcomp_canonical_merge gcomp_merge_gcd_gcomp_canonical_merge. (exists ff_lt_gcrt_gcomp_canonical_merge_bound. ff_lt_gcrt_gcomp_canonical_merge_bound + S gcomp_merge_index_gcomp_canonical_merge = l) -> (((forall gcrt_common_index_gcomp_canonical_merge_lcm_own gcrt_common_modulus_gcomp_canonical_merge_lcm_own. (exists ff_lt_gcrt_gcomp_canonical_merge_lcm_own_bound. ff_lt_gcrt_gcomp_canonical_merge_lcm_own_bound + S gcrt_common_index_gcomp_canonical_merge_lcm_own = gcomp_merge_index_gcomp_canonical_merge) -> (((exists ff_h_gcrt_gcomp_canonical_merge_lcm_own_entry. ff_h_gcrt_gcomp_canonical_merge_lcm_own_entry + S (gcrt_common_modulus_gcomp_canonical_merge_lcm_own) = S ((S (gcrt_common_index_gcomp_canonical_merge_lcm_own)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_merge_lcm_own_entry. b = ff_q_gcrt_gcomp_canonical_merge_lcm_own_entry * S ((S (gcrt_common_index_gcomp_canonical_merge_lcm_own)) * c) + (gcrt_common_modulus_gcomp_canonical_merge_lcm_own))) -> exists gcrt_common_quotient_gcomp_canonical_merge_lcm_own. gcomp_merge_lcm_gcomp_canonical_merge = gcrt_common_modulus_gcomp_canonical_merge_lcm_own * gcrt_common_quotient_gcomp_canonical_merge_lcm_own) /\ forall gcrt_lcm_common_gcomp_canonical_merge_lcm. (forall gcrt_common_index_gcomp_canonical_merge_lcm_other gcrt_common_modulus_gcomp_canonical_merge_lcm_other. (exists ff_lt_gcrt_gcomp_canonical_merge_lcm_other_bound. ff_lt_gcrt_gcomp_canonical_merge_lcm_other_bound + S gcrt_common_index_gcomp_canonical_merge_lcm_other = gcomp_merge_index_gcomp_canonical_merge) -> (((exists ff_h_gcrt_gcomp_canonical_merge_lcm_other_entry. ff_h_gcrt_gcomp_canonical_merge_lcm_other_entry + S (gcrt_common_modulus_gcomp_canonical_merge_lcm_other) = S ((S (gcrt_common_index_gcomp_canonical_merge_lcm_other)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_merge_lcm_other_entry. b = ff_q_gcrt_gcomp_canonical_merge_lcm_other_entry * S ((S (gcrt_common_index_gcomp_canonical_merge_lcm_other)) * c) + (gcrt_common_modulus_gcomp_canonical_merge_lcm_other))) -> exists gcrt_common_quotient_gcomp_canonical_merge_lcm_other. gcrt_lcm_common_gcomp_canonical_merge_lcm = gcrt_common_modulus_gcomp_canonical_merge_lcm_other * gcrt_common_quotient_gcomp_canonical_merge_lcm_other) -> exists gcrt_lcm_quotient_gcomp_canonical_merge_lcm. gcrt_lcm_common_gcomp_canonical_merge_lcm = gcomp_merge_lcm_gcomp_canonical_merge * gcrt_lcm_quotient_gcomp_canonical_merge_lcm)) -> (forall gcrt_solution_index_gcomp_canonical_merge_solution gcrt_solution_residue_gcomp_canonical_merge_solution gcrt_solution_modulus_gcomp_canonical_merge_solution. (exists ff_lt_gcrt_gcomp_canonical_merge_solution_bound. ff_lt_gcrt_gcomp_canonical_merge_solution_bound + S gcrt_solution_index_gcomp_canonical_merge_solution = gcomp_merge_index_gcomp_canonical_merge) -> (((exists ff_h_gcrt_gcomp_canonical_merge_solution_residue. ff_h_gcrt_gcomp_canonical_merge_solution_residue + S (gcrt_solution_residue_gcomp_canonical_merge_solution) = S ((S (gcrt_solution_index_gcomp_canonical_merge_solution)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_merge_solution_residue. r = ff_q_gcrt_gcomp_canonical_merge_solution_residue * S ((S (gcrt_solution_index_gcomp_canonical_merge_solution)) * s) + (gcrt_solution_residue_gcomp_canonical_merge_solution))) -> (((exists ff_h_gcrt_gcomp_canonical_merge_solution_modulus. ff_h_gcrt_gcomp_canonical_merge_solution_modulus + S (gcrt_solution_modulus_gcomp_canonical_merge_solution) = S ((S (gcrt_solution_index_gcomp_canonical_merge_solution)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_merge_solution_modulus. b = ff_q_gcrt_gcomp_canonical_merge_solution_modulus * S ((S (gcrt_solution_index_gcomp_canonical_merge_solution)) * c) + (gcrt_solution_modulus_gcomp_canonical_merge_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_merge_solution_congruence hgcrt_mod_right_gcrt_gcomp_canonical_merge_solution_congruence. gcomp_merge_solution_gcomp_canonical_merge + gcrt_solution_modulus_gcomp_canonical_merge_solution * hgcrt_mod_left_gcrt_gcomp_canonical_merge_solution_congruence = gcrt_solution_residue_gcomp_canonical_merge_solution + gcrt_solution_modulus_gcomp_canonical_merge_solution * hgcrt_mod_right_gcrt_gcomp_canonical_merge_solution_congruence)) -> (((exists ff_h_gcrt_gcomp_canonical_merge_residue. ff_h_gcrt_gcomp_canonical_merge_residue + S (gcomp_merge_residue_gcomp_canonical_merge) = S ((S (gcomp_merge_index_gcomp_canonical_merge)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_merge_residue. r = ff_q_gcrt_gcomp_canonical_merge_residue * S ((S (gcomp_merge_index_gcomp_canonical_merge)) * s) + (gcomp_merge_residue_gcomp_canonical_merge))) -> (((exists ff_h_gcrt_gcomp_canonical_merge_modulus. ff_h_gcrt_gcomp_canonical_merge_modulus + S (gcomp_merge_modulus_gcomp_canonical_merge) = S ((S (gcomp_merge_index_gcomp_canonical_merge)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_merge_modulus. b = ff_q_gcrt_gcomp_canonical_merge_modulus * S ((S (gcomp_merge_index_gcomp_canonical_merge)) * c) + (gcomp_merge_modulus_gcomp_canonical_merge))) -> ((((exists hag_left_factor_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_lcm_gcomp_canonical_merge = gcomp_merge_gcd_gcomp_canonical_merge * hag_left_factor_gcomp_gcomp_canonical_merge_gcd) /\ (exists hag_right_factor_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_modulus_gcomp_canonical_merge = gcomp_merge_gcd_gcomp_canonical_merge * hag_right_factor_gcomp_gcomp_canonical_merge_gcd)) /\ forall hag_divisor_gcomp_gcomp_canonical_merge_gcd. (exists hag_common_left_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_lcm_gcomp_canonical_merge = hag_divisor_gcomp_gcomp_canonical_merge_gcd * hag_common_left_gcomp_gcomp_canonical_merge_gcd) -> (exists hag_common_right_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_modulus_gcomp_canonical_merge = hag_divisor_gcomp_gcomp_canonical_merge_gcd * hag_common_right_gcomp_gcomp_canonical_merge_gcd) -> exists hag_greatest_factor_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_gcd_gcomp_canonical_merge = hag_divisor_gcomp_gcomp_canonical_merge_gcd * hag_greatest_factor_gcomp_gcomp_canonical_merge_gcd)) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_merge_result hgcrt_mod_right_gcrt_gcomp_canonical_merge_result. gcomp_merge_solution_gcomp_canonical_merge + gcomp_merge_gcd_gcomp_canonical_merge * hgcrt_mod_left_gcrt_gcomp_canonical_merge_result = gcomp_merge_residue_gcomp_canonical_merge + gcomp_merge_gcd_gcomp_canonical_merge * hgcrt_mod_right_gcrt_gcomp_canonical_merge_result)) -> exists x M. ((((((forall gcrt_common_index_gcomp_canonical_chosen_lcm_own gcrt_common_modulus_gcomp_canonical_chosen_lcm_own. (exists ff_lt_gcrt_gcomp_canonical_chosen_lcm_own_bound. ff_lt_gcrt_gcomp_canonical_chosen_lcm_own_bound + S gcrt_common_index_gcomp_canonical_chosen_lcm_own = l) -> (((exists ff_h_gcrt_gcomp_canonical_chosen_lcm_own_entry. ff_h_gcrt_gcomp_canonical_chosen_lcm_own_entry + S (gcrt_common_modulus_gcomp_canonical_chosen_lcm_own) = S ((S (gcrt_common_index_gcomp_canonical_chosen_lcm_own)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_chosen_lcm_own_entry. b = ff_q_gcrt_gcomp_canonical_chosen_lcm_own_entry * S ((S (gcrt_common_index_gcomp_canonical_chosen_lcm_own)) * c) + (gcrt_common_modulus_gcomp_canonical_chosen_lcm_own))) -> exists gcrt_common_quotient_gcomp_canonical_chosen_lcm_own. M = gcrt_common_modulus_gcomp_canonical_chosen_lcm_own * gcrt_common_quotient_gcomp_canonical_chosen_lcm_own) /\ forall gcrt_lcm_common_gcomp_canonical_chosen_lcm. (forall gcrt_common_index_gcomp_canonical_chosen_lcm_other gcrt_common_modulus_gcomp_canonical_chosen_lcm_other. (exists ff_lt_gcrt_gcomp_canonical_chosen_lcm_other_bound. ff_lt_gcrt_gcomp_canonical_chosen_lcm_other_bound + S gcrt_common_index_gcomp_canonical_chosen_lcm_other = l) -> (((exists ff_h_gcrt_gcomp_canonical_chosen_lcm_other_entry. ff_h_gcrt_gcomp_canonical_chosen_lcm_other_entry + S (gcrt_common_modulus_gcomp_canonical_chosen_lcm_other) = S ((S (gcrt_common_index_gcomp_canonical_chosen_lcm_other)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_chosen_lcm_other_entry. b = ff_q_gcrt_gcomp_canonical_chosen_lcm_other_entry * S ((S (gcrt_common_index_gcomp_canonical_chosen_lcm_other)) * c) + (gcrt_common_modulus_gcomp_canonical_chosen_lcm_other))) -> exists gcrt_common_quotient_gcomp_canonical_chosen_lcm_other. gcrt_lcm_common_gcomp_canonical_chosen_lcm = gcrt_common_modulus_gcomp_canonical_chosen_lcm_other * gcrt_common_quotient_gcomp_canonical_chosen_lcm_other) -> exists gcrt_lcm_quotient_gcomp_canonical_chosen_lcm. gcrt_lcm_common_gcomp_canonical_chosen_lcm = M * gcrt_lcm_quotient_gcomp_canonical_chosen_lcm)) /\ ((exists ff_lt_gcrt_gcomp_canonical_chosen_bounded. ff_lt_gcrt_gcomp_canonical_chosen_bounded + S x = M) /\ (forall gcrt_solution_index_gcomp_canonical_chosen_solution gcrt_solution_residue_gcomp_canonical_chosen_solution gcrt_solution_modulus_gcomp_canonical_chosen_solution. (exists ff_lt_gcrt_gcomp_canonical_chosen_solution_bound. ff_lt_gcrt_gcomp_canonical_chosen_solution_bound + S gcrt_solution_index_gcomp_canonical_chosen_solution = l) -> (((exists ff_h_gcrt_gcomp_canonical_chosen_solution_residue. ff_h_gcrt_gcomp_canonical_chosen_solution_residue + S (gcrt_solution_residue_gcomp_canonical_chosen_solution) = S ((S (gcrt_solution_index_gcomp_canonical_chosen_solution)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_chosen_solution_residue. r = ff_q_gcrt_gcomp_canonical_chosen_solution_residue * S ((S (gcrt_solution_index_gcomp_canonical_chosen_solution)) * s) + (gcrt_solution_residue_gcomp_canonical_chosen_solution))) -> (((exists ff_h_gcrt_gcomp_canonical_chosen_solution_modulus. ff_h_gcrt_gcomp_canonical_chosen_solution_modulus + S (gcrt_solution_modulus_gcomp_canonical_chosen_solution) = S ((S (gcrt_solution_index_gcomp_canonical_chosen_solution)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_chosen_solution_modulus. b = ff_q_gcrt_gcomp_canonical_chosen_solution_modulus * S ((S (gcrt_solution_index_gcomp_canonical_chosen_solution)) * c) + (gcrt_solution_modulus_gcomp_canonical_chosen_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_chosen_solution_congruence hgcrt_mod_right_gcrt_gcomp_canonical_chosen_solution_congruence. x + gcrt_solution_modulus_gcomp_canonical_chosen_solution * hgcrt_mod_left_gcrt_gcomp_canonical_chosen_solution_congruence = gcrt_solution_residue_gcomp_canonical_chosen_solution + gcrt_solution_modulus_gcomp_canonical_chosen_solution * hgcrt_mod_right_gcrt_gcomp_canonical_chosen_solution_congruence))))) /\ forall y. (((((forall gcrt_common_index_gcomp_canonical_compared_lcm_own gcrt_common_modulus_gcomp_canonical_compared_lcm_own. (exists ff_lt_gcrt_gcomp_canonical_compared_lcm_own_bound. ff_lt_gcrt_gcomp_canonical_compared_lcm_own_bound + S gcrt_common_index_gcomp_canonical_compared_lcm_own = l) -> (((exists ff_h_gcrt_gcomp_canonical_compared_lcm_own_entry. ff_h_gcrt_gcomp_canonical_compared_lcm_own_entry + S (gcrt_common_modulus_gcomp_canonical_compared_lcm_own) = S ((S (gcrt_common_index_gcomp_canonical_compared_lcm_own)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_compared_lcm_own_entry. b = ff_q_gcrt_gcomp_canonical_compared_lcm_own_entry * S ((S (gcrt_common_index_gcomp_canonical_compared_lcm_own)) * c) + (gcrt_common_modulus_gcomp_canonical_compared_lcm_own))) -> exists gcrt_common_quotient_gcomp_canonical_compared_lcm_own. M = gcrt_common_modulus_gcomp_canonical_compared_lcm_own * gcrt_common_quotient_gcomp_canonical_compared_lcm_own) /\ forall gcrt_lcm_common_gcomp_canonical_compared_lcm. (forall gcrt_common_index_gcomp_canonical_compared_lcm_other gcrt_common_modulus_gcomp_canonical_compared_lcm_other. (exists ff_lt_gcrt_gcomp_canonical_compared_lcm_other_bound. ff_lt_gcrt_gcomp_canonical_compared_lcm_other_bound + S gcrt_common_index_gcomp_canonical_compared_lcm_other = l) -> (((exists ff_h_gcrt_gcomp_canonical_compared_lcm_other_entry. ff_h_gcrt_gcomp_canonical_compared_lcm_other_entry + S (gcrt_common_modulus_gcomp_canonical_compared_lcm_other) = S ((S (gcrt_common_index_gcomp_canonical_compared_lcm_other)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_compared_lcm_other_entry. b = ff_q_gcrt_gcomp_canonical_compared_lcm_other_entry * S ((S (gcrt_common_index_gcomp_canonical_compared_lcm_other)) * c) + (gcrt_common_modulus_gcomp_canonical_compared_lcm_other))) -> exists gcrt_common_quotient_gcomp_canonical_compared_lcm_other. gcrt_lcm_common_gcomp_canonical_compared_lcm = gcrt_common_modulus_gcomp_canonical_compared_lcm_other * gcrt_common_quotient_gcomp_canonical_compared_lcm_other) -> exists gcrt_lcm_quotient_gcomp_canonical_compared_lcm. gcrt_lcm_common_gcomp_canonical_compared_lcm = M * gcrt_lcm_quotient_gcomp_canonical_compared_lcm)) /\ ((exists ff_lt_gcrt_gcomp_canonical_compared_bounded. ff_lt_gcrt_gcomp_canonical_compared_bounded + S y = M) /\ (forall gcrt_solution_index_gcomp_canonical_compared_solution gcrt_solution_residue_gcomp_canonical_compared_solution gcrt_solution_modulus_gcomp_canonical_compared_solution. (exists ff_lt_gcrt_gcomp_canonical_compared_solution_bound. ff_lt_gcrt_gcomp_canonical_compared_solution_bound + S gcrt_solution_index_gcomp_canonical_compared_solution = l) -> (((exists ff_h_gcrt_gcomp_canonical_compared_solution_residue. ff_h_gcrt_gcomp_canonical_compared_solution_residue + S (gcrt_solution_residue_gcomp_canonical_compared_solution) = S ((S (gcrt_solution_index_gcomp_canonical_compared_solution)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_compared_solution_residue. r = ff_q_gcrt_gcomp_canonical_compared_solution_residue * S ((S (gcrt_solution_index_gcomp_canonical_compared_solution)) * s) + (gcrt_solution_residue_gcomp_canonical_compared_solution))) -> (((exists ff_h_gcrt_gcomp_canonical_compared_solution_modulus. ff_h_gcrt_gcomp_canonical_compared_solution_modulus + S (gcrt_solution_modulus_gcomp_canonical_compared_solution) = S ((S (gcrt_solution_index_gcomp_canonical_compared_solution)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_compared_solution_modulus. b = ff_q_gcrt_gcomp_canonical_compared_solution_modulus * S ((S (gcrt_solution_index_gcomp_canonical_compared_solution)) * c) + (gcrt_solution_modulus_gcomp_canonical_compared_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_compared_solution_congruence hgcrt_mod_right_gcrt_gcomp_canonical_compared_solution_congruence. y + gcrt_solution_modulus_gcomp_canonical_compared_solution * hgcrt_mod_left_gcrt_gcomp_canonical_compared_solution_congruence = gcrt_solution_residue_gcomp_canonical_compared_solution + gcrt_solution_modulus_gcomp_canonical_compared_solution * hgcrt_mod_right_gcrt_gcomp_canonical_compared_solution_congruence))))) -> y = x)

Complete unchanged native tactic proof

All 61 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

61 script commands · 15 reading checkpoints · 3 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 (2)
crt merge compatible prefix solution existscrt positive prefix lcm nonzero

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro l
  6. L6
    intro hpositive
  7. L7
    intro hmerge
02Establish hsolutionL8–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt merge compatible prefix solution exists.

  1. L8
    have hsolution : ∃ z. CRTPrefixSolution(r,s,b,c,l,z)Definitions: CRTPrefixSolutionOriginal native command in the exact edition
  2. L9
    specialize crt_merge_compatible_prefix_solution_exists r
  3. L10
    specialize crt_merge_compatible_prefix_solution_exists s
  4. L11
    specialize crt_merge_compatible_prefix_solution_exists b
  5. L12
    specialize crt_merge_compatible_prefix_solution_exists c
  6. L13
    specialize crt_merge_compatible_prefix_solution_exists l
  7. L14
    apply crt_merge_compatible_prefix_solution_exists
  8. L15
    exact hmerge
03Separate the logical casesL16–16

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

  1. L16
    cases hsolution
04Use earlier factsL17–19

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

  1. L17
    specialize crt_prefix_lcm_exists_unique b
  2. L18
    specialize crt_prefix_lcm_exists_unique c
  3. L19
    specialize crt_prefix_lcm_exists_unique l
05Separate the logical casesL20–21

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

  1. L20
    cases crt_prefix_lcm_exists_unique
  2. L21
    cases crt_prefix_lcm_exists_unique_witness
06Establish hnonzeroL22–31

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

  1. L22
    have hnonzero : ~(x1 = 0)
  2. L23
    specialize crt_positive_prefix_lcm_nonzero b
  3. L24
    specialize crt_positive_prefix_lcm_nonzero c
  4. L25
    specialize crt_positive_prefix_lcm_nonzero l
  5. L26
    specialize crt_positive_prefix_lcm_nonzero x1
  6. L27
    intro hz
  7. L28
    apply crt_positive_prefix_lcm_nonzero
  8. L29
    exact hpositive
  9. L30
    exact crt_prefix_lcm_exists_unique_witness_left
  10. L31
    exact hz
07Establish hcanonicalL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt prefix solution canonical remainder.

  1. L32
    have hcanonical : ∃ z. CRTCanonicalPrefixSolution(r,s,b,c,l,z,x1)Definitions: CRTCanonicalPrefixSolutionOriginal native command in the exact edition
  2. L33
    specialize crt_prefix_solution_canonical_remainder r
  3. L34
    specialize crt_prefix_solution_canonical_remainder s
  4. L35
    specialize crt_prefix_solution_canonical_remainder b
  5. L36
    specialize crt_prefix_solution_canonical_remainder c
  6. L37
    specialize crt_prefix_solution_canonical_remainder l
  7. L38
    specialize crt_prefix_solution_canonical_remainder x1
  8. L39
    specialize crt_prefix_solution_canonical_remainder x
  9. L40
    apply crt_prefix_solution_canonical_remainder
  10. L41
    exact hnonzero
08Use earlier factsL42–43

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

  1. L42
    exact crt_prefix_lcm_exists_unique_witness_left
  2. L43
    exact hsolution_witness
09Separate the logical casesL44–44

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

  1. L44
    cases hcanonical
10Construct an explicit witnessL45–46

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

  1. L45
    exists x2
  2. L46
    exists x1
11Separate the logical casesL47–47

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

  1. L47
    split
12Use earlier factsL48–48

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

  1. L48
    exact hcanonical_witness
13Fix variables and assumptionsL49–50

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

  1. L49
    intro y
  2. L50
    intro hy
14Use earlier factsL51–60

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

  1. L51
    specialize crt_canonical_prefix_solution_unique r
  2. L52
    specialize crt_canonical_prefix_solution_unique s
  3. L53
    specialize crt_canonical_prefix_solution_unique b
  4. L54
    specialize crt_canonical_prefix_solution_unique c
  5. L55
    specialize crt_canonical_prefix_solution_unique l
  6. L56
    specialize crt_canonical_prefix_solution_unique x1
  7. L57
    specialize crt_canonical_prefix_solution_unique x2
  8. L58
    specialize crt_canonical_prefix_solution_unique y
  9. L59
    apply crt_canonical_prefix_solution_unique
  10. L60
    exact hcanonical_witness
15Use earlier factsL61–61

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

  1. L61
    exact hy

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro hpositive
  7. 0007intro hmerge
  8. 0008have hsolution : exists z. (forall gcrt_solution_index_gcomp_canonical_old_solution gcrt_solution_residue_gcomp_canonical_old_solution gcrt_solution_modulus_gcomp_canonical_old_solution. (exists ff_lt_gcrt_gcomp_canonical_old_solution_bound. ff_lt_gcrt_gcomp_canonical_old_solution_bound + S gcrt_solution_index_gcomp_canonical_old_solution = l) -> (((exists ff_h_gcrt_gcomp_canonical_old_solution_residue. ff_h_gcrt_gcomp_canonical_old_solution_residue + S (gcrt_solution_residue_gcomp_canonical_old_solution) = S ((S (gcrt_solution_index_gcomp_canonical_old_solution)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_old_solution_residue. r = ff_q_gcrt_gcomp_canonical_old_solution_residue * S ((S (gcrt_solution_index_gcomp_canonical_old_solution)) * s) + (gcrt_solution_residue_gcomp_canonical_old_solution))) -> (((exists ff_h_gcrt_gcomp_canonical_old_solution_modulus. ff_h_gcrt_gcomp_canonical_old_solution_modulus + S (gcrt_solution_modulus_gcomp_canonical_old_solution) = S ((S (gcrt_solution_index_gcomp_canonical_old_solution)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_old_solution_modulus. b = ff_q_gcrt_gcomp_canonical_old_solution_modulus * S ((S (gcrt_solution_index_gcomp_canonical_old_solution)) * c) + (gcrt_solution_modulus_gcomp_canonical_old_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_old_solution_congruence hgcrt_mod_right_gcrt_gcomp_canonical_old_solution_congruence. z + gcrt_solution_modulus_gcomp_canonical_old_solution * hgcrt_mod_left_gcrt_gcomp_canonical_old_solution_congruence = gcrt_solution_residue_gcomp_canonical_old_solution + gcrt_solution_modulus_gcomp_canonical_old_solution * hgcrt_mod_right_gcrt_gcomp_canonical_old_solution_congruence))
  9. 0009specialize crt_merge_compatible_prefix_solution_exists r
  10. 0010specialize crt_merge_compatible_prefix_solution_exists s
  11. 0011specialize crt_merge_compatible_prefix_solution_exists b
  12. 0012specialize crt_merge_compatible_prefix_solution_exists c
  13. 0013specialize crt_merge_compatible_prefix_solution_exists l
  14. 0014apply crt_merge_compatible_prefix_solution_exists
  15. 0015exact hmerge
  16. 0016cases hsolution
  17. 0017specialize crt_prefix_lcm_exists_unique b
  18. 0018specialize crt_prefix_lcm_exists_unique c
  19. 0019specialize crt_prefix_lcm_exists_unique l
  20. 0020cases crt_prefix_lcm_exists_unique
  21. 0021cases crt_prefix_lcm_exists_unique_witness
  22. 0022have hnonzero : ~(x1 = 0)
  23. 0023specialize crt_positive_prefix_lcm_nonzero b
  24. 0024specialize crt_positive_prefix_lcm_nonzero c
  25. 0025specialize crt_positive_prefix_lcm_nonzero l
  26. 0026specialize crt_positive_prefix_lcm_nonzero x1
  27. 0027intro hz
  28. 0028apply crt_positive_prefix_lcm_nonzero
  29. 0029exact hpositive
  30. 0030exact crt_prefix_lcm_exists_unique_witness_left
  31. 0031exact hz
  32. 0032have hcanonical : exists z. (((((forall gcrt_common_index_gcomp_canonical_exists_actual_lcm_own gcrt_common_modulus_gcomp_canonical_exists_actual_lcm_own. (exists ff_lt_gcrt_gcomp_canonical_exists_actual_lcm_own_bound. ff_lt_gcrt_gcomp_canonical_exists_actual_lcm_own_bound + S gcrt_common_index_gcomp_canonical_exists_actual_lcm_own = l) -> (((exists ff_h_gcrt_gcomp_canonical_exists_actual_lcm_own_entry. ff_h_gcrt_gcomp_canonical_exists_actual_lcm_own_entry + S (gcrt_common_modulus_gcomp_canonical_exists_actual_lcm_own) = S ((S (gcrt_common_index_gcomp_canonical_exists_actual_lcm_own)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_exists_actual_lcm_own_entry. b = ff_q_gcrt_gcomp_canonical_exists_actual_lcm_own_entry * S ((S (gcrt_common_index_gcomp_canonical_exists_actual_lcm_own)) * c) + (gcrt_common_modulus_gcomp_canonical_exists_actual_lcm_own))) -> exists gcrt_common_quotient_gcomp_canonical_exists_actual_lcm_own. x1 = gcrt_common_modulus_gcomp_canonical_exists_actual_lcm_own * gcrt_common_quotient_gcomp_canonical_exists_actual_lcm_own) /\ forall gcrt_lcm_common_gcomp_canonical_exists_actual_lcm. (forall gcrt_common_index_gcomp_canonical_exists_actual_lcm_other gcrt_common_modulus_gcomp_canonical_exists_actual_lcm_other. (exists ff_lt_gcrt_gcomp_canonical_exists_actual_lcm_other_bound. ff_lt_gcrt_gcomp_canonical_exists_actual_lcm_other_bound + S gcrt_common_index_gcomp_canonical_exists_actual_lcm_other = l) -> (((exists ff_h_gcrt_gcomp_canonical_exists_actual_lcm_other_entry. ff_h_gcrt_gcomp_canonical_exists_actual_lcm_other_entry + S (gcrt_common_modulus_gcomp_canonical_exists_actual_lcm_other) = S ((S (gcrt_common_index_gcomp_canonical_exists_actual_lcm_other)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_exists_actual_lcm_other_entry. b = ff_q_gcrt_gcomp_canonical_exists_actual_lcm_other_entry * S ((S (gcrt_common_index_gcomp_canonical_exists_actual_lcm_other)) * c) + (gcrt_common_modulus_gcomp_canonical_exists_actual_lcm_other))) -> exists gcrt_common_quotient_gcomp_canonical_exists_actual_lcm_other. gcrt_lcm_common_gcomp_canonical_exists_actual_lcm = gcrt_common_modulus_gcomp_canonical_exists_actual_lcm_other * gcrt_common_quotient_gcomp_canonical_exists_actual_lcm_other) -> exists gcrt_lcm_quotient_gcomp_canonical_exists_actual_lcm. gcrt_lcm_common_gcomp_canonical_exists_actual_lcm = x1 * gcrt_lcm_quotient_gcomp_canonical_exists_actual_lcm)) /\ ((exists ff_lt_gcrt_gcomp_canonical_exists_actual_bounded. ff_lt_gcrt_gcomp_canonical_exists_actual_bounded + S z = x1) /\ (forall gcrt_solution_index_gcomp_canonical_exists_actual_solution gcrt_solution_residue_gcomp_canonical_exists_actual_solution gcrt_solution_modulus_gcomp_canonical_exists_actual_solution. (exists ff_lt_gcrt_gcomp_canonical_exists_actual_solution_bound. ff_lt_gcrt_gcomp_canonical_exists_actual_solution_bound + S gcrt_solution_index_gcomp_canonical_exists_actual_solution = l) -> (((exists ff_h_gcrt_gcomp_canonical_exists_actual_solution_residue. ff_h_gcrt_gcomp_canonical_exists_actual_solution_residue + S (gcrt_solution_residue_gcomp_canonical_exists_actual_solution) = S ((S (gcrt_solution_index_gcomp_canonical_exists_actual_solution)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_exists_actual_solution_residue. r = ff_q_gcrt_gcomp_canonical_exists_actual_solution_residue * S ((S (gcrt_solution_index_gcomp_canonical_exists_actual_solution)) * s) + (gcrt_solution_residue_gcomp_canonical_exists_actual_solution))) -> (((exists ff_h_gcrt_gcomp_canonical_exists_actual_solution_modulus. ff_h_gcrt_gcomp_canonical_exists_actual_solution_modulus + S (gcrt_solution_modulus_gcomp_canonical_exists_actual_solution) = S ((S (gcrt_solution_index_gcomp_canonical_exists_actual_solution)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_exists_actual_solution_modulus. b = ff_q_gcrt_gcomp_canonical_exists_actual_solution_modulus * S ((S (gcrt_solution_index_gcomp_canonical_exists_actual_solution)) * c) + (gcrt_solution_modulus_gcomp_canonical_exists_actual_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_exists_actual_solution_congruence hgcrt_mod_right_gcrt_gcomp_canonical_exists_actual_solution_congruence. z + gcrt_solution_modulus_gcomp_canonical_exists_actual_solution * hgcrt_mod_left_gcrt_gcomp_canonical_exists_actual_solution_congruence = gcrt_solution_residue_gcomp_canonical_exists_actual_solution + gcrt_solution_modulus_gcomp_canonical_exists_actual_solution * hgcrt_mod_right_gcrt_gcomp_canonical_exists_actual_solution_congruence)))))
  33. 0033specialize crt_prefix_solution_canonical_remainder r
  34. 0034specialize crt_prefix_solution_canonical_remainder s
  35. 0035specialize crt_prefix_solution_canonical_remainder b
  36. 0036specialize crt_prefix_solution_canonical_remainder c
  37. 0037specialize crt_prefix_solution_canonical_remainder l
  38. 0038specialize crt_prefix_solution_canonical_remainder x1
  39. 0039specialize crt_prefix_solution_canonical_remainder x
  40. 0040apply crt_prefix_solution_canonical_remainder
  41. 0041exact hnonzero
  42. 0042exact crt_prefix_lcm_exists_unique_witness_left
  43. 0043exact hsolution_witness
  44. 0044cases hcanonical
  45. 0045exists x2
  46. 0046exists x1
  47. 0047split
  48. 0048exact hcanonical_witness
  49. 0049intro y
  50. 0050intro hy
  51. 0051specialize crt_canonical_prefix_solution_unique r
  52. 0052specialize crt_canonical_prefix_solution_unique s
  53. 0053specialize crt_canonical_prefix_solution_unique b
  54. 0054specialize crt_canonical_prefix_solution_unique c
  55. 0055specialize crt_canonical_prefix_solution_unique l
  56. 0056specialize crt_canonical_prefix_solution_unique x1
  57. 0057specialize crt_canonical_prefix_solution_unique x2
  58. 0058specialize crt_canonical_prefix_solution_unique y
  59. 0059apply crt_canonical_prefix_solution_unique
  60. 0060exact hcanonical_witness
  61. 0061exact hy