GC0013

crt_gcd_scaled_coprime_component

After factoring a common divisor from a multiplier and comparison input, the gcd is exactly that divisor times the gcd of the remaining coprime component.

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

∀ k. ∀ n. ∀ d. ∀ K. ∀ N. ∀ a. ∀ ga. ∀ A. ∀ G. k = d · K → n = d · N → A = k · a → G = d · ga → Coprime(K,N) → IsGCD(ga,a,N) → IsGCD(G,A,n)

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

Definition DAG

Coprime(a,b) · 1IsGCD(g,a,b) · 2

Actual proof prerequisites

crt_product_witnesscrt_is_gcd_coprime_factor_removemul_assoc · checked external prerequisitecrt_is_gcd_scale
Original expanded first-order statement 
forall k n d K N a ga A G. k = d * K -> n = d * N -> A = k * a -> G = d * ga -> (forall frp_divisor_gcomp_scaled_component_coprime. (exists frp_left_factor_gcomp_scaled_component_coprime. K = frp_divisor_gcomp_scaled_component_coprime * frp_left_factor_gcomp_scaled_component_coprime) -> (exists frp_right_factor_gcomp_scaled_component_coprime. N = frp_divisor_gcomp_scaled_component_coprime * frp_right_factor_gcomp_scaled_component_coprime) -> frp_divisor_gcomp_scaled_component_coprime = 1) -> ((((exists hag_left_factor_gcomp_scaled_component_base. a = ga * hag_left_factor_gcomp_scaled_component_base) /\ (exists hag_right_factor_gcomp_scaled_component_base. N = ga * hag_right_factor_gcomp_scaled_component_base)) /\ forall hag_divisor_gcomp_scaled_component_base. (exists hag_common_left_gcomp_scaled_component_base. a = hag_divisor_gcomp_scaled_component_base * hag_common_left_gcomp_scaled_component_base) -> (exists hag_common_right_gcomp_scaled_component_base. N = hag_divisor_gcomp_scaled_component_base * hag_common_right_gcomp_scaled_component_base) -> exists hag_greatest_factor_gcomp_scaled_component_base. ga = hag_divisor_gcomp_scaled_component_base * hag_greatest_factor_gcomp_scaled_component_base)) -> ((((exists hag_left_factor_gcomp_scaled_component_result. A = G * hag_left_factor_gcomp_scaled_component_result) /\ (exists hag_right_factor_gcomp_scaled_component_result. n = G * hag_right_factor_gcomp_scaled_component_result)) /\ forall hag_divisor_gcomp_scaled_component_result. (exists hag_common_left_gcomp_scaled_component_result. A = hag_divisor_gcomp_scaled_component_result * hag_common_left_gcomp_scaled_component_result) -> (exists hag_common_right_gcomp_scaled_component_result. n = hag_divisor_gcomp_scaled_component_result * hag_common_right_gcomp_scaled_component_result) -> exists hag_greatest_factor_gcomp_scaled_component_result. G = hag_divisor_gcomp_scaled_component_result * hag_greatest_factor_gcomp_scaled_component_result))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

46 script commands · 12 reading checkpoints · 1 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 (3)
crt product witnesscrt is gcd coprime factor removecrt is gcd scale

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 k
  2. L2
    intro n
  3. L3
    intro d
  4. L4
    intro K
  5. L5
    intro N
  6. L6
    intro a
  7. L7
    intro ga
  8. L8
    intro A
  9. L9
    intro G
  10. L10
    intro hk
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hn
  2. L12
    intro hA
  3. L13
    intro hG
  4. L14
    intro hcoprime
  5. L15
    intro hga
03Use earlier factsL16–17

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

  1. L16
    specialize crt_product_witness K
  2. L17
    specialize crt_product_witness a
04Separate the logical casesL18–18

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

  1. L18
    cases crt_product_witness
05Establish hbaseL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt is gcd coprime factor remove.

  1. L19
    have hbase : IsGCD(ga,x,N)Definitions: IsGCDOriginal native command in the exact edition
  2. L20
    specialize crt_is_gcd_coprime_factor_remove K
  3. L21
    specialize crt_is_gcd_coprime_factor_remove a
  4. L22
    specialize crt_is_gcd_coprime_factor_remove N
  5. L23
    specialize crt_is_gcd_coprime_factor_remove ga
  6. L24
    specialize crt_is_gcd_coprime_factor_remove x
  7. L25
    apply crt_is_gcd_coprime_factor_remove
  8. L26
    exact crt_product_witness_witness
  9. L27
    exact hcoprime
  10. L28
    exact hga
