GC0018

crt_pairwise_compatible_dominating_last_canonical_exists_unique

Every positive pairwise gcd-compatible successor list whose last modulus dominates all predecessors has its exact list LCM and a unique strictly bounded simultaneous solution without assuming pairwise coprimality or the stronger merge invariant.

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. ∀ a. ∀ M. CRTPositiveModuliPrefix(b,c,S l) → CRTPairwiseCompatiblePrefix(r,s,b,c,S l) → Beta(r,s,l,a) → Beta(b,c,l,M) → (∀ x. ∀ y. Lt(x,l) → Beta(b,c,x,y) → Dvd(y,M)) → ∃ x. ∃ y. CRTCanonicalPrefixSolution(r,s,b,c,S l,x,y) ∧ (∀ z. CRTCanonicalPrefixSolution(r,s,b,c,S l,z,y) → z = x)

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

Definition DAG

Beta(b,c,i,x) · 3CRTPositiveModuliPrefix(b,c,l) · 1CRTCanonicalPrefixSolution(r,s,b,c,l,x,M) · 2CRTPairwiseCompatiblePrefix(r,s,b,c,l) · 1Lt(a,b) · 1Dvd(d,n) · 1

Actual proof prerequisites

crt_pairwise_compatible_dominating_last_solutioncrt_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 a M. (forall gcrt_positive_index_dominating_canonical_positive gcrt_positive_value_dominating_canonical_positive. (exists ff_lt_gcrt_dominating_canonical_positive_bound. ff_lt_gcrt_dominating_canonical_positive_bound + S gcrt_positive_index_dominating_canonical_positive = S l) -> (((exists ff_h_gcrt_dominating_canonical_positive_entry. ff_h_gcrt_dominating_canonical_positive_entry + S (gcrt_positive_value_dominating_canonical_positive) = S ((S (gcrt_positive_index_dominating_canonical_positive)) * c)) /\ exists ff_q_gcrt_dominating_canonical_positive_entry. b = ff_q_gcrt_dominating_canonical_positive_entry * S ((S (gcrt_positive_index_dominating_canonical_positive)) * c) + (gcrt_positive_value_dominating_canonical_positive))) -> ~(gcrt_positive_value_dominating_canonical_positive = 0)) -> (forall gcomp_left_index_dominating_canonical_pairs gcomp_right_index_dominating_canonical_pairs gcomp_left_residue_dominating_canonical_pairs gcomp_right_residue_dominating_canonical_pairs gcomp_left_modulus_dominating_canonical_pairs gcomp_right_modulus_dominating_canonical_pairs gcomp_pair_gcd_dominating_canonical_pairs. (exists ff_lt_gcrt_dominating_canonical_pairs_left_bound. ff_lt_gcrt_dominating_canonical_pairs_left_bound + S gcomp_left_index_dominating_canonical_pairs = S l) -> (exists ff_lt_gcrt_dominating_canonical_pairs_right_bound. ff_lt_gcrt_dominating_canonical_pairs_right_bound + S gcomp_right_index_dominating_canonical_pairs = S l) -> (((exists ff_h_gcrt_dominating_canonical_pairs_left_residue. ff_h_gcrt_dominating_canonical_pairs_left_residue + S (gcomp_left_residue_dominating_canonical_pairs) = S ((S (gcomp_left_index_dominating_canonical_pairs)) * s)) /\ exists ff_q_gcrt_dominating_canonical_pairs_left_residue. r = ff_q_gcrt_dominating_canonical_pairs_left_residue * S ((S (gcomp_left_index_dominating_canonical_pairs)) * s) + (gcomp_left_residue_dominating_canonical_pairs))) -> (((exists ff_h_gcrt_dominating_canonical_pairs_right_residue. ff_h_gcrt_dominating_canonical_pairs_right_residue + S (gcomp_right_residue_dominating_canonical_pairs) = S ((S (gcomp_right_index_dominating_canonical_pairs)) * s)) /\ exists ff_q_gcrt_dominating_canonical_pairs_right_residue. r = ff_q_gcrt_dominating_canonical_pairs_right_residue * S ((S (gcomp_right_index_dominating_canonical_pairs)) * s) + (gcomp_right_residue_dominating_canonical_pairs))) -> (((exists ff_h_gcrt_dominating_canonical_pairs_left_modulus. ff_h_gcrt_dominating_canonical_pairs_left_modulus + S (gcomp_left_modulus_dominating_canonical_pairs) = S ((S (gcomp_left_index_dominating_canonical_pairs)) * c)) /\ exists ff_q_gcrt_dominating_canonical_pairs_left_modulus. b = ff_q_gcrt_dominating_canonical_pairs_left_modulus * S ((S (gcomp_left_index_dominating_canonical_pairs)) * c) + (gcomp_left_modulus_dominating_canonical_pairs))) -> (((exists ff_h_gcrt_dominating_canonical_pairs_right_modulus. ff_h_gcrt_dominating_canonical_pairs_right_modulus + S (gcomp_right_modulus_dominating_canonical_pairs) = S ((S (gcomp_right_index_dominating_canonical_pairs)) * c)) /\ exists ff_q_gcrt_dominating_canonical_pairs_right_modulus. b = ff_q_gcrt_dominating_canonical_pairs_right_modulus * S ((S (gcomp_right_index_dominating_canonical_pairs)) * c) + (gcomp_right_modulus_dominating_canonical_pairs))) -> ((((exists hag_left_factor_gcomp_dominating_canonical_pairs_gcd. gcomp_left_modulus_dominating_canonical_pairs = gcomp_pair_gcd_dominating_canonical_pairs * hag_left_factor_gcomp_dominating_canonical_pairs_gcd) /\ (exists hag_right_factor_gcomp_dominating_canonical_pairs_gcd. gcomp_right_modulus_dominating_canonical_pairs = gcomp_pair_gcd_dominating_canonical_pairs * hag_right_factor_gcomp_dominating_canonical_pairs_gcd)) /\ forall hag_divisor_gcomp_dominating_canonical_pairs_gcd. (exists hag_common_left_gcomp_dominating_canonical_pairs_gcd. gcomp_left_modulus_dominating_canonical_pairs = hag_divisor_gcomp_dominating_canonical_pairs_gcd * hag_common_left_gcomp_dominating_canonical_pairs_gcd) -> (exists hag_common_right_gcomp_dominating_canonical_pairs_gcd. gcomp_right_modulus_dominating_canonical_pairs = hag_divisor_gcomp_dominating_canonical_pairs_gcd * hag_common_right_gcomp_dominating_canonical_pairs_gcd) -> exists hag_greatest_factor_gcomp_dominating_canonical_pairs_gcd. gcomp_pair_gcd_dominating_canonical_pairs = hag_divisor_gcomp_dominating_canonical_pairs_gcd * hag_greatest_factor_gcomp_dominating_canonical_pairs_gcd)) -> (exists hgcrt_mod_left_gcrt_dominating_canonical_pairs_result hgcrt_mod_right_gcrt_dominating_canonical_pairs_result. gcomp_left_residue_dominating_canonical_pairs + gcomp_pair_gcd_dominating_canonical_pairs * hgcrt_mod_left_gcrt_dominating_canonical_pairs_result = gcomp_right_residue_dominating_canonical_pairs + gcomp_pair_gcd_dominating_canonical_pairs * hgcrt_mod_right_gcrt_dominating_canonical_pairs_result)) -> (((exists ff_h_gcrt_dominating_canonical_residue. ff_h_gcrt_dominating_canonical_residue + S (a) = S ((S (l)) * s)) /\ exists ff_q_gcrt_dominating_canonical_residue. r = ff_q_gcrt_dominating_canonical_residue * S ((S (l)) * s) + (a))) -> (((exists ff_h_gcrt_dominating_canonical_modulus. ff_h_gcrt_dominating_canonical_modulus + S (M) = S ((S (l)) * c)) /\ exists ff_q_gcrt_dominating_canonical_modulus. b = ff_q_gcrt_dominating_canonical_modulus * S ((S (l)) * c) + (M))) -> (forall gcrt_common_index_dominating_canonical_common gcrt_common_modulus_dominating_canonical_common. (exists ff_lt_gcrt_dominating_canonical_common_bound. ff_lt_gcrt_dominating_canonical_common_bound + S gcrt_common_index_dominating_canonical_common = l) -> (((exists ff_h_gcrt_dominating_canonical_common_entry. ff_h_gcrt_dominating_canonical_common_entry + S (gcrt_common_modulus_dominating_canonical_common) = S ((S (gcrt_common_index_dominating_canonical_common)) * c)) /\ exists ff_q_gcrt_dominating_canonical_common_entry. b = ff_q_gcrt_dominating_canonical_common_entry * S ((S (gcrt_common_index_dominating_canonical_common)) * c) + (gcrt_common_modulus_dominating_canonical_common))) -> exists gcrt_common_quotient_dominating_canonical_common. M = gcrt_common_modulus_dominating_canonical_common * gcrt_common_quotient_dominating_canonical_common) -> exists x L. ((((((forall gcrt_common_index_dominating_canonical_chosen_lcm_own gcrt_common_modulus_dominating_canonical_chosen_lcm_own. (exists ff_lt_gcrt_dominating_canonical_chosen_lcm_own_bound. ff_lt_gcrt_dominating_canonical_chosen_lcm_own_bound + S gcrt_common_index_dominating_canonical_chosen_lcm_own = S l) -> (((exists ff_h_gcrt_dominating_canonical_chosen_lcm_own_entry. ff_h_gcrt_dominating_canonical_chosen_lcm_own_entry + S (gcrt_common_modulus_dominating_canonical_chosen_lcm_own) = S ((S (gcrt_common_index_dominating_canonical_chosen_lcm_own)) * c)) /\ exists ff_q_gcrt_dominating_canonical_chosen_lcm_own_entry. b = ff_q_gcrt_dominating_canonical_chosen_lcm_own_entry * S ((S (gcrt_common_index_dominating_canonical_chosen_lcm_own)) * c) + (gcrt_common_modulus_dominating_canonical_chosen_lcm_own))) -> exists gcrt_common_quotient_dominating_canonical_chosen_lcm_own. L = gcrt_common_modulus_dominating_canonical_chosen_lcm_own * gcrt_common_quotient_dominating_canonical_chosen_lcm_own) /\ forall gcrt_lcm_common_dominating_canonical_chosen_lcm. (forall gcrt_common_index_dominating_canonical_chosen_lcm_other gcrt_common_modulus_dominating_canonical_chosen_lcm_other. (exists ff_lt_gcrt_dominating_canonical_chosen_lcm_other_bound. ff_lt_gcrt_dominating_canonical_chosen_lcm_other_bound + S gcrt_common_index_dominating_canonical_chosen_lcm_other = S l) -> (((exists ff_h_gcrt_dominating_canonical_chosen_lcm_other_entry. ff_h_gcrt_dominating_canonical_chosen_lcm_other_entry + S (gcrt_common_modulus_dominating_canonical_chosen_lcm_other) = S ((S (gcrt_common_index_dominating_canonical_chosen_lcm_other)) * c)) /\ exists ff_q_gcrt_dominating_canonical_chosen_lcm_other_entry. b = ff_q_gcrt_dominating_canonical_chosen_lcm_other_entry * S ((S (gcrt_common_index_dominating_canonical_chosen_lcm_other)) * c) + (gcrt_common_modulus_dominating_canonical_chosen_lcm_other))) -> exists gcrt_common_quotient_dominating_canonical_chosen_lcm_other. gcrt_lcm_common_dominating_canonical_chosen_lcm = gcrt_common_modulus_dominating_canonical_chosen_lcm_other * gcrt_common_quotient_dominating_canonical_chosen_lcm_other) -> exists gcrt_lcm_quotient_dominating_canonical_chosen_lcm. gcrt_lcm_common_dominating_canonical_chosen_lcm = L * gcrt_lcm_quotient_dominating_canonical_chosen_lcm)) /\ ((exists ff_lt_gcrt_dominating_canonical_chosen_bounded. ff_lt_gcrt_dominating_canonical_chosen_bounded + S x = L) /\ (forall gcrt_solution_index_dominating_canonical_chosen_solution gcrt_solution_residue_dominating_canonical_chosen_solution gcrt_solution_modulus_dominating_canonical_chosen_solution. (exists ff_lt_gcrt_dominating_canonical_chosen_solution_bound. ff_lt_gcrt_dominating_canonical_chosen_solution_bound + S gcrt_solution_index_dominating_canonical_chosen_solution = S l) -> (((exists ff_h_gcrt_dominating_canonical_chosen_solution_residue. ff_h_gcrt_dominating_canonical_chosen_solution_residue + S (gcrt_solution_residue_dominating_canonical_chosen_solution) = S ((S (gcrt_solution_index_dominating_canonical_chosen_solution)) * s)) /\ exists ff_q_gcrt_dominating_canonical_chosen_solution_residue. r = ff_q_gcrt_dominating_canonical_chosen_solution_residue * S ((S (gcrt_solution_index_dominating_canonical_chosen_solution)) * s) + (gcrt_solution_residue_dominating_canonical_chosen_solution))) -> (((exists ff_h_gcrt_dominating_canonical_chosen_solution_modulus. ff_h_gcrt_dominating_canonical_chosen_solution_modulus + S (gcrt_solution_modulus_dominating_canonical_chosen_solution) = S ((S (gcrt_solution_index_dominating_canonical_chosen_solution)) * c)) /\ exists ff_q_gcrt_dominating_canonical_chosen_solution_modulus. b = ff_q_gcrt_dominating_canonical_chosen_solution_modulus * S ((S (gcrt_solution_index_dominating_canonical_chosen_solution)) * c) + (gcrt_solution_modulus_dominating_canonical_chosen_solution))) -> (exists hgcrt_mod_left_gcrt_dominating_canonical_chosen_solution_congruence hgcrt_mod_right_gcrt_dominating_canonical_chosen_solution_congruence. x + gcrt_solution_modulus_dominating_canonical_chosen_solution * hgcrt_mod_left_gcrt_dominating_canonical_chosen_solution_congruence = gcrt_solution_residue_dominating_canonical_chosen_solution + gcrt_solution_modulus_dominating_canonical_chosen_solution * hgcrt_mod_right_gcrt_dominating_canonical_chosen_solution_congruence))))) /\ forall y. (((((forall gcrt_common_index_dominating_canonical_compared_lcm_own gcrt_common_modulus_dominating_canonical_compared_lcm_own. (exists ff_lt_gcrt_dominating_canonical_compared_lcm_own_bound. ff_lt_gcrt_dominating_canonical_compared_lcm_own_bound + S gcrt_common_index_dominating_canonical_compared_lcm_own = S l) -> (((exists ff_h_gcrt_dominating_canonical_compared_lcm_own_entry. ff_h_gcrt_dominating_canonical_compared_lcm_own_entry + S (gcrt_common_modulus_dominating_canonical_compared_lcm_own) = S ((S (gcrt_common_index_dominating_canonical_compared_lcm_own)) * c)) /\ exists ff_q_gcrt_dominating_canonical_compared_lcm_own_entry. b = ff_q_gcrt_dominating_canonical_compared_lcm_own_entry * S ((S (gcrt_common_index_dominating_canonical_compared_lcm_own)) * c) + (gcrt_common_modulus_dominating_canonical_compared_lcm_own))) -> exists gcrt_common_quotient_dominating_canonical_compared_lcm_own. L = gcrt_common_modulus_dominating_canonical_compared_lcm_own * gcrt_common_quotient_dominating_canonical_compared_lcm_own) /\ forall gcrt_lcm_common_dominating_canonical_compared_lcm. (forall gcrt_common_index_dominating_canonical_compared_lcm_other gcrt_common_modulus_dominating_canonical_compared_lcm_other. (exists ff_lt_gcrt_dominating_canonical_compared_lcm_other_bound. ff_lt_gcrt_dominating_canonical_compared_lcm_other_bound + S gcrt_common_index_dominating_canonical_compared_lcm_other = S l) -> (((exists ff_h_gcrt_dominating_canonical_compared_lcm_other_entry. ff_h_gcrt_dominating_canonical_compared_lcm_other_entry + S (gcrt_common_modulus_dominating_canonical_compared_lcm_other) = S ((S (gcrt_common_index_dominating_canonical_compared_lcm_other)) * c)) /\ exists ff_q_gcrt_dominating_canonical_compared_lcm_other_entry. b = ff_q_gcrt_dominating_canonical_compared_lcm_other_entry * S ((S (gcrt_common_index_dominating_canonical_compared_lcm_other)) * c) + (gcrt_common_modulus_dominating_canonical_compared_lcm_other))) -> exists gcrt_common_quotient_dominating_canonical_compared_lcm_other. gcrt_lcm_common_dominating_canonical_compared_lcm = gcrt_common_modulus_dominating_canonical_compared_lcm_other * gcrt_common_quotient_dominating_canonical_compared_lcm_other) -> exists gcrt_lcm_quotient_dominating_canonical_compared_lcm. gcrt_lcm_common_dominating_canonical_compared_lcm = L * gcrt_lcm_quotient_dominating_canonical_compared_lcm)) /\ ((exists ff_lt_gcrt_dominating_canonical_compared_bounded. ff_lt_gcrt_dominating_canonical_compared_bounded + S y = L) /\ (forall gcrt_solution_index_dominating_canonical_compared_solution gcrt_solution_residue_dominating_canonical_compared_solution gcrt_solution_modulus_dominating_canonical_compared_solution. (exists ff_lt_gcrt_dominating_canonical_compared_solution_bound. ff_lt_gcrt_dominating_canonical_compared_solution_bound + S gcrt_solution_index_dominating_canonical_compared_solution = S l) -> (((exists ff_h_gcrt_dominating_canonical_compared_solution_residue. ff_h_gcrt_dominating_canonical_compared_solution_residue + S (gcrt_solution_residue_dominating_canonical_compared_solution) = S ((S (gcrt_solution_index_dominating_canonical_compared_solution)) * s)) /\ exists ff_q_gcrt_dominating_canonical_compared_solution_residue. r = ff_q_gcrt_dominating_canonical_compared_solution_residue * S ((S (gcrt_solution_index_dominating_canonical_compared_solution)) * s) + (gcrt_solution_residue_dominating_canonical_compared_solution))) -> (((exists ff_h_gcrt_dominating_canonical_compared_solution_modulus. ff_h_gcrt_dominating_canonical_compared_solution_modulus + S (gcrt_solution_modulus_dominating_canonical_compared_solution) = S ((S (gcrt_solution_index_dominating_canonical_compared_solution)) * c)) /\ exists ff_q_gcrt_dominating_canonical_compared_solution_modulus. b = ff_q_gcrt_dominating_canonical_compared_solution_modulus * S ((S (gcrt_solution_index_dominating_canonical_compared_solution)) * c) + (gcrt_solution_modulus_dominating_canonical_compared_solution))) -> (exists hgcrt_mod_left_gcrt_dominating_canonical_compared_solution_congruence hgcrt_mod_right_gcrt_dominating_canonical_compared_solution_congruence. y + gcrt_solution_modulus_dominating_canonical_compared_solution * hgcrt_mod_left_gcrt_dominating_canonical_compared_solution_congruence = gcrt_solution_residue_dominating_canonical_compared_solution + gcrt_solution_modulus_dominating_canonical_compared_solution * hgcrt_mod_right_gcrt_dominating_canonical_compared_solution_congruence))))) -> y = x)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

