FC0005

crt_gcd_lcm_distributes_scaled_coprime

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Factoring a common gcd scale reduces unrestricted gcd--LCM distributivity to genuinely coprime cofactors.

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.

Exact expanded first-order arithmetic statement

forall k n d K N a b L ga gb g. k = d * K -> n = d * N -> ~(d = 0) -> ~(N = 0) -> (forall frp_divisor_gfull_scaled_comparison. (exists frp_left_factor_gfull_scaled_comparison. K = frp_divisor_gfull_scaled_comparison * frp_left_factor_gfull_scaled_comparison) -> (exists frp_right_factor_gfull_scaled_comparison. N = frp_divisor_gfull_scaled_comparison * frp_right_factor_gfull_scaled_comparison) -> frp_divisor_gfull_scaled_comparison = 1) -> (forall frp_divisor_gfull_scaled_factors. (exists frp_left_factor_gfull_scaled_factors. a = frp_divisor_gfull_scaled_factors * frp_left_factor_gfull_scaled_factors) -> (exists frp_right_factor_gfull_scaled_factors. b = frp_divisor_gfull_scaled_factors * frp_right_factor_gfull_scaled_factors) -> frp_divisor_gfull_scaled_factors = 1) -> L = k * (a * b) -> ((((exists ec_gcd_left_gfull_scaled_ga. (k * a) = ga * ec_gcd_left_gfull_scaled_ga) /\ (exists ec_gcd_right_gfull_scaled_ga. n = ga * ec_gcd_right_gfull_scaled_ga)) /\ forall ec_gcd_common_gfull_scaled_ga. (exists ec_gcd_common_left_gfull_scaled_ga. (k * a) = ec_gcd_common_gfull_scaled_ga * ec_gcd_common_left_gfull_scaled_ga) -> (exists ec_gcd_common_right_gfull_scaled_ga. n = ec_gcd_common_gfull_scaled_ga * ec_gcd_common_right_gfull_scaled_ga) -> exists ec_gcd_greatest_gfull_scaled_ga. ga = ec_gcd_common_gfull_scaled_ga * ec_gcd_greatest_gfull_scaled_ga)) -> ((((exists ec_gcd_left_gfull_scaled_gb. (k * b) = gb * ec_gcd_left_gfull_scaled_gb) /\ (exists ec_gcd_right_gfull_scaled_gb. n = gb * ec_gcd_right_gfull_scaled_gb)) /\ forall ec_gcd_common_gfull_scaled_gb. (exists ec_gcd_common_left_gfull_scaled_gb. (k * b) = ec_gcd_common_gfull_scaled_gb * ec_gcd_common_left_gfull_scaled_gb) -> (exists ec_gcd_common_right_gfull_scaled_gb. n = ec_gcd_common_gfull_scaled_gb * ec_gcd_common_right_gfull_scaled_gb) -> exists ec_gcd_greatest_gfull_scaled_gb. gb = ec_gcd_common_gfull_scaled_gb * ec_gcd_greatest_gfull_scaled_gb)) -> ((((exists ec_gcd_left_gfull_scaled_g. L = g * ec_gcd_left_gfull_scaled_g) /\ (exists ec_gcd_right_gfull_scaled_g. n = g * ec_gcd_right_gfull_scaled_g)) /\ forall ec_gcd_common_gfull_scaled_g. (exists ec_gcd_common_left_gfull_scaled_g. L = ec_gcd_common_gfull_scaled_g * ec_gcd_common_left_gfull_scaled_g) -> (exists ec_gcd_common_right_gfull_scaled_g. n = ec_gcd_common_gfull_scaled_g * ec_gcd_common_right_gfull_scaled_g) -> exists ec_gcd_greatest_gfull_scaled_g. g = ec_gcd_common_gfull_scaled_g * ec_gcd_greatest_gfull_scaled_g)) -> ((((exists hscale_left_factor_gfull_scaled_result. g = ga * hscale_left_factor_gfull_scaled_result) /\ (exists hscale_right_factor_gfull_scaled_result. g = gb * hscale_right_factor_gfull_scaled_result)) /\ forall hscale_common_gfull_scaled_result. (exists hscale_left_common_gfull_scaled_result. hscale_common_gfull_scaled_result = ga * hscale_left_common_gfull_scaled_result) -> (exists hscale_right_common_gfull_scaled_result. hscale_common_gfull_scaled_result = gb * hscale_right_common_gfull_scaled_result) -> exists hscale_least_factor_gfull_scaled_result. hscale_common_gfull_scaled_result = g * hscale_least_factor_gfull_scaled_result))

