FC0018

crt_positive_normalized_prefix_iff_canonical

For positive modulus lists, zero-safe normalization is exactly the historical strict canonical definition, not a weaker replacement.

Alpha v34 checked-use · first admitted v27 · 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.

All finite lists are included, even the empty list and zero moduli. A positive LCM gives x<M; at zero LCM congruence is exact equality and normalization deliberately does not require the impossible x<0.

Exact theorem in conservative defined notation

∀ r. ∀ s. ∀ b. ∀ c. ∀ l. ∀ x. ∀ M. CRTPositiveModuliPrefix(b,c,l) → (CRTNormalizedPrefixSolution(r,s,b,c,l,x,M) → CRTPrefixLCM(b,c,l,M) ∧ (Lt(x,M) ∧ CRTPrefixSolution(r,s,b,c,l,x))) ∧ (CRTPrefixLCM(b,c,l,M) ∧ (Lt(x,M) ∧ CRTPrefixSolution(r,s,b,c,l,x)) → CRTNormalizedPrefixSolution(r,s,b,c,l,x,M))

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

Definition DAG

CRTPositiveModuliPrefix(b,c,l) · 1CRTPrefixSolution(r,s,b,c,l,x) · 2CRTPrefixLCM(b,c,l,M) · 2CRTNormalizedPrefixSolution(r,s,b,c,l,x,M) · 2Lt(a,b) · 2

Actual proof prerequisites