68 script commands · 15 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 (2)
crt positive prefix lcm nonzerocrt pairwise compatible dominating last solution

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–10

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 a
  7. L7
    intro M
  8. L8
    intro hpositive
  9. L9
    intro hpairs
  10. L10
    intro ha
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hM
  2. L12
    intro hcommon
03Use earlier factsL13–15

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

  1. L13
    specialize crt_prefix_lcm_exists_unique b
  2. L14
    specialize crt_prefix_lcm_exists_unique c
  3. L15
    specialize crt_prefix_lcm_exists_unique (S l)
04Separate the logical casesL16–17

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

  1. L16
    cases crt_prefix_lcm_exists_unique
  2. L17
    cases crt_prefix_lcm_exists_unique_witness
05Establish hnonzeroL18–27

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

  1. L18
    have hnonzero : ~(x = 0)
  2. L19
    specialize crt_positive_prefix_lcm_nonzero b
  3. L20
    specialize crt_positive_prefix_lcm_nonzero c
  4. L21
    specialize crt_positive_prefix_lcm_nonzero (S l)
  5. L22
    specialize crt_positive_prefix_lcm_nonzero x
  6. L23
    intro hz
  7. L24
    apply crt_positive_prefix_lcm_nonzero
  8. L25
    exact hpositive
  9. L26
    exact crt_prefix_lcm_exists_unique_witness_left
  10. L27
    exact hz