Constructive proof overview

Generated structural guide

Factoring a common gcd scale reduces unrestricted gcd--LCM distributivity to genuinely coprime cofactors.

The unchanged tactic script uses 8 declared prerequisites and contains 157 exact native proof lines.

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

Proof neighborhood

Direct dependencies

canonical_gcd_exists Alpha theorem; checked-use authorized crt_coprime_divisor_pair Alpha theorem; checked-use authorized is_gcd_dvd_left Stable theorem; checked-use authorized crt_is_gcd_coprime_product Alpha theorem; checked-use authorized crt_gcd_scaled_coprime_component Alpha theorem; checked-use authorized is_gcd_unique Stable theorem; checked-use authorized is_lcm_scale_nonzero Stable theorem; checked-use authorized coprime_product_is_lcm Stable theorem; checked-use authorized

Direct dependents

FC0006 crt_gcd_lcm_distributes_nonzero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

157 script commands · 31 reading checkpoints · 11 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.

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 b
  8. L8
    intro L
  9. L9
    intro ga
  10. L10
    intro gb
02Fix variables and assumptionsL11–20

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

  1. L11
    intro g
  2. L12
    intro hk
  3. L13
    intro hn
  4. L14
    intro hd
  5. L15
    intro hN
  6. L16
    intro hKN
  7. L17
    intro hab
  8. L18
    intro hL
  9. L19
    intro hga
  10. L20
    intro hgb
03Fix variables and assumptionsL21–21

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

  1. L21
    intro hg
04Establish hauL22–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply canonical gcd exists.

  1. L22
    have hau : exists u. (((exists ec_gcd_left_gfull_scaled_u. a = u * ec_gcd_left_gfull_scaled_u) /\ (exists ec_gcd_right_gfull_scaled_u. N = u * ec_gcd_right_gfull_scaled_u)) /\ forall ec_gcd_common_gfull_scaled_u. (exists ec_gcd_common_left_gfull_scaled_u. a = ec_gcd_common_gfull_scaled_u * ec_gcd_common_left_gfull_scaled_u) -> (exists ec_gcd_common_right_gfull_scaled_u. N = ec_gcd_common_gfull_scaled_u * ec_gcd_common_right_gfull_scaled_u) -> exists ec_gcd_greatest_gfull_scaled_u. u = ec_gcd_common_gfull_scaled_u * ec_gcd_greatest_gfull_scaled_u)
  2. L23
    specialize canonical_gcd_exists a
  3. L24
    specialize canonical_gcd_exists N
  4. L25
    apply canonical_gcd_exists
05Separate the logical casesL26–26

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

  1. L26
    cases hau
06Establish hbvL27–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply canonical gcd exists.

  1. L27
    have hbv : exists v. (((exists ec_gcd_left_gfull_scaled_v. b = v * ec_gcd_left_gfull_scaled_v) /\ (exists ec_gcd_right_gfull_scaled_v. N = v * ec_gcd_right_gfull_scaled_v)) /\ forall ec_gcd_common_gfull_scaled_v. (exists ec_gcd_common_left_gfull_scaled_v. b = ec_gcd_common_gfull_scaled_v * ec_gcd_common_left_gfull_scaled_v) -> (exists ec_gcd_common_right_gfull_scaled_v. N = ec_gcd_common_gfull_scaled_v * ec_gcd_common_right_gfull_scaled_v) -> exists ec_gcd_greatest_gfull_scaled_v. v = ec_gcd_common_gfull_scaled_v * ec_gcd_greatest_gfull_scaled_v)
  2. L28
    specialize canonical_gcd_exists b
  3. L29
    specialize canonical_gcd_exists N
  4. L30
    apply canonical_gcd_exists