06Use earlier factsL29–36

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

  1. L29
    specialize crt_is_gcd_scale d
  2. L30
    specialize crt_is_gcd_scale x
  3. L31
    specialize crt_is_gcd_scale N
  4. L32
    specialize crt_is_gcd_scale ga
  5. L33
    specialize crt_is_gcd_scale A
  6. L34
    specialize crt_is_gcd_scale n
  7. L35
    specialize crt_is_gcd_scale G
  8. L36
    apply crt_is_gcd_scale
07Calculate and transport equalitiesL37–37

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

  1. L37
    trans k * a
08Use earlier factsL38–38

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

  1. L38
    exact hA
09Calculate and transport equalitiesL39–40

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

  1. L39
    rewrite hk
  2. L40
    trans d * (K * a)
10Use earlier factsL41–41

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

  1. L41
    apply mul_assoc
11Calculate and transport equalitiesL42–43

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

  1. L42
    rewrite crt_product_witness_witness
  2. L43
    refl
12Use earlier factsL44–46

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

  1. L44
    exact hn
  2. L45
    exact hG
  3. L46
    exact hbase

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003intro d
  4. 0004intro K
  5. 0005intro N
  6. 0006intro a
  7. 0007intro ga
  8. 0008intro A
  9. 0009intro G
  10. 0010intro hk
  11. 0011intro hn
  12. 0012intro hA
  13. 0013intro hG
  14. 0014intro hcoprime
  15. 0015intro hga
  16. 0016specialize crt_product_witness K
  17. 0017specialize crt_product_witness a
  18. 0018cases crt_product_witness
  19. 0019have hbase : (((exists hag_left_factor_gcomp_scaled_component_coprime_product. x = ga * hag_left_factor_gcomp_scaled_component_coprime_product) /\ (exists hag_right_factor_gcomp_scaled_component_coprime_product. N = ga * hag_right_factor_gcomp_scaled_component_coprime_product)) /\ forall hag_divisor_gcomp_scaled_component_coprime_product. (exists hag_common_left_gcomp_scaled_component_coprime_product. x = hag_divisor_gcomp_scaled_component_coprime_product * hag_common_left_gcomp_scaled_component_coprime_product) -> (exists hag_common_right_gcomp_scaled_component_coprime_product. N = hag_divisor_gcomp_scaled_component_coprime_product * hag_common_right_gcomp_scaled_component_coprime_product) -> exists hag_greatest_factor_gcomp_scaled_component_coprime_product. ga = hag_divisor_gcomp_scaled_component_coprime_product * hag_greatest_factor_gcomp_scaled_component_coprime_product)
  20. 0020specialize crt_is_gcd_coprime_factor_remove K
  21. 0021specialize crt_is_gcd_coprime_factor_remove a
  22. 0022specialize crt_is_gcd_coprime_factor_remove N
  23. 0023specialize crt_is_gcd_coprime_factor_remove ga
  24. 0024specialize crt_is_gcd_coprime_factor_remove x
  25. 0025apply crt_is_gcd_coprime_factor_remove
  26. 0026exact crt_product_witness_witness
  27. 0027exact hcoprime
  28. 0028exact hga
  29. 0029specialize crt_is_gcd_scale d
  30. 0030specialize crt_is_gcd_scale x
  31. 0031specialize crt_is_gcd_scale N
  32. 0032specialize crt_is_gcd_scale ga
  33. 0033specialize crt_is_gcd_scale A
  34. 0034specialize crt_is_gcd_scale n
  35. 0035specialize crt_is_gcd_scale G
  36. 0036apply crt_is_gcd_scale
  37. 0037trans k * a
  38. 0038exact hA
  39. 0039rewrite hk
  40. 0040trans d * (K * a)
  41. 0041apply mul_assoc
  42. 0042rewrite crt_product_witness_witness
  43. 0043refl
  44. 0044exact hn
  45. 0045exact hG
  46. 0046exact hbase