06Establish hcanonicalL28–37

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

  1. L28
    have hcanonical : ∃ z. CRTCanonicalPrefixSolution(r,s,b,c,S l,z,x)Definitions: CRTCanonicalPrefixSolutionOriginal native command in the exact edition
  2. L29
    specialize crt_prefix_solution_canonical_remainder r
  3. L30
    specialize crt_prefix_solution_canonical_remainder s
  4. L31
    specialize crt_prefix_solution_canonical_remainder b
  5. L32
    specialize crt_prefix_solution_canonical_remainder c
  6. L33
    specialize crt_prefix_solution_canonical_remainder (S l)
  7. L34
    specialize crt_prefix_solution_canonical_remainder x
  8. L35
    specialize crt_prefix_solution_canonical_remainder a
  9. L36
    apply crt_prefix_solution_canonical_remainder
  10. L37
    exact hnonzero
07Use earlier factsL38–47

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

  1. L38
    exact crt_prefix_lcm_exists_unique_witness_left
  2. L39
    specialize crt_pairwise_compatible_dominating_last_solution r
  3. L40
    specialize crt_pairwise_compatible_dominating_last_solution s
  4. L41
    specialize crt_pairwise_compatible_dominating_last_solution b
  5. L42
    specialize crt_pairwise_compatible_dominating_last_solution c
  6. L43
    specialize crt_pairwise_compatible_dominating_last_solution l
  7. L44
    specialize crt_pairwise_compatible_dominating_last_solution a
  8. L45
    specialize crt_pairwise_compatible_dominating_last_solution M
  9. L46
    apply crt_pairwise_compatible_dominating_last_solution
  10. L47
    exact hpairs