07Separate the logical casesL31–31

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

  1. L31
    cases hbv
08Establish huvL32–41

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

  1. L32
    have huv : forall frp_divisor_gfull_scaled_uv. (exists frp_left_factor_gfull_scaled_uv. x = frp_divisor_gfull_scaled_uv * frp_left_factor_gfull_scaled_uv) -> (exists frp_right_factor_gfull_scaled_uv. x1 = frp_divisor_gfull_scaled_uv * frp_right_factor_gfull_scaled_uv) -> frp_divisor_gfull_scaled_uv = 1
  2. L33
    specialize crt_coprime_divisor_pair a
  3. L34
    specialize crt_coprime_divisor_pair b
  4. L35
    specialize crt_coprime_divisor_pair x
  5. L36
    specialize crt_coprime_divisor_pair x1
  6. L37
    apply crt_coprime_divisor_pair
  7. L38
    exact hab
  8. L39
    specialize is_gcd_dvd_left x
  9. L40
    specialize is_gcd_dvd_left a
  10. L41
    specialize is_gcd_dvd_left N
09Use earlier factsL42–48

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

  1. L42
    apply is_gcd_dvd_left
  2. L43
    exact hau_witness
  3. L44
    specialize is_gcd_dvd_left x1
  4. L45
    specialize is_gcd_dvd_left b
  5. L46
    specialize is_gcd_dvd_left N
  6. L47
    apply is_gcd_dvd_left
  7. L48
    exact hbv_witness
10Establish hproductL49–58

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

  1. L49
    have hproduct : IsGCD(x · x1,a · b,N)Definitions: IsGCD
  2. L50
    specialize crt_is_gcd_coprime_product a
  3. L51
    specialize crt_is_gcd_coprime_product b
  4. L52
    specialize crt_is_gcd_coprime_product N
  5. L53
    specialize crt_is_gcd_coprime_product x
  6. L54
    specialize crt_is_gcd_coprime_product x1
  7. L55
    specialize crt_is_gcd_coprime_product (x * x1)
  8. L56
    specialize crt_is_gcd_coprime_product (a * b)
  9. L57
    apply crt_is_gcd_coprime_product
  10. L58
    exact hN
11Calculate and transport equalitiesL59–60

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

  1. L59
    refl
  2. L60
    refl
12Use earlier factsL61–63

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

  1. L61
    exact hab
  2. L62
    exact hau_witness
  3. L63
    exact hbv_witness
13Establish huaL64–73

Establish this local claim before using it. It is not an additional assumption.

  1. L64
    have hua : (((exists ec_gcd_left_gfull_scaled_ua. (k * a) = (d * x) * ec_gcd_left_gfull_scaled_ua) /\ (exists ec_gcd_right_gfull_scaled_ua. n = (d * x) * ec_gcd_right_gfull_scaled_ua)) /\ forall ec_gcd_common_gfull_scaled_ua. (exists ec_gcd_common_left_gfull_scaled_ua. (k * a) = ec_gcd_common_gfull_scaled_ua * ec_gcd_common_left_gfull_scaled_ua) -> (exists ec_gcd_common_right_gfull_scaled_ua. n = ec_gcd_common_gfull_scaled_ua * ec_gcd_common_right_gfull_scaled_ua) -> exists ec_gcd_greatest_gfull_scaled_ua. (d * x) = ec_gcd_common_gfull_scaled_ua * ec_gcd_greatest_gfull_scaled_ua)
  2. L65
    specialize crt_gcd_scaled_coprime_component k
  3. L66
    specialize crt_gcd_scaled_coprime_component n
  4. L67
    specialize crt_gcd_scaled_coprime_component d
  5. L68
    specialize crt_gcd_scaled_coprime_component K
  6. L69
    specialize crt_gcd_scaled_coprime_component N
  7. L70
    specialize crt_gcd_scaled_coprime_component a
  8. L71
    specialize crt_gcd_scaled_coprime_component x
  9. L72
    specialize crt_gcd_scaled_coprime_component (k * a)
  10. L73
    specialize crt_gcd_scaled_coprime_component (d * x)