crt_positive_prefix_lcm_nonzero · checked external prerequisitecrt_canonical_prefix_solution_implies_normalized
Original expanded first-order statement 
forall r s b c l x M. (forall gcrt_positive_index_gfull_normalized_positive_hypothesis gcrt_positive_value_gfull_normalized_positive_hypothesis. (exists ff_lt_gcrt_gfull_normalized_positive_hypothesis_bound. ff_lt_gcrt_gfull_normalized_positive_hypothesis_bound + S gcrt_positive_index_gfull_normalized_positive_hypothesis = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_hypothesis_entry. ff_h_gcrt_gfull_normalized_positive_hypothesis_entry + S (gcrt_positive_value_gfull_normalized_positive_hypothesis) = S ((S (gcrt_positive_index_gfull_normalized_positive_hypothesis)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_hypothesis_entry. b = ff_q_gcrt_gfull_normalized_positive_hypothesis_entry * S ((S (gcrt_positive_index_gfull_normalized_positive_hypothesis)) * c) + (gcrt_positive_value_gfull_normalized_positive_hypothesis))) -> ~(gcrt_positive_value_gfull_normalized_positive_hypothesis = 0)) -> (((((((forall gcrt_common_index_gfull_normalized_positive_forward_lcm_own gcrt_common_modulus_gfull_normalized_positive_forward_lcm_own. (exists ff_lt_gcrt_gfull_normalized_positive_forward_lcm_own_bound. ff_lt_gcrt_gfull_normalized_positive_forward_lcm_own_bound + S gcrt_common_index_gfull_normalized_positive_forward_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_forward_lcm_own_entry. ff_h_gcrt_gfull_normalized_positive_forward_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_positive_forward_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_positive_forward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_forward_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_positive_forward_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_positive_forward_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_positive_forward_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_positive_forward_lcm_own. M = gcrt_common_modulus_gfull_normalized_positive_forward_lcm_own * gcrt_common_quotient_gfull_normalized_positive_forward_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_positive_forward_lcm. (forall gcrt_common_index_gfull_normalized_positive_forward_lcm_other gcrt_common_modulus_gfull_normalized_positive_forward_lcm_other. (exists ff_lt_gcrt_gfull_normalized_positive_forward_lcm_other_bound. ff_lt_gcrt_gfull_normalized_positive_forward_lcm_other_bound + S gcrt_common_index_gfull_normalized_positive_forward_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_forward_lcm_other_entry. ff_h_gcrt_gfull_normalized_positive_forward_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_positive_forward_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_positive_forward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_forward_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_positive_forward_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_positive_forward_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_positive_forward_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_positive_forward_lcm_other. gcrt_lcm_common_gfull_normalized_positive_forward_lcm = gcrt_common_modulus_gfull_normalized_positive_forward_lcm_other * gcrt_common_quotient_gfull_normalized_positive_forward_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_positive_forward_lcm. gcrt_lcm_common_gfull_normalized_positive_forward_lcm = M * gcrt_lcm_quotient_gfull_normalized_positive_forward_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_positive_forward_bound. ff_lt_gcrt_gfull_normalized_positive_forward_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_positive_forward_solution gcrt_solution_residue_gfull_normalized_positive_forward_solution gcrt_solution_modulus_gfull_normalized_positive_forward_solution. (exists ff_lt_gcrt_gfull_normalized_positive_forward_solution_bound. ff_lt_gcrt_gfull_normalized_positive_forward_solution_bound + S gcrt_solution_index_gfull_normalized_positive_forward_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_forward_solution_residue. ff_h_gcrt_gfull_normalized_positive_forward_solution_residue + S (gcrt_solution_residue_gfull_normalized_positive_forward_solution) = S ((S (gcrt_solution_index_gfull_normalized_positive_forward_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_positive_forward_solution_residue. r = ff_q_gcrt_gfull_normalized_positive_forward_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_positive_forward_solution)) * s) + (gcrt_solution_residue_gfull_normalized_positive_forward_solution))) -> (((exists ff_h_gcrt_gfull_normalized_positive_forward_solution_modulus. ff_h_gcrt_gfull_normalized_positive_forward_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_positive_forward_solution) = S ((S (gcrt_solution_index_gfull_normalized_positive_forward_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_forward_solution_modulus. b = ff_q_gcrt_gfull_normalized_positive_forward_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_positive_forward_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_positive_forward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_positive_forward_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_positive_forward_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_positive_forward_solution * hgcrt_mod_left_gcrt_gfull_normalized_positive_forward_solution_congruence = gcrt_solution_residue_gfull_normalized_positive_forward_solution + gcrt_solution_modulus_gfull_normalized_positive_forward_solution * hgcrt_mod_right_gcrt_gfull_normalized_positive_forward_solution_congruence))))) -> (((((forall gcrt_common_index_gfull_canonical_positive_forward_lcm_own gcrt_common_modulus_gfull_canonical_positive_forward_lcm_own. (exists ff_lt_gcrt_gfull_canonical_positive_forward_lcm_own_bound. ff_lt_gcrt_gfull_canonical_positive_forward_lcm_own_bound + S gcrt_common_index_gfull_canonical_positive_forward_lcm_own = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_forward_lcm_own_entry. ff_h_gcrt_gfull_canonical_positive_forward_lcm_own_entry + S (gcrt_common_modulus_gfull_canonical_positive_forward_lcm_own) = S ((S (gcrt_common_index_gfull_canonical_positive_forward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_forward_lcm_own_entry. b = ff_q_gcrt_gfull_canonical_positive_forward_lcm_own_entry * S ((S (gcrt_common_index_gfull_canonical_positive_forward_lcm_own)) * c) + (gcrt_common_modulus_gfull_canonical_positive_forward_lcm_own))) -> exists gcrt_common_quotient_gfull_canonical_positive_forward_lcm_own. M = gcrt_common_modulus_gfull_canonical_positive_forward_lcm_own * gcrt_common_quotient_gfull_canonical_positive_forward_lcm_own) /\ forall gcrt_lcm_common_gfull_canonical_positive_forward_lcm. (forall gcrt_common_index_gfull_canonical_positive_forward_lcm_other gcrt_common_modulus_gfull_canonical_positive_forward_lcm_other. (exists ff_lt_gcrt_gfull_canonical_positive_forward_lcm_other_bound. ff_lt_gcrt_gfull_canonical_positive_forward_lcm_other_bound + S gcrt_common_index_gfull_canonical_positive_forward_lcm_other = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_forward_lcm_other_entry. ff_h_gcrt_gfull_canonical_positive_forward_lcm_other_entry + S (gcrt_common_modulus_gfull_canonical_positive_forward_lcm_other) = S ((S (gcrt_common_index_gfull_canonical_positive_forward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_forward_lcm_other_entry. b = ff_q_gcrt_gfull_canonical_positive_forward_lcm_other_entry * S ((S (gcrt_common_index_gfull_canonical_positive_forward_lcm_other)) * c) + (gcrt_common_modulus_gfull_canonical_positive_forward_lcm_other))) -> exists gcrt_common_quotient_gfull_canonical_positive_forward_lcm_other. gcrt_lcm_common_gfull_canonical_positive_forward_lcm = gcrt_common_modulus_gfull_canonical_positive_forward_lcm_other * gcrt_common_quotient_gfull_canonical_positive_forward_lcm_other) -> exists gcrt_lcm_quotient_gfull_canonical_positive_forward_lcm. gcrt_lcm_common_gfull_canonical_positive_forward_lcm = M * gcrt_lcm_quotient_gfull_canonical_positive_forward_lcm)) /\ ((exists ff_lt_gcrt_gfull_canonical_positive_forward_bounded. ff_lt_gcrt_gfull_canonical_positive_forward_bounded + S x = M) /\ (forall gcrt_solution_index_gfull_canonical_positive_forward_solution gcrt_solution_residue_gfull_canonical_positive_forward_solution gcrt_solution_modulus_gfull_canonical_positive_forward_solution. (exists ff_lt_gcrt_gfull_canonical_positive_forward_solution_bound. ff_lt_gcrt_gfull_canonical_positive_forward_solution_bound + S gcrt_solution_index_gfull_canonical_positive_forward_solution = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_forward_solution_residue. ff_h_gcrt_gfull_canonical_positive_forward_solution_residue + S (gcrt_solution_residue_gfull_canonical_positive_forward_solution) = S ((S (gcrt_solution_index_gfull_canonical_positive_forward_solution)) * s)) /\ exists ff_q_gcrt_gfull_canonical_positive_forward_solution_residue. r = ff_q_gcrt_gfull_canonical_positive_forward_solution_residue * S ((S (gcrt_solution_index_gfull_canonical_positive_forward_solution)) * s) + (gcrt_solution_residue_gfull_canonical_positive_forward_solution))) -> (((exists ff_h_gcrt_gfull_canonical_positive_forward_solution_modulus. ff_h_gcrt_gfull_canonical_positive_forward_solution_modulus + S (gcrt_solution_modulus_gfull_canonical_positive_forward_solution) = S ((S (gcrt_solution_index_gfull_canonical_positive_forward_solution)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_forward_solution_modulus. b = ff_q_gcrt_gfull_canonical_positive_forward_solution_modulus * S ((S (gcrt_solution_index_gfull_canonical_positive_forward_solution)) * c) + (gcrt_solution_modulus_gfull_canonical_positive_forward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_canonical_positive_forward_solution_congruence hgcrt_mod_right_gcrt_gfull_canonical_positive_forward_solution_congruence. x + gcrt_solution_modulus_gfull_canonical_positive_forward_solution * hgcrt_mod_left_gcrt_gfull_canonical_positive_forward_solution_congruence = gcrt_solution_residue_gfull_canonical_positive_forward_solution + gcrt_solution_modulus_gfull_canonical_positive_forward_solution * hgcrt_mod_right_gcrt_gfull_canonical_positive_forward_solution_congruence)))))) /\ ((((((forall gcrt_common_index_gfull_canonical_positive_backward_lcm_own gcrt_common_modulus_gfull_canonical_positive_backward_lcm_own. (exists ff_lt_gcrt_gfull_canonical_positive_backward_lcm_own_bound. ff_lt_gcrt_gfull_canonical_positive_backward_lcm_own_bound + S gcrt_common_index_gfull_canonical_positive_backward_lcm_own = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_backward_lcm_own_entry. ff_h_gcrt_gfull_canonical_positive_backward_lcm_own_entry + S (gcrt_common_modulus_gfull_canonical_positive_backward_lcm_own) = S ((S (gcrt_common_index_gfull_canonical_positive_backward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_backward_lcm_own_entry. b = ff_q_gcrt_gfull_canonical_positive_backward_lcm_own_entry * S ((S (gcrt_common_index_gfull_canonical_positive_backward_lcm_own)) * c) + (gcrt_common_modulus_gfull_canonical_positive_backward_lcm_own))) -> exists gcrt_common_quotient_gfull_canonical_positive_backward_lcm_own. M = gcrt_common_modulus_gfull_canonical_positive_backward_lcm_own * gcrt_common_quotient_gfull_canonical_positive_backward_lcm_own) /\ forall gcrt_lcm_common_gfull_canonical_positive_backward_lcm. (forall gcrt_common_index_gfull_canonical_positive_backward_lcm_other gcrt_common_modulus_gfull_canonical_positive_backward_lcm_other. (exists ff_lt_gcrt_gfull_canonical_positive_backward_lcm_other_bound. ff_lt_gcrt_gfull_canonical_positive_backward_lcm_other_bound + S gcrt_common_index_gfull_canonical_positive_backward_lcm_other = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_backward_lcm_other_entry. ff_h_gcrt_gfull_canonical_positive_backward_lcm_other_entry + S (gcrt_common_modulus_gfull_canonical_positive_backward_lcm_other) = S ((S (gcrt_common_index_gfull_canonical_positive_backward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_backward_lcm_other_entry. b = ff_q_gcrt_gfull_canonical_positive_backward_lcm_other_entry * S ((S (gcrt_common_index_gfull_canonical_positive_backward_lcm_other)) * c) + (gcrt_common_modulus_gfull_canonical_positive_backward_lcm_other))) -> exists gcrt_common_quotient_gfull_canonical_positive_backward_lcm_other. gcrt_lcm_common_gfull_canonical_positive_backward_lcm = gcrt_common_modulus_gfull_canonical_positive_backward_lcm_other * gcrt_common_quotient_gfull_canonical_positive_backward_lcm_other) -> exists gcrt_lcm_quotient_gfull_canonical_positive_backward_lcm. gcrt_lcm_common_gfull_canonical_positive_backward_lcm = M * gcrt_lcm_quotient_gfull_canonical_positive_backward_lcm)) /\ ((exists ff_lt_gcrt_gfull_canonical_positive_backward_bounded. ff_lt_gcrt_gfull_canonical_positive_backward_bounded + S x = M) /\ (forall gcrt_solution_index_gfull_canonical_positive_backward_solution gcrt_solution_residue_gfull_canonical_positive_backward_solution gcrt_solution_modulus_gfull_canonical_positive_backward_solution. (exists ff_lt_gcrt_gfull_canonical_positive_backward_solution_bound. ff_lt_gcrt_gfull_canonical_positive_backward_solution_bound + S gcrt_solution_index_gfull_canonical_positive_backward_solution = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_backward_solution_residue. ff_h_gcrt_gfull_canonical_positive_backward_solution_residue + S (gcrt_solution_residue_gfull_canonical_positive_backward_solution) = S ((S (gcrt_solution_index_gfull_canonical_positive_backward_solution)) * s)) /\ exists ff_q_gcrt_gfull_canonical_positive_backward_solution_residue. r = ff_q_gcrt_gfull_canonical_positive_backward_solution_residue * S ((S (gcrt_solution_index_gfull_canonical_positive_backward_solution)) * s) + (gcrt_solution_residue_gfull_canonical_positive_backward_solution))) -> (((exists ff_h_gcrt_gfull_canonical_positive_backward_solution_modulus. ff_h_gcrt_gfull_canonical_positive_backward_solution_modulus + S (gcrt_solution_modulus_gfull_canonical_positive_backward_solution) = S ((S (gcrt_solution_index_gfull_canonical_positive_backward_solution)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_backward_solution_modulus. b = ff_q_gcrt_gfull_canonical_positive_backward_solution_modulus * S ((S (gcrt_solution_index_gfull_canonical_positive_backward_solution)) * c) + (gcrt_solution_modulus_gfull_canonical_positive_backward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_canonical_positive_backward_solution_congruence hgcrt_mod_right_gcrt_gfull_canonical_positive_backward_solution_congruence. x + gcrt_solution_modulus_gfull_canonical_positive_backward_solution * hgcrt_mod_left_gcrt_gfull_canonical_positive_backward_solution_congruence = gcrt_solution_residue_gfull_canonical_positive_backward_solution + gcrt_solution_modulus_gfull_canonical_positive_backward_solution * hgcrt_mod_right_gcrt_gfull_canonical_positive_backward_solution_congruence))))) -> (((((forall gcrt_common_index_gfull_normalized_positive_backward_lcm_own gcrt_common_modulus_gfull_normalized_positive_backward_lcm_own. (exists ff_lt_gcrt_gfull_normalized_positive_backward_lcm_own_bound. ff_lt_gcrt_gfull_normalized_positive_backward_lcm_own_bound + S gcrt_common_index_gfull_normalized_positive_backward_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_backward_lcm_own_entry. ff_h_gcrt_gfull_normalized_positive_backward_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_positive_backward_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_positive_backward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_backward_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_positive_backward_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_positive_backward_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_positive_backward_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_positive_backward_lcm_own. M = gcrt_common_modulus_gfull_normalized_positive_backward_lcm_own * gcrt_common_quotient_gfull_normalized_positive_backward_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_positive_backward_lcm. (forall gcrt_common_index_gfull_normalized_positive_backward_lcm_other gcrt_common_modulus_gfull_normalized_positive_backward_lcm_other. (exists ff_lt_gcrt_gfull_normalized_positive_backward_lcm_other_bound. ff_lt_gcrt_gfull_normalized_positive_backward_lcm_other_bound + S gcrt_common_index_gfull_normalized_positive_backward_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_backward_lcm_other_entry. ff_h_gcrt_gfull_normalized_positive_backward_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_positive_backward_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_positive_backward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_backward_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_positive_backward_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_positive_backward_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_positive_backward_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_positive_backward_lcm_other. gcrt_lcm_common_gfull_normalized_positive_backward_lcm = gcrt_common_modulus_gfull_normalized_positive_backward_lcm_other * gcrt_common_quotient_gfull_normalized_positive_backward_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_positive_backward_lcm. gcrt_lcm_common_gfull_normalized_positive_backward_lcm = M * gcrt_lcm_quotient_gfull_normalized_positive_backward_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_positive_backward_bound. ff_lt_gcrt_gfull_normalized_positive_backward_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_positive_backward_solution gcrt_solution_residue_gfull_normalized_positive_backward_solution gcrt_solution_modulus_gfull_normalized_positive_backward_solution. (exists ff_lt_gcrt_gfull_normalized_positive_backward_solution_bound. ff_lt_gcrt_gfull_normalized_positive_backward_solution_bound + S gcrt_solution_index_gfull_normalized_positive_backward_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_backward_solution_residue. ff_h_gcrt_gfull_normalized_positive_backward_solution_residue + S (gcrt_solution_residue_gfull_normalized_positive_backward_solution) = S ((S (gcrt_solution_index_gfull_normalized_positive_backward_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_positive_backward_solution_residue. r = ff_q_gcrt_gfull_normalized_positive_backward_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_positive_backward_solution)) * s) + (gcrt_solution_residue_gfull_normalized_positive_backward_solution))) -> (((exists ff_h_gcrt_gfull_normalized_positive_backward_solution_modulus. ff_h_gcrt_gfull_normalized_positive_backward_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_positive_backward_solution) = S ((S (gcrt_solution_index_gfull_normalized_positive_backward_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_backward_solution_modulus. b = ff_q_gcrt_gfull_normalized_positive_backward_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_positive_backward_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_positive_backward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_positive_backward_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_positive_backward_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_positive_backward_solution * hgcrt_mod_left_gcrt_gfull_normalized_positive_backward_solution_congruence = gcrt_solution_residue_gfull_normalized_positive_backward_solution + gcrt_solution_modulus_gfull_normalized_positive_backward_solution * hgcrt_mod_right_gcrt_gfull_normalized_positive_backward_solution_congruence)))))))

Complete tactic proof in conservative notation

All 37 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

37 script commands · 9 reading checkpoints · 0 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 (1)
crt canonical prefix solution implies normalized
01Fix variables and assumptionsL1–8

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 x
  7. L7
    intro M
  8. L8
    intro hp
02Separate the logical casesL9–9

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

  1. L9
    split
03Fix variables and assumptionsL10–10

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

  1. L10
    intro hn
04Separate the logical casesL11–13

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

  1. L11
    cases hn
  2. L12
    cases hn_right
  3. L13
    split
05Use earlier factsL14–14

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

  1. L14
    exact hn_left
06Separate the logical casesL15–17

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

  1. L15
    split
  2. L16
    cases hn_right_left
  3. L17
    exfalso
07Use earlier factsL18–27

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

  1. L18
    specialize crt_positive_prefix_lcm_nonzero b
  2. L19
    specialize crt_positive_prefix_lcm_nonzero c
  3. L20
    specialize crt_positive_prefix_lcm_nonzero l
  4. L21
    specialize crt_positive_prefix_lcm_nonzero M
  5. L22
    apply crt_positive_prefix_lcm_nonzero
  6. L23
    exact hp
  7. L24
    exact hn_left
  8. L25
    exact hn_right_left_left
  9. L26
    exact hn_right_left_right
  10. L27
    exact hn_right_right
08Fix variables and assumptionsL28–28

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

  1. L28
    intro hc
09Use earlier factsL29–37

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

  1. L29
    specialize crt_canonical_prefix_solution_implies_normalized r
  2. L30
    specialize crt_canonical_prefix_solution_implies_normalized s
  3. L31
    specialize crt_canonical_prefix_solution_implies_normalized b
  4. L32
    specialize crt_canonical_prefix_solution_implies_normalized c
  5. L33
    specialize crt_canonical_prefix_solution_implies_normalized l
  6. L34
    specialize crt_canonical_prefix_solution_implies_normalized x
  7. L35
    specialize crt_canonical_prefix_solution_implies_normalized M
  8. L36
    apply crt_canonical_prefix_solution_implies_normalized
  9. L37
    exact hc

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro x
  7. 0007intro M
  8. 0008intro hp
  9. 0009split
  10. 0010intro hn
  11. 0011cases hn
  12. 0012cases hn_right
  13. 0013split
  14. 0014exact hn_left
  15. 0015split
  16. 0016cases hn_right_left
  17. 0017exfalso
  18. 0018specialize crt_positive_prefix_lcm_nonzero b
  19. 0019specialize crt_positive_prefix_lcm_nonzero c
  20. 0020specialize crt_positive_prefix_lcm_nonzero l
  21. 0021specialize crt_positive_prefix_lcm_nonzero M
  22. 0022apply crt_positive_prefix_lcm_nonzero
  23. 0023exact hp
  24. 0024exact hn_left
  25. 0025exact hn_right_left_left
  26. 0026exact hn_right_left_right
  27. 0027exact hn_right_right
  28. 0028intro hc
  29. 0029specialize crt_canonical_prefix_solution_implies_normalized r
  30. 0030specialize crt_canonical_prefix_solution_implies_normalized s
  31. 0031specialize crt_canonical_prefix_solution_implies_normalized b
  32. 0032specialize crt_canonical_prefix_solution_implies_normalized c
  33. 0033specialize crt_canonical_prefix_solution_implies_normalized l
  34. 0034specialize crt_canonical_prefix_solution_implies_normalized x
  35. 0035specialize crt_canonical_prefix_solution_implies_normalized M
  36. 0036apply crt_canonical_prefix_solution_implies_normalized
  37. 0037exact hc