08Use earlier factsL48–50

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

  1. L48
    exact ha
  2. L49
    exact hM
  3. L50
    exact hcommon
09Separate the logical casesL51–51

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

  1. L51
    cases hcanonical
10Construct an explicit witnessL52–53

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

  1. L52
    exists x1
  2. L53
    exists x
11Separate the logical casesL54–54

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

  1. L54
    split
12Use earlier factsL55–55

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

  1. L55
    exact hcanonical_witness
13Fix variables and assumptionsL56–57

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

  1. L56
    intro y
  2. L57
    intro hy
14Use earlier factsL58–67

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

  1. L58
    specialize crt_canonical_prefix_solution_unique r
  2. L59
    specialize crt_canonical_prefix_solution_unique s
  3. L60
    specialize crt_canonical_prefix_solution_unique b
  4. L61
    specialize crt_canonical_prefix_solution_unique c
  5. L62
    specialize crt_canonical_prefix_solution_unique (S l)
  6. L63
    specialize crt_canonical_prefix_solution_unique x
  7. L64
    specialize crt_canonical_prefix_solution_unique x1
  8. L65
    specialize crt_canonical_prefix_solution_unique y
  9. L66
    apply crt_canonical_prefix_solution_unique
  10. L67
    exact hcanonical_witness