14Use earlier factsL74–76

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

  1. L74
    apply crt_gcd_scaled_coprime_component
  2. L75
    exact hk
  3. L76
    exact hn
15Calculate and transport equalitiesL77–78

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

  1. L77
    refl
  2. L78
    refl
16Use earlier factsL79–80

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

  1. L79
    exact hKN
  2. L80
    exact hau_witness
17Establish hvbL81–90

Establish this local claim before using it. It is not an additional assumption.

  1. L81
    have hvb : (((exists ec_gcd_left_gfull_scaled_vb. (k * b) = (d * x1) * ec_gcd_left_gfull_scaled_vb) /\ (exists ec_gcd_right_gfull_scaled_vb. n = (d * x1) * ec_gcd_right_gfull_scaled_vb)) /\ forall ec_gcd_common_gfull_scaled_vb. (exists ec_gcd_common_left_gfull_scaled_vb. (k * b) = ec_gcd_common_gfull_scaled_vb * ec_gcd_common_left_gfull_scaled_vb) -> (exists ec_gcd_common_right_gfull_scaled_vb. n = ec_gcd_common_gfull_scaled_vb * ec_gcd_common_right_gfull_scaled_vb) -> exists ec_gcd_greatest_gfull_scaled_vb. (d * x1) = ec_gcd_common_gfull_scaled_vb * ec_gcd_greatest_gfull_scaled_vb)
  2. L82
    specialize crt_gcd_scaled_coprime_component k
  3. L83
    specialize crt_gcd_scaled_coprime_component n
  4. L84
    specialize crt_gcd_scaled_coprime_component d
  5. L85
    specialize crt_gcd_scaled_coprime_component K
  6. L86
    specialize crt_gcd_scaled_coprime_component N
  7. L87
    specialize crt_gcd_scaled_coprime_component b
  8. L88
    specialize crt_gcd_scaled_coprime_component x1
  9. L89
    specialize crt_gcd_scaled_coprime_component (k * b)
  10. L90
    specialize crt_gcd_scaled_coprime_component (d * x1)
18Use earlier factsL91–93

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

  1. L91
    apply crt_gcd_scaled_coprime_component
  2. L92
    exact hk
  3. L93
    exact hn
19Calculate and transport equalitiesL94–95

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

  1. L94
    refl
  2. L95
    refl
20Use earlier factsL96–97

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

  1. L96
    exact hKN
  2. L97
    exact hbv_witness
21Establish hwL98–107

Establish this local claim before using it. It is not an additional assumption.

  1. L98
    have hw : (((exists ec_gcd_left_gfull_scaled_w. L = (d * (x * x1)) * ec_gcd_left_gfull_scaled_w) /\ (exists ec_gcd_right_gfull_scaled_w. n = (d * (x * x1)) * ec_gcd_right_gfull_scaled_w)) /\ forall ec_gcd_common_gfull_scaled_w. (exists ec_gcd_common_left_gfull_scaled_w. L = ec_gcd_common_gfull_scaled_w * ec_gcd_common_left_gfull_scaled_w) -> (exists ec_gcd_common_right_gfull_scaled_w. n = ec_gcd_common_gfull_scaled_w * ec_gcd_common_right_gfull_scaled_w) -> exists ec_gcd_greatest_gfull_scaled_w. (d * (x * x1)) = ec_gcd_common_gfull_scaled_w * ec_gcd_greatest_gfull_scaled_w)
  2. L99
    specialize crt_gcd_scaled_coprime_component k
  3. L100
    specialize crt_gcd_scaled_coprime_component n
  4. L101
    specialize crt_gcd_scaled_coprime_component d
  5. L102
    specialize crt_gcd_scaled_coprime_component K
  6. L103
    specialize crt_gcd_scaled_coprime_component N
  7. L104
    specialize crt_gcd_scaled_coprime_component (a * b)
  8. L105
    specialize crt_gcd_scaled_coprime_component (x * x1)
  9. L106
    specialize crt_gcd_scaled_coprime_component L
  10. L107
    specialize crt_gcd_scaled_coprime_component (d * (x * x1))
22Use earlier factsL108–111

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

  1. L108
    apply crt_gcd_scaled_coprime_component
  2. L109
    exact hk
  3. L110
    exact hn
  4. L111
    exact hL
23Calculate and transport equalitiesL112–112

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

  1. L112
    refl
24Use earlier factsL113–114

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

  1. L113
    exact hKN
  2. L114
    exact hproduct
25Establish heqaL115–122

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

  1. L115
    have heqa : ga = d * x
  2. L116
    specialize is_gcd_unique ga
  3. L117
    specialize is_gcd_unique (d * x)
  4. L118
    specialize is_gcd_unique (k * a)
  5. L119
    specialize is_gcd_unique n
  6. L120
    apply is_gcd_unique
  7. L121
    exact hga
  8. L122
    exact hua
26Establish heqbL123–130

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

  1. L123
    have heqb : gb = d * x1
  2. L124
    specialize is_gcd_unique gb
  3. L125
    specialize is_gcd_unique (d * x1)
  4. L126
    specialize is_gcd_unique (k * b)
  5. L127
    specialize is_gcd_unique n
  6. L128
    apply is_gcd_unique
  7. L129
    exact hgb
  8. L130
    exact hvb
27Establish heqgL131–138

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

  1. L131
    have heqg : g = d * (x * x1)
  2. L132
    specialize is_gcd_unique g
  3. L133
    specialize is_gcd_unique (d * (x * x1))
  4. L134
    specialize is_gcd_unique L
  5. L135
    specialize is_gcd_unique n
  6. L136
    apply is_gcd_unique
  7. L137
    exact hg
  8. L138
    exact hw
28Establish hlcmL139–148

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

  1. L139
    have hlcm : Dvd(d · x,d · (x · x1)) ∧ Dvd(d · x1,d · (x · x1)) ∧ (∀ y. Dvd(d · x,y) → Dvd(d · x1,y) → Dvd(d · (x · x1),y))Definitions: Dvd
  2. L140
    specialize is_lcm_scale_nonzero d
  3. L141
    specialize is_lcm_scale_nonzero (x * x1)
  4. L142
    specialize is_lcm_scale_nonzero x
  5. L143
    specialize is_lcm_scale_nonzero x1
  6. L144
    apply is_lcm_scale_nonzero
  7. L145
    exact hd
  8. L146
    specialize coprime_product_is_lcm x
  9. L147
    specialize coprime_product_is_lcm x1
  10. L148
    apply coprime_product_is_lcm
29Use earlier factsL149–149

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

  1. L149
    exact huv
30Calculate and transport equalitiesL150–156

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

  1. L150
    rewrite heqa
  2. L151
    rewrite heqa
  3. L152
    rewrite heqb
  4. L153
    rewrite heqb
  5. L154
    rewrite heqg
  6. L155
    rewrite heqg
  7. L156
    rewrite heqg
31Use earlier factsL157–157

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

  1. L157
    exact hlcm

Library-wide reading audit

Original exact command ledger · 157 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003intro d
  4. 0004intro K
  5. 0005intro N
  6. 0006intro a
  7. 0007intro b
  8. 0008intro L
  9. 0009intro ga
  10. 0010intro gb
  11. 0011intro g
  12. 0012intro hk
  13. 0013intro hn
  14. 0014intro hd
  15. 0015intro hN
  16. 0016intro hKN
  17. 0017intro hab
  18. 0018intro hL
  19. 0019intro hga
  20. 0020intro hgb
  21. 0021intro hg
  22. 0022have hau : exists u. (((exists ec_gcd_left_gfull_scaled_u. a = u * ec_gcd_left_gfull_scaled_u) /\ (exists ec_gcd_right_gfull_scaled_u. N = u * ec_gcd_right_gfull_scaled_u)) /\ forall ec_gcd_common_gfull_scaled_u. (exists ec_gcd_common_left_gfull_scaled_u. a = ec_gcd_common_gfull_scaled_u * ec_gcd_common_left_gfull_scaled_u) -> (exists ec_gcd_common_right_gfull_scaled_u. N = ec_gcd_common_gfull_scaled_u * ec_gcd_common_right_gfull_scaled_u) -> exists ec_gcd_greatest_gfull_scaled_u. u = ec_gcd_common_gfull_scaled_u * ec_gcd_greatest_gfull_scaled_u)
  23. 0023specialize canonical_gcd_exists a
  24. 0024specialize canonical_gcd_exists N
  25. 0025apply canonical_gcd_exists
  26. 0026cases hau
  27. 0027have hbv : exists v. (((exists ec_gcd_left_gfull_scaled_v. b = v * ec_gcd_left_gfull_scaled_v) /\ (exists ec_gcd_right_gfull_scaled_v. N = v * ec_gcd_right_gfull_scaled_v)) /\ forall ec_gcd_common_gfull_scaled_v. (exists ec_gcd_common_left_gfull_scaled_v. b = ec_gcd_common_gfull_scaled_v * ec_gcd_common_left_gfull_scaled_v) -> (exists ec_gcd_common_right_gfull_scaled_v. N = ec_gcd_common_gfull_scaled_v * ec_gcd_common_right_gfull_scaled_v) -> exists ec_gcd_greatest_gfull_scaled_v. v = ec_gcd_common_gfull_scaled_v * ec_gcd_greatest_gfull_scaled_v)
  28. 0028specialize canonical_gcd_exists b
  29. 0029specialize canonical_gcd_exists N
  30. 0030apply canonical_gcd_exists
  31. 0031cases hbv
  32. 0032have huv : forall frp_divisor_gfull_scaled_uv. (exists frp_left_factor_gfull_scaled_uv. x = frp_divisor_gfull_scaled_uv * frp_left_factor_gfull_scaled_uv) -> (exists frp_right_factor_gfull_scaled_uv. x1 = frp_divisor_gfull_scaled_uv * frp_right_factor_gfull_scaled_uv) -> frp_divisor_gfull_scaled_uv = 1
  33. 0033specialize crt_coprime_divisor_pair a
  34. 0034specialize crt_coprime_divisor_pair b
  35. 0035specialize crt_coprime_divisor_pair x
  36. 0036specialize crt_coprime_divisor_pair x1
  37. 0037apply crt_coprime_divisor_pair
  38. 0038exact hab
  39. 0039specialize is_gcd_dvd_left x
  40. 0040specialize is_gcd_dvd_left a
  41. 0041specialize is_gcd_dvd_left N
  42. 0042apply is_gcd_dvd_left
  43. 0043exact hau_witness
  44. 0044specialize is_gcd_dvd_left x1
  45. 0045specialize is_gcd_dvd_left b
  46. 0046specialize is_gcd_dvd_left N
  47. 0047apply is_gcd_dvd_left
  48. 0048exact hbv_witness
  49. 0049have hproduct : (((exists ec_gcd_left_gfull_scaled_product. (a * b) = (x * x1) * ec_gcd_left_gfull_scaled_product) /\ (exists ec_gcd_right_gfull_scaled_product. N = (x * x1) * ec_gcd_right_gfull_scaled_product)) /\ forall ec_gcd_common_gfull_scaled_product. (exists ec_gcd_common_left_gfull_scaled_product. (a * b) = ec_gcd_common_gfull_scaled_product * ec_gcd_common_left_gfull_scaled_product) -> (exists ec_gcd_common_right_gfull_scaled_product. N = ec_gcd_common_gfull_scaled_product * ec_gcd_common_right_gfull_scaled_product) -> exists ec_gcd_greatest_gfull_scaled_product. (x * x1) = ec_gcd_common_gfull_scaled_product * ec_gcd_greatest_gfull_scaled_product)
  50. 0050specialize crt_is_gcd_coprime_product a
  51. 0051specialize crt_is_gcd_coprime_product b
  52. 0052specialize crt_is_gcd_coprime_product N
  53. 0053specialize crt_is_gcd_coprime_product x
  54. 0054specialize crt_is_gcd_coprime_product x1
  55. 0055specialize crt_is_gcd_coprime_product (x * x1)
  56. 0056specialize crt_is_gcd_coprime_product (a * b)
  57. 0057apply crt_is_gcd_coprime_product
  58. 0058exact hN
  59. 0059refl
  60. 0060refl
  61. 0061exact hab
  62. 0062exact hau_witness
  63. 0063exact hbv_witness
  64. 0064have hua : (((exists ec_gcd_left_gfull_scaled_ua. (k * a) = (d * x) * ec_gcd_left_gfull_scaled_ua) /\ (exists ec_gcd_right_gfull_scaled_ua. n = (d * x) * ec_gcd_right_gfull_scaled_ua)) /\ forall ec_gcd_common_gfull_scaled_ua. (exists ec_gcd_common_left_gfull_scaled_ua. (k * a) = ec_gcd_common_gfull_scaled_ua * ec_gcd_common_left_gfull_scaled_ua) -> (exists ec_gcd_common_right_gfull_scaled_ua. n = ec_gcd_common_gfull_scaled_ua * ec_gcd_common_right_gfull_scaled_ua) -> exists ec_gcd_greatest_gfull_scaled_ua. (d * x) = ec_gcd_common_gfull_scaled_ua * ec_gcd_greatest_gfull_scaled_ua)
  65. 0065specialize crt_gcd_scaled_coprime_component k
  66. 0066specialize crt_gcd_scaled_coprime_component n
  67. 0067specialize crt_gcd_scaled_coprime_component d
  68. 0068specialize crt_gcd_scaled_coprime_component K
  69. 0069specialize crt_gcd_scaled_coprime_component N
  70. 0070specialize crt_gcd_scaled_coprime_component a
  71. 0071specialize crt_gcd_scaled_coprime_component x
  72. 0072specialize crt_gcd_scaled_coprime_component (k * a)
  73. 0073specialize crt_gcd_scaled_coprime_component (d * x)
  74. 0074apply crt_gcd_scaled_coprime_component
  75. 0075exact hk
  76. 0076exact hn
  77. 0077refl
  78. 0078refl
  79. 0079exact hKN
  80. 0080exact hau_witness
  81. 0081have hvb : (((exists ec_gcd_left_gfull_scaled_vb. (k * b) = (d * x1) * ec_gcd_left_gfull_scaled_vb) /\ (exists ec_gcd_right_gfull_scaled_vb. n = (d * x1) * ec_gcd_right_gfull_scaled_vb)) /\ forall ec_gcd_common_gfull_scaled_vb. (exists ec_gcd_common_left_gfull_scaled_vb. (k * b) = ec_gcd_common_gfull_scaled_vb * ec_gcd_common_left_gfull_scaled_vb) -> (exists ec_gcd_common_right_gfull_scaled_vb. n = ec_gcd_common_gfull_scaled_vb * ec_gcd_common_right_gfull_scaled_vb) -> exists ec_gcd_greatest_gfull_scaled_vb. (d * x1) = ec_gcd_common_gfull_scaled_vb * ec_gcd_greatest_gfull_scaled_vb)
  82. 0082specialize crt_gcd_scaled_coprime_component k
  83. 0083specialize crt_gcd_scaled_coprime_component n
  84. 0084specialize crt_gcd_scaled_coprime_component d
  85. 0085specialize crt_gcd_scaled_coprime_component K
  86. 0086specialize crt_gcd_scaled_coprime_component N
  87. 0087specialize crt_gcd_scaled_coprime_component b
  88. 0088specialize crt_gcd_scaled_coprime_component x1
  89. 0089specialize crt_gcd_scaled_coprime_component (k * b)
  90. 0090specialize crt_gcd_scaled_coprime_component (d * x1)
  91. 0091apply crt_gcd_scaled_coprime_component
  92. 0092exact hk
  93. 0093exact hn
  94. 0094refl
  95. 0095refl
  96. 0096exact hKN
  97. 0097exact hbv_witness
  98. 0098have hw : (((exists ec_gcd_left_gfull_scaled_w. L = (d * (x * x1)) * ec_gcd_left_gfull_scaled_w) /\ (exists ec_gcd_right_gfull_scaled_w. n = (d * (x * x1)) * ec_gcd_right_gfull_scaled_w)) /\ forall ec_gcd_common_gfull_scaled_w. (exists ec_gcd_common_left_gfull_scaled_w. L = ec_gcd_common_gfull_scaled_w * ec_gcd_common_left_gfull_scaled_w) -> (exists ec_gcd_common_right_gfull_scaled_w. n = ec_gcd_common_gfull_scaled_w * ec_gcd_common_right_gfull_scaled_w) -> exists ec_gcd_greatest_gfull_scaled_w. (d * (x * x1)) = ec_gcd_common_gfull_scaled_w * ec_gcd_greatest_gfull_scaled_w)
  99. 0099specialize crt_gcd_scaled_coprime_component k
  100. 0100specialize crt_gcd_scaled_coprime_component n
  101. 0101specialize crt_gcd_scaled_coprime_component d
  102. 0102specialize crt_gcd_scaled_coprime_component K
  103. 0103specialize crt_gcd_scaled_coprime_component N
  104. 0104specialize crt_gcd_scaled_coprime_component (a * b)
  105. 0105specialize crt_gcd_scaled_coprime_component (x * x1)
  106. 0106specialize crt_gcd_scaled_coprime_component L
  107. 0107specialize crt_gcd_scaled_coprime_component (d * (x * x1))
  108. 0108apply crt_gcd_scaled_coprime_component
  109. 0109exact hk
  110. 0110exact hn
  111. 0111exact hL
  112. 0112refl
  113. 0113exact hKN
  114. 0114exact hproduct
  115. 0115have heqa : ga = d * x
  116. 0116specialize is_gcd_unique ga
  117. 0117specialize is_gcd_unique (d * x)
  118. 0118specialize is_gcd_unique (k * a)
  119. 0119specialize is_gcd_unique n
  120. 0120apply is_gcd_unique
  121. 0121exact hga
  122. 0122exact hua
  123. 0123have heqb : gb = d * x1
  124. 0124specialize is_gcd_unique gb
  125. 0125specialize is_gcd_unique (d * x1)
  126. 0126specialize is_gcd_unique (k * b)
  127. 0127specialize is_gcd_unique n
  128. 0128apply is_gcd_unique
  129. 0129exact hgb
  130. 0130exact hvb
  131. 0131have heqg : g = d * (x * x1)
  132. 0132specialize is_gcd_unique g
  133. 0133specialize is_gcd_unique (d * (x * x1))
  134. 0134specialize is_gcd_unique L
  135. 0135specialize is_gcd_unique n
  136. 0136apply is_gcd_unique
  137. 0137exact hg
  138. 0138exact hw
  139. 0139have hlcm : (((exists hscale_left_factor_gfull_scaled_lcm. (d * (x * x1)) = (d * x) * hscale_left_factor_gfull_scaled_lcm) /\ (exists hscale_right_factor_gfull_scaled_lcm. (d * (x * x1)) = (d * x1) * hscale_right_factor_gfull_scaled_lcm)) /\ forall hscale_common_gfull_scaled_lcm. (exists hscale_left_common_gfull_scaled_lcm. hscale_common_gfull_scaled_lcm = (d * x) * hscale_left_common_gfull_scaled_lcm) -> (exists hscale_right_common_gfull_scaled_lcm. hscale_common_gfull_scaled_lcm = (d * x1) * hscale_right_common_gfull_scaled_lcm) -> exists hscale_least_factor_gfull_scaled_lcm. hscale_common_gfull_scaled_lcm = (d * (x * x1)) * hscale_least_factor_gfull_scaled_lcm)
  140. 0140specialize is_lcm_scale_nonzero d
  141. 0141specialize is_lcm_scale_nonzero (x * x1)
  142. 0142specialize is_lcm_scale_nonzero x
  143. 0143specialize is_lcm_scale_nonzero x1
  144. 0144apply is_lcm_scale_nonzero
  145. 0145exact hd
  146. 0146specialize coprime_product_is_lcm x
  147. 0147specialize coprime_product_is_lcm x1
  148. 0148apply coprime_product_is_lcm
  149. 0149exact huv
  150. 0150rewrite heqa
  151. 0151rewrite heqa
  152. 0152rewrite heqb
  153. 0153rewrite heqb
  154. 0154rewrite heqg
  155. 0155rewrite heqg
  156. 0156rewrite heqg
  157. 0157exact hlcm