CR0012

crt_pairwise_coprime_prefix_product_coprime_last

The actual predecessor product is coprime to the final modulus of any pairwise-coprime list.

Alpha v34 checked-use · first admitted v24 · 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 for finite positive pairwise-coprime systems and exact LCM solution classes. G011 is now closed in the separate Alpha-v27 generalized-crt branch for arbitrary pairwise-compatible systems, including noncoprime moduli. Full G011 proof · Alpha v27

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. ∀ x. ∀ m. CRTPairwiseCoprimePrefix(b,c,S l) → (∃ y. ∃ z. Beta(y,z,0,1) ∧ (Beta(y,z,l,x) ∧ (∀ n. Lt(n,l) → ∃ k. ∃ i. ∃ j. Beta(b,c,n,k) ∧ (Beta(y,z,n,i) ∧ (Beta(y,z,S n,j) ∧ j = i · k))))) → Beta(b,c,l,m) → Coprime(x,m)

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

Definition DAG

Beta(b,c,i,x) · 6CRTPairwiseCoprimePrefix(b,c,l) · 1Lt(a,b) · 1Coprime(a,b) · 1

Actual proof prerequisites

beta_product_pointwise_coprime · checked external prerequisitecrt_pairwise_coprime_prefix_last
Original expanded first-order statement 
forall b c l x m. (forall bpr_left_index_gcrt_product_last_pairs bpr_right_index_gcrt_product_last_pairs bpr_left_value_gcrt_product_last_pairs bpr_right_value_gcrt_product_last_pairs. (exists bpr_gap_gcrt_product_last_pairs_left_bound. bpr_gap_gcrt_product_last_pairs_left_bound + S (bpr_left_index_gcrt_product_last_pairs) = S l) -> (exists bpr_gap_gcrt_product_last_pairs_right_bound. bpr_gap_gcrt_product_last_pairs_right_bound + S (bpr_right_index_gcrt_product_last_pairs) = S l) -> (((exists bpr_height_gcrt_product_last_pairs_left_at. bpr_height_gcrt_product_last_pairs_left_at + S (bpr_left_value_gcrt_product_last_pairs) = S ((S (bpr_left_index_gcrt_product_last_pairs)) * c)) /\ exists bpr_quotient_gcrt_product_last_pairs_left_at. b = bpr_quotient_gcrt_product_last_pairs_left_at * S ((S (bpr_left_index_gcrt_product_last_pairs)) * c) + (bpr_left_value_gcrt_product_last_pairs))) -> (((exists bpr_height_gcrt_product_last_pairs_right_at. bpr_height_gcrt_product_last_pairs_right_at + S (bpr_right_value_gcrt_product_last_pairs) = S ((S (bpr_right_index_gcrt_product_last_pairs)) * c)) /\ exists bpr_quotient_gcrt_product_last_pairs_right_at. b = bpr_quotient_gcrt_product_last_pairs_right_at * S ((S (bpr_right_index_gcrt_product_last_pairs)) * c) + (bpr_right_value_gcrt_product_last_pairs))) -> ~(bpr_left_index_gcrt_product_last_pairs = bpr_right_index_gcrt_product_last_pairs) -> (forall bpr_coprime_divisor_gcrt_product_last_pairs_coprime. (exists bpr_coprime_left_factor_gcrt_product_last_pairs_coprime. bpr_left_value_gcrt_product_last_pairs = bpr_coprime_divisor_gcrt_product_last_pairs_coprime * bpr_coprime_left_factor_gcrt_product_last_pairs_coprime) -> (exists bpr_coprime_right_factor_gcrt_product_last_pairs_coprime. bpr_right_value_gcrt_product_last_pairs = bpr_coprime_divisor_gcrt_product_last_pairs_coprime * bpr_coprime_right_factor_gcrt_product_last_pairs_coprime) -> bpr_coprime_divisor_gcrt_product_last_pairs_coprime = 1)) -> (exists ff_u_gcrt_product_last_prefix ff_v_gcrt_product_last_prefix. ((((exists ff_h_gcrt_product_last_prefix_start. ff_h_gcrt_product_last_prefix_start + S (1) = S ((S (0)) * ff_v_gcrt_product_last_prefix)) /\ exists ff_q_gcrt_product_last_prefix_start. ff_u_gcrt_product_last_prefix = ff_q_gcrt_product_last_prefix_start * S ((S (0)) * ff_v_gcrt_product_last_prefix) + (1))) /\ ((((exists ff_h_gcrt_product_last_prefix_terminal. ff_h_gcrt_product_last_prefix_terminal + S (x) = S ((S (l)) * ff_v_gcrt_product_last_prefix)) /\ exists ff_q_gcrt_product_last_prefix_terminal. ff_u_gcrt_product_last_prefix = ff_q_gcrt_product_last_prefix_terminal * S ((S (l)) * ff_v_gcrt_product_last_prefix) + (x))) /\ forall ff_i_gcrt_product_last_prefix. (exists ff_lt_gcrt_product_last_prefix_bound. ff_lt_gcrt_product_last_prefix_bound + S ff_i_gcrt_product_last_prefix = l) -> exists ff_p_gcrt_product_last_prefix ff_r_gcrt_product_last_prefix ff_s_gcrt_product_last_prefix. ((((exists ff_h_gcrt_product_last_prefix_factor. ff_h_gcrt_product_last_prefix_factor + S (ff_p_gcrt_product_last_prefix) = S ((S (ff_i_gcrt_product_last_prefix)) * c)) /\ exists ff_q_gcrt_product_last_prefix_factor. b = ff_q_gcrt_product_last_prefix_factor * S ((S (ff_i_gcrt_product_last_prefix)) * c) + (ff_p_gcrt_product_last_prefix))) /\ ((((exists ff_h_gcrt_product_last_prefix_partial. ff_h_gcrt_product_last_prefix_partial + S (ff_r_gcrt_product_last_prefix) = S ((S (ff_i_gcrt_product_last_prefix)) * ff_v_gcrt_product_last_prefix)) /\ exists ff_q_gcrt_product_last_prefix_partial. ff_u_gcrt_product_last_prefix = ff_q_gcrt_product_last_prefix_partial * S ((S (ff_i_gcrt_product_last_prefix)) * ff_v_gcrt_product_last_prefix) + (ff_r_gcrt_product_last_prefix))) /\ ((((exists ff_h_gcrt_product_last_prefix_successor. ff_h_gcrt_product_last_prefix_successor + S (ff_s_gcrt_product_last_prefix) = S ((S (S ff_i_gcrt_product_last_prefix)) * ff_v_gcrt_product_last_prefix)) /\ exists ff_q_gcrt_product_last_prefix_successor. ff_u_gcrt_product_last_prefix = ff_q_gcrt_product_last_prefix_successor * S ((S (S ff_i_gcrt_product_last_prefix)) * ff_v_gcrt_product_last_prefix) + (ff_s_gcrt_product_last_prefix))) /\ ff_s_gcrt_product_last_prefix = ff_r_gcrt_product_last_prefix * ff_p_gcrt_product_last_prefix)))))) -> (((exists ff_h_gcrt_product_last_entry. ff_h_gcrt_product_last_entry + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_product_last_entry. b = ff_q_gcrt_product_last_entry * S ((S (l)) * c) + (m))) -> (forall frp_divisor_gcrt_product_last_coprime. (exists frp_left_factor_gcrt_product_last_coprime. x = frp_divisor_gcrt_product_last_coprime * frp_left_factor_gcrt_product_last_coprime) -> (exists frp_right_factor_gcrt_product_last_coprime. m = frp_divisor_gcrt_product_last_coprime * frp_right_factor_gcrt_product_last_coprime) -> frp_divisor_gcrt_product_last_coprime = 1)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

30 script commands · 5 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 pairwise coprime prefix last
01Fix variables and assumptionsL1–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro x
  5. L5
    intro m
  6. L6
    intro hpairs
  7. L7
    intro hproduct
  8. L8
    intro hm
02Use earlier factsL9–14

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

  1. L9
    specialize beta_product_pointwise_coprime m
  2. L10
    specialize beta_product_pointwise_coprime b
  3. L11
    specialize beta_product_pointwise_coprime c
  4. L12
    specialize beta_product_pointwise_coprime l
  5. L13
    specialize beta_product_pointwise_coprime x
  6. L14
    apply beta_product_pointwise_coprime
03Fix variables and assumptionsL15–18

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

  1. L15
    intro i
  2. L16
    intro n
  3. L17
    intro hi
  4. L18
    intro hn
04Use earlier factsL19–28

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

  1. L19
    specialize crt_pairwise_coprime_prefix_last b
  2. L20
    specialize crt_pairwise_coprime_prefix_last c
  3. L21
    specialize crt_pairwise_coprime_prefix_last l
  4. L22
    specialize crt_pairwise_coprime_prefix_last i
  5. L23
    specialize crt_pairwise_coprime_prefix_last n
  6. L24
    specialize crt_pairwise_coprime_prefix_last m
  7. L25
    apply crt_pairwise_coprime_prefix_last
  8. L26
    exact hpairs
  9. L27
    exact hi
  10. L28
    exact hn
05Use earlier factsL29–30

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

  1. L29
    exact hm
  2. L30
    exact hproduct

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro x
  5. 0005intro m
  6. 0006intro hpairs
  7. 0007intro hproduct
  8. 0008intro hm
  9. 0009specialize beta_product_pointwise_coprime m
  10. 0010specialize beta_product_pointwise_coprime b
  11. 0011specialize beta_product_pointwise_coprime c
  12. 0012specialize beta_product_pointwise_coprime l
  13. 0013specialize beta_product_pointwise_coprime x
  14. 0014apply beta_product_pointwise_coprime
  15. 0015intro i
  16. 0016intro n
  17. 0017intro hi
  18. 0018intro hn
  19. 0019specialize crt_pairwise_coprime_prefix_last b
  20. 0020specialize crt_pairwise_coprime_prefix_last c
  21. 0021specialize crt_pairwise_coprime_prefix_last l
  22. 0022specialize crt_pairwise_coprime_prefix_last i
  23. 0023specialize crt_pairwise_coprime_prefix_last n
  24. 0024specialize crt_pairwise_coprime_prefix_last m
  25. 0025apply crt_pairwise_coprime_prefix_last
  26. 0026exact hpairs
  27. 0027exact hi
  28. 0028exact hn
  29. 0029exact hm
  30. 0030exact hproduct