15Use earlier factsL68–68

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

  1. L68
    exact hy

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro a
  7. 0007intro M
  8. 0008intro hpositive
  9. 0009intro hpairs
  10. 0010intro ha
  11. 0011intro hM
  12. 0012intro hcommon
  13. 0013specialize crt_prefix_lcm_exists_unique b
  14. 0014specialize crt_prefix_lcm_exists_unique c
  15. 0015specialize crt_prefix_lcm_exists_unique (S l)
  16. 0016cases crt_prefix_lcm_exists_unique
  17. 0017cases crt_prefix_lcm_exists_unique_witness
  18. 0018have hnonzero : ~(x = 0)
  19. 0019specialize crt_positive_prefix_lcm_nonzero b
  20. 0020specialize crt_positive_prefix_lcm_nonzero c
  21. 0021specialize crt_positive_prefix_lcm_nonzero (S l)
  22. 0022specialize crt_positive_prefix_lcm_nonzero x
  23. 0023intro hz
  24. 0024apply crt_positive_prefix_lcm_nonzero
  25. 0025exact hpositive
  26. 0026exact crt_prefix_lcm_exists_unique_witness_left
  27. 0027exact hz
  28. 0028have hcanonical : exists z. (((((forall gcrt_common_index_dominating_canonical_actual_lcm_own gcrt_common_modulus_dominating_canonical_actual_lcm_own. (exists ff_lt_gcrt_dominating_canonical_actual_lcm_own_bound. ff_lt_gcrt_dominating_canonical_actual_lcm_own_bound + S gcrt_common_index_dominating_canonical_actual_lcm_own = S l) -> (((exists ff_h_gcrt_dominating_canonical_actual_lcm_own_entry. ff_h_gcrt_dominating_canonical_actual_lcm_own_entry + S (gcrt_common_modulus_dominating_canonical_actual_lcm_own) = S ((S (gcrt_common_index_dominating_canonical_actual_lcm_own)) * c)) /\ exists ff_q_gcrt_dominating_canonical_actual_lcm_own_entry. b = ff_q_gcrt_dominating_canonical_actual_lcm_own_entry * S ((S (gcrt_common_index_dominating_canonical_actual_lcm_own)) * c) + (gcrt_common_modulus_dominating_canonical_actual_lcm_own))) -> exists gcrt_common_quotient_dominating_canonical_actual_lcm_own. x = gcrt_common_modulus_dominating_canonical_actual_lcm_own * gcrt_common_quotient_dominating_canonical_actual_lcm_own) /\ forall gcrt_lcm_common_dominating_canonical_actual_lcm. (forall gcrt_common_index_dominating_canonical_actual_lcm_other gcrt_common_modulus_dominating_canonical_actual_lcm_other. (exists ff_lt_gcrt_dominating_canonical_actual_lcm_other_bound. ff_lt_gcrt_dominating_canonical_actual_lcm_other_bound + S gcrt_common_index_dominating_canonical_actual_lcm_other = S l) -> (((exists ff_h_gcrt_dominating_canonical_actual_lcm_other_entry. ff_h_gcrt_dominating_canonical_actual_lcm_other_entry + S (gcrt_common_modulus_dominating_canonical_actual_lcm_other) = S ((S (gcrt_common_index_dominating_canonical_actual_lcm_other)) * c)) /\ exists ff_q_gcrt_dominating_canonical_actual_lcm_other_entry. b = ff_q_gcrt_dominating_canonical_actual_lcm_other_entry * S ((S (gcrt_common_index_dominating_canonical_actual_lcm_other)) * c) + (gcrt_common_modulus_dominating_canonical_actual_lcm_other))) -> exists gcrt_common_quotient_dominating_canonical_actual_lcm_other. gcrt_lcm_common_dominating_canonical_actual_lcm = gcrt_common_modulus_dominating_canonical_actual_lcm_other * gcrt_common_quotient_dominating_canonical_actual_lcm_other) -> exists gcrt_lcm_quotient_dominating_canonical_actual_lcm. gcrt_lcm_common_dominating_canonical_actual_lcm = x * gcrt_lcm_quotient_dominating_canonical_actual_lcm)) /\ ((exists ff_lt_gcrt_dominating_canonical_actual_bounded. ff_lt_gcrt_dominating_canonical_actual_bounded + S z = x) /\ (forall gcrt_solution_index_dominating_canonical_actual_solution gcrt_solution_residue_dominating_canonical_actual_solution gcrt_solution_modulus_dominating_canonical_actual_solution. (exists ff_lt_gcrt_dominating_canonical_actual_solution_bound. ff_lt_gcrt_dominating_canonical_actual_solution_bound + S gcrt_solution_index_dominating_canonical_actual_solution = S l) -> (((exists ff_h_gcrt_dominating_canonical_actual_solution_residue. ff_h_gcrt_dominating_canonical_actual_solution_residue + S (gcrt_solution_residue_dominating_canonical_actual_solution) = S ((S (gcrt_solution_index_dominating_canonical_actual_solution)) * s)) /\ exists ff_q_gcrt_dominating_canonical_actual_solution_residue. r = ff_q_gcrt_dominating_canonical_actual_solution_residue * S ((S (gcrt_solution_index_dominating_canonical_actual_solution)) * s) + (gcrt_solution_residue_dominating_canonical_actual_solution))) -> (((exists ff_h_gcrt_dominating_canonical_actual_solution_modulus. ff_h_gcrt_dominating_canonical_actual_solution_modulus + S (gcrt_solution_modulus_dominating_canonical_actual_solution) = S ((S (gcrt_solution_index_dominating_canonical_actual_solution)) * c)) /\ exists ff_q_gcrt_dominating_canonical_actual_solution_modulus. b = ff_q_gcrt_dominating_canonical_actual_solution_modulus * S ((S (gcrt_solution_index_dominating_canonical_actual_solution)) * c) + (gcrt_solution_modulus_dominating_canonical_actual_solution))) -> (exists hgcrt_mod_left_gcrt_dominating_canonical_actual_solution_congruence hgcrt_mod_right_gcrt_dominating_canonical_actual_solution_congruence. z + gcrt_solution_modulus_dominating_canonical_actual_solution * hgcrt_mod_left_gcrt_dominating_canonical_actual_solution_congruence = gcrt_solution_residue_dominating_canonical_actual_solution + gcrt_solution_modulus_dominating_canonical_actual_solution * hgcrt_mod_right_gcrt_dominating_canonical_actual_solution_congruence)))))
  29. 0029specialize crt_prefix_solution_canonical_remainder r
  30. 0030specialize crt_prefix_solution_canonical_remainder s
  31. 0031specialize crt_prefix_solution_canonical_remainder b
  32. 0032specialize crt_prefix_solution_canonical_remainder c
  33. 0033specialize crt_prefix_solution_canonical_remainder (S l)
  34. 0034specialize crt_prefix_solution_canonical_remainder x
  35. 0035specialize crt_prefix_solution_canonical_remainder a
  36. 0036apply crt_prefix_solution_canonical_remainder
  37. 0037exact hnonzero
  38. 0038exact crt_prefix_lcm_exists_unique_witness_left
  39. 0039specialize crt_pairwise_compatible_dominating_last_solution r
  40. 0040specialize crt_pairwise_compatible_dominating_last_solution s
  41. 0041specialize crt_pairwise_compatible_dominating_last_solution b
  42. 0042specialize crt_pairwise_compatible_dominating_last_solution c
  43. 0043specialize crt_pairwise_compatible_dominating_last_solution l
  44. 0044specialize crt_pairwise_compatible_dominating_last_solution a
  45. 0045specialize crt_pairwise_compatible_dominating_last_solution M
  46. 0046apply crt_pairwise_compatible_dominating_last_solution
  47. 0047exact hpairs
  48. 0048exact ha
  49. 0049exact hM
  50. 0050exact hcommon
  51. 0051cases hcanonical
  52. 0052exists x1
  53. 0053exists x
  54. 0054split
  55. 0055exact hcanonical_witness
  56. 0056intro y
  57. 0057intro hy
  58. 0058specialize crt_canonical_prefix_solution_unique r
  59. 0059specialize crt_canonical_prefix_solution_unique s
  60. 0060specialize crt_canonical_prefix_solution_unique b
  61. 0061specialize crt_canonical_prefix_solution_unique c
  62. 0062specialize crt_canonical_prefix_solution_unique (S l)
  63. 0063specialize crt_canonical_prefix_solution_unique x
  64. 0064specialize crt_canonical_prefix_solution_unique x1
  65. 0065specialize crt_canonical_prefix_solution_unique y
  66. 0066apply crt_canonical_prefix_solution_unique
  67. 0067exact hcanonical_witness
  68. 0068exact hy