GC0011

crt_is_gcd_coprime_product

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

For coprime natural factors and any nonzero comparison input, the gcd of their product is exactly the product of their individual relational gcd values.

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 a b n ga gb P T. ~(n = 0) -> T = a * b -> P = ga * gb -> (forall frp_divisor_gcomp_product_coprime. (exists frp_left_factor_gcomp_product_coprime. a = frp_divisor_gcomp_product_coprime * frp_left_factor_gcomp_product_coprime) -> (exists frp_right_factor_gcomp_product_coprime. b = frp_divisor_gcomp_product_coprime * frp_right_factor_gcomp_product_coprime) -> frp_divisor_gcomp_product_coprime = 1) -> ((((exists hag_left_factor_gcomp_product_left. a = ga * hag_left_factor_gcomp_product_left) /\ (exists hag_right_factor_gcomp_product_left. n = ga * hag_right_factor_gcomp_product_left)) /\ forall hag_divisor_gcomp_product_left. (exists hag_common_left_gcomp_product_left. a = hag_divisor_gcomp_product_left * hag_common_left_gcomp_product_left) -> (exists hag_common_right_gcomp_product_left. n = hag_divisor_gcomp_product_left * hag_common_right_gcomp_product_left) -> exists hag_greatest_factor_gcomp_product_left. ga = hag_divisor_gcomp_product_left * hag_greatest_factor_gcomp_product_left)) -> ((((exists hag_left_factor_gcomp_product_right. b = gb * hag_left_factor_gcomp_product_right) /\ (exists hag_right_factor_gcomp_product_right. n = gb * hag_right_factor_gcomp_product_right)) /\ forall hag_divisor_gcomp_product_right. (exists hag_common_left_gcomp_product_right. b = hag_divisor_gcomp_product_right * hag_common_left_gcomp_product_right) -> (exists hag_common_right_gcomp_product_right. n = hag_divisor_gcomp_product_right * hag_common_right_gcomp_product_right) -> exists hag_greatest_factor_gcomp_product_right. gb = hag_divisor_gcomp_product_right * hag_greatest_factor_gcomp_product_right)) -> ((((exists hag_left_factor_gcomp_product_result. T = P * hag_left_factor_gcomp_product_result) /\ (exists hag_right_factor_gcomp_product_result. n = P * hag_right_factor_gcomp_product_result)) /\ forall hag_divisor_gcomp_product_result. (exists hag_common_left_gcomp_product_result. T = hag_divisor_gcomp_product_result * hag_common_left_gcomp_product_result) -> (exists hag_common_right_gcomp_product_result. n = hag_divisor_gcomp_product_result * hag_common_right_gcomp_product_result) -> exists hag_greatest_factor_gcomp_product_result. P = hag_divisor_gcomp_product_result * hag_greatest_factor_gcomp_product_result))

Constructive proof overview

Generated structural guide

For coprime natural factors and any nonzero comparison input, the gcd of their product is exactly the product of their individual relational gcd values.

The unchanged tactic script uses 13 declared prerequisites and contains 123 exact native proof lines.

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

Proof neighborhood

Direct dependencies

is_gcd_dvd_left Stable theorem; checked-use authorized is_gcd_dvd_right Stable theorem; checked-use authorized factor_nonzero_left Stable theorem; checked-use authorized is_gcd_quotients_coprime_nonzero Stable theorem; checked-use authorized multiple_refl Stable theorem; checked-use authorized GC0002 crt_coprime_divisor_pair canonical_gcd_exists Alpha theorem; checked-use authorized is_gcd_symm Stable theorem; checked-use authorized GC000F crt_is_gcd_coprime_factor_remove is_gcd_unique Stable theorem; checked-use authorized GC0010 crt_product_witness mul_assoc Stable theorem; checked-use authorized GC000E crt_is_gcd_scale

Direct dependents

none

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

123 script commands · 28 reading checkpoints · 10 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.

Named ingredients (4)
crt coprime divisor paircrt is gcd coprime factor removecrt product witnesscrt 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 a
  2. L2
    intro b
  3. L3
    intro n
  4. L4
    intro ga
  5. L5
    intro gb
  6. L6
    intro P
  7. L7
    intro T
  8. L8
    intro hnzero
  9. L9
    intro hT
  10. L10
    intro hP
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hab
  2. L12
    intro hga
  3. L13
    intro hgb
03Establish haquotL14–19

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

  1. L14
    have haquot : exists q. a = ga * q
  2. L15
    specialize is_gcd_dvd_left ga
  3. L16
    specialize is_gcd_dvd_left a
  4. L17
    specialize is_gcd_dvd_left n
  5. L18
    apply is_gcd_dvd_left
  6. L19
    exact hga
04Separate the logical casesL20–20

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

  1. L20
    cases haquot
05Establish hnquotL21–26

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

  1. L21
    have hnquot : exists q. n = ga * q
  2. L22
    specialize is_gcd_dvd_right ga
  3. L23
    specialize is_gcd_dvd_right a
  4. L24
    specialize is_gcd_dvd_right n
  5. L25
    apply is_gcd_dvd_right
  6. L26
    exact hga
06Separate the logical casesL27–27

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

  1. L27
    cases hnquot
07Establish hganzeroL28–36

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

  1. L28
    have hganzero : ~(ga = 0)
  2. L29
    specialize factor_nonzero_left n
  3. L30
    specialize factor_nonzero_left ga
  4. L31
    specialize factor_nonzero_left x1
  5. L32
    intro hzero
  6. L33
    apply factor_nonzero_left
  7. L34
    exact hnzero
  8. L35
    exact hnquot_witness
  9. L36
    exact hzero
08Establish hquotcopL37–46

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

  1. L37
    have hquotcop : forall frp_divisor_gcomp_product_quotients. (exists frp_left_factor_gcomp_product_quotients. x = frp_divisor_gcomp_product_quotients * frp_left_factor_gcomp_product_quotients) -> (exists frp_right_factor_gcomp_product_quotients. x1 = frp_divisor_gcomp_product_quotients * frp_right_factor_gcomp_product_quotients) -> frp_divisor_gcomp_product_quotients = 1
  2. L38
    specialize is_gcd_quotients_coprime_nonzero ga
  3. L39
    specialize is_gcd_quotients_coprime_nonzero a
  4. L40
    specialize is_gcd_quotients_coprime_nonzero n
  5. L41
    specialize is_gcd_quotients_coprime_nonzero x
  6. L42
    specialize is_gcd_quotients_coprime_nonzero x1
  7. L43
    apply is_gcd_quotients_coprime_nonzero
  8. L44
    exact hga
  9. L45
    exact hganzero
  10. L46
    exact haquot_witness
09Use earlier factsL47–47

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

  1. L47
    exact hnquot_witness
10Establish hgbcopL48–54

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

  1. L48
    have hgbcop : forall frp_divisor_gcomp_product_scale_coprime. (exists frp_left_factor_gcomp_product_scale_coprime. ga = frp_divisor_gcomp_product_scale_coprime * frp_left_factor_gcomp_product_scale_coprime) -> (exists frp_right_factor_gcomp_product_scale_coprime. b = frp_divisor_gcomp_product_scale_coprime * frp_right_factor_gcomp_product_scale_coprime) -> frp_divisor_gcomp_product_scale_coprime = 1
  2. L49
    specialize crt_coprime_divisor_pair a
  3. L50
    specialize crt_coprime_divisor_pair b
  4. L51
    specialize crt_coprime_divisor_pair ga
  5. L52
    specialize crt_coprime_divisor_pair b
  6. L53
    apply crt_coprime_divisor_pair
  7. L54
    exact hab
11Construct an explicit witnessL55–55

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

  1. L55
    exists x
12Use earlier factsL56–60

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

  1. L56
    exact haquot_witness
  2. L57
    specialize multiple_refl b
  3. L58
    exact multiple_refl
  4. L59
    specialize canonical_gcd_exists b
  5. L60
    specialize canonical_gcd_exists x1
13Separate the logical casesL61–61

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

  1. L61
    cases canonical_gcd_exists
14Establish hswapL62–67

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

  1. L62
    have hswap : IsGCD(x2,x1,b)Definitions: IsGCD
  2. L63
    specialize is_gcd_symm x2
  3. L64
    specialize is_gcd_symm b
  4. L65
    specialize is_gcd_symm x1
  5. L66
    apply is_gcd_symm
  6. L67
    exact canonical_gcd_exists_witness
15Establish hrestoreL68–77

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. L68
    have hrestore : IsGCD(x2,n,b)Definitions: IsGCD
  2. L69
    specialize crt_is_gcd_coprime_factor_remove ga
  3. L70
    specialize crt_is_gcd_coprime_factor_remove x1
  4. L71
    specialize crt_is_gcd_coprime_factor_remove b
  5. L72
    specialize crt_is_gcd_coprime_factor_remove x2
  6. L73
    specialize crt_is_gcd_coprime_factor_remove n
  7. L74
    apply crt_is_gcd_coprime_factor_remove
  8. L75
    exact hnquot_witness
  9. L76
    exact hgbcop
  10. L77
    exact hswap
16Establish hbackL78–83

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

  1. L78
    have hback : IsGCD(x2,b,n)Definitions: IsGCD
  2. L79
    specialize is_gcd_symm x2
  3. L80
    specialize is_gcd_symm n
  4. L81
    specialize is_gcd_symm b
  5. L82
    apply is_gcd_symm
  6. L83
    exact hrestore
17Establish heqL84–93

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

  1. L84
    have heq : x2 = gb
  2. L85
    specialize is_gcd_unique x2
  3. L86
    specialize is_gcd_unique gb
  4. L87
    specialize is_gcd_unique b
  5. L88
    specialize is_gcd_unique n
  6. L89
    apply is_gcd_unique
  7. L90
    exact hback
  8. L91
    exact hgb
  9. L92
    specialize crt_product_witness x
  10. L93
    specialize crt_product_witness b
18Separate the logical casesL94–94

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

  1. L94
    cases crt_product_witness
19Establish hbaseL95–104

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. L95
    have hbase : IsGCD(x2,x3,x1)Definitions: IsGCD
  2. L96
    specialize crt_is_gcd_coprime_factor_remove x
  3. L97
    specialize crt_is_gcd_coprime_factor_remove b
  4. L98
    specialize crt_is_gcd_coprime_factor_remove x1
  5. L99
    specialize crt_is_gcd_coprime_factor_remove x2
  6. L100
    specialize crt_is_gcd_coprime_factor_remove x3
  7. L101
    apply crt_is_gcd_coprime_factor_remove
  8. L102
    exact crt_product_witness_witness
  9. L103
    exact hquotcop
  10. L104
    exact canonical_gcd_exists_witness
20Use earlier factsL105–112

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

  1. L105
    specialize crt_is_gcd_scale ga
  2. L106
    specialize crt_is_gcd_scale x3
  3. L107
    specialize crt_is_gcd_scale x1
  4. L108
    specialize crt_is_gcd_scale x2
  5. L109
    specialize crt_is_gcd_scale T
  6. L110
    specialize crt_is_gcd_scale n
  7. L111
    specialize crt_is_gcd_scale P
  8. L112
    apply crt_is_gcd_scale
21Calculate and transport equalitiesL113–113

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

  1. L113
    trans a * b
22Use earlier factsL114–114

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

  1. L114
    exact hT
23Calculate and transport equalitiesL115–116

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

  1. L115
    rewrite haquot_witness
  2. L116
    trans ga * (x * b)
24Use earlier factsL117–117

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

  1. L117
    apply mul_assoc
25Calculate and transport equalitiesL118–119

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

  1. L118
    rewrite crt_product_witness_witness
  2. L119
    refl
26Use earlier factsL120–120

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

  1. L120
    exact hnquot_witness
27Calculate and transport equalitiesL121–121

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

  1. L121
    rewrite heq
28Use earlier factsL122–123

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

  1. L122
    exact hP
  2. L123
    exact hbase

Library-wide reading audit

Original exact command ledger · 123 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro n
  4. 0004intro ga
  5. 0005intro gb
  6. 0006intro P
  7. 0007intro T
  8. 0008intro hnzero
  9. 0009intro hT
  10. 0010intro hP
  11. 0011intro hab
  12. 0012intro hga
  13. 0013intro hgb
  14. 0014have haquot : exists q. a = ga * q
  15. 0015specialize is_gcd_dvd_left ga
  16. 0016specialize is_gcd_dvd_left a
  17. 0017specialize is_gcd_dvd_left n
  18. 0018apply is_gcd_dvd_left
  19. 0019exact hga
  20. 0020cases haquot
  21. 0021have hnquot : exists q. n = ga * q
  22. 0022specialize is_gcd_dvd_right ga
  23. 0023specialize is_gcd_dvd_right a
  24. 0024specialize is_gcd_dvd_right n
  25. 0025apply is_gcd_dvd_right
  26. 0026exact hga
  27. 0027cases hnquot
  28. 0028have hganzero : ~(ga = 0)
  29. 0029specialize factor_nonzero_left n
  30. 0030specialize factor_nonzero_left ga
  31. 0031specialize factor_nonzero_left x1
  32. 0032intro hzero
  33. 0033apply factor_nonzero_left
  34. 0034exact hnzero
  35. 0035exact hnquot_witness
  36. 0036exact hzero
  37. 0037have hquotcop : forall frp_divisor_gcomp_product_quotients. (exists frp_left_factor_gcomp_product_quotients. x = frp_divisor_gcomp_product_quotients * frp_left_factor_gcomp_product_quotients) -> (exists frp_right_factor_gcomp_product_quotients. x1 = frp_divisor_gcomp_product_quotients * frp_right_factor_gcomp_product_quotients) -> frp_divisor_gcomp_product_quotients = 1
  38. 0038specialize is_gcd_quotients_coprime_nonzero ga
  39. 0039specialize is_gcd_quotients_coprime_nonzero a
  40. 0040specialize is_gcd_quotients_coprime_nonzero n
  41. 0041specialize is_gcd_quotients_coprime_nonzero x
  42. 0042specialize is_gcd_quotients_coprime_nonzero x1
  43. 0043apply is_gcd_quotients_coprime_nonzero
  44. 0044exact hga
  45. 0045exact hganzero
  46. 0046exact haquot_witness
  47. 0047exact hnquot_witness
  48. 0048have hgbcop : forall frp_divisor_gcomp_product_scale_coprime. (exists frp_left_factor_gcomp_product_scale_coprime. ga = frp_divisor_gcomp_product_scale_coprime * frp_left_factor_gcomp_product_scale_coprime) -> (exists frp_right_factor_gcomp_product_scale_coprime. b = frp_divisor_gcomp_product_scale_coprime * frp_right_factor_gcomp_product_scale_coprime) -> frp_divisor_gcomp_product_scale_coprime = 1
  49. 0049specialize crt_coprime_divisor_pair a
  50. 0050specialize crt_coprime_divisor_pair b
  51. 0051specialize crt_coprime_divisor_pair ga
  52. 0052specialize crt_coprime_divisor_pair b
  53. 0053apply crt_coprime_divisor_pair
  54. 0054exact hab
  55. 0055exists x
  56. 0056exact haquot_witness
  57. 0057specialize multiple_refl b
  58. 0058exact multiple_refl
  59. 0059specialize canonical_gcd_exists b
  60. 0060specialize canonical_gcd_exists x1
  61. 0061cases canonical_gcd_exists
  62. 0062have hswap : (((exists hag_left_factor_gcomp_product_intermediate_swap. x1 = x2 * hag_left_factor_gcomp_product_intermediate_swap) /\ (exists hag_right_factor_gcomp_product_intermediate_swap. b = x2 * hag_right_factor_gcomp_product_intermediate_swap)) /\ forall hag_divisor_gcomp_product_intermediate_swap. (exists hag_common_left_gcomp_product_intermediate_swap. x1 = hag_divisor_gcomp_product_intermediate_swap * hag_common_left_gcomp_product_intermediate_swap) -> (exists hag_common_right_gcomp_product_intermediate_swap. b = hag_divisor_gcomp_product_intermediate_swap * hag_common_right_gcomp_product_intermediate_swap) -> exists hag_greatest_factor_gcomp_product_intermediate_swap. x2 = hag_divisor_gcomp_product_intermediate_swap * hag_greatest_factor_gcomp_product_intermediate_swap)
  63. 0063specialize is_gcd_symm x2
  64. 0064specialize is_gcd_symm b
  65. 0065specialize is_gcd_symm x1
  66. 0066apply is_gcd_symm
  67. 0067exact canonical_gcd_exists_witness
  68. 0068have hrestore : (((exists hag_left_factor_gcomp_product_restore_scaled. n = x2 * hag_left_factor_gcomp_product_restore_scaled) /\ (exists hag_right_factor_gcomp_product_restore_scaled. b = x2 * hag_right_factor_gcomp_product_restore_scaled)) /\ forall hag_divisor_gcomp_product_restore_scaled. (exists hag_common_left_gcomp_product_restore_scaled. n = hag_divisor_gcomp_product_restore_scaled * hag_common_left_gcomp_product_restore_scaled) -> (exists hag_common_right_gcomp_product_restore_scaled. b = hag_divisor_gcomp_product_restore_scaled * hag_common_right_gcomp_product_restore_scaled) -> exists hag_greatest_factor_gcomp_product_restore_scaled. x2 = hag_divisor_gcomp_product_restore_scaled * hag_greatest_factor_gcomp_product_restore_scaled)
  69. 0069specialize crt_is_gcd_coprime_factor_remove ga
  70. 0070specialize crt_is_gcd_coprime_factor_remove x1
  71. 0071specialize crt_is_gcd_coprime_factor_remove b
  72. 0072specialize crt_is_gcd_coprime_factor_remove x2
  73. 0073specialize crt_is_gcd_coprime_factor_remove n
  74. 0074apply crt_is_gcd_coprime_factor_remove
  75. 0075exact hnquot_witness
  76. 0076exact hgbcop
  77. 0077exact hswap
  78. 0078have hback : (((exists hag_left_factor_gcomp_product_restore_back. b = x2 * hag_left_factor_gcomp_product_restore_back) /\ (exists hag_right_factor_gcomp_product_restore_back. n = x2 * hag_right_factor_gcomp_product_restore_back)) /\ forall hag_divisor_gcomp_product_restore_back. (exists hag_common_left_gcomp_product_restore_back. b = hag_divisor_gcomp_product_restore_back * hag_common_left_gcomp_product_restore_back) -> (exists hag_common_right_gcomp_product_restore_back. n = hag_divisor_gcomp_product_restore_back * hag_common_right_gcomp_product_restore_back) -> exists hag_greatest_factor_gcomp_product_restore_back. x2 = hag_divisor_gcomp_product_restore_back * hag_greatest_factor_gcomp_product_restore_back)
  79. 0079specialize is_gcd_symm x2
  80. 0080specialize is_gcd_symm n
  81. 0081specialize is_gcd_symm b
  82. 0082apply is_gcd_symm
  83. 0083exact hrestore
  84. 0084have heq : x2 = gb
  85. 0085specialize is_gcd_unique x2
  86. 0086specialize is_gcd_unique gb
  87. 0087specialize is_gcd_unique b
  88. 0088specialize is_gcd_unique n
  89. 0089apply is_gcd_unique
  90. 0090exact hback
  91. 0091exact hgb
  92. 0092specialize crt_product_witness x
  93. 0093specialize crt_product_witness b
  94. 0094cases crt_product_witness
  95. 0095have hbase : (((exists hag_left_factor_gcomp_product_base_temporary. x3 = x2 * hag_left_factor_gcomp_product_base_temporary) /\ (exists hag_right_factor_gcomp_product_base_temporary. x1 = x2 * hag_right_factor_gcomp_product_base_temporary)) /\ forall hag_divisor_gcomp_product_base_temporary. (exists hag_common_left_gcomp_product_base_temporary. x3 = hag_divisor_gcomp_product_base_temporary * hag_common_left_gcomp_product_base_temporary) -> (exists hag_common_right_gcomp_product_base_temporary. x1 = hag_divisor_gcomp_product_base_temporary * hag_common_right_gcomp_product_base_temporary) -> exists hag_greatest_factor_gcomp_product_base_temporary. x2 = hag_divisor_gcomp_product_base_temporary * hag_greatest_factor_gcomp_product_base_temporary)
  96. 0096specialize crt_is_gcd_coprime_factor_remove x
  97. 0097specialize crt_is_gcd_coprime_factor_remove b
  98. 0098specialize crt_is_gcd_coprime_factor_remove x1
  99. 0099specialize crt_is_gcd_coprime_factor_remove x2
  100. 0100specialize crt_is_gcd_coprime_factor_remove x3
  101. 0101apply crt_is_gcd_coprime_factor_remove
  102. 0102exact crt_product_witness_witness
  103. 0103exact hquotcop
  104. 0104exact canonical_gcd_exists_witness
  105. 0105specialize crt_is_gcd_scale ga
  106. 0106specialize crt_is_gcd_scale x3
  107. 0107specialize crt_is_gcd_scale x1
  108. 0108specialize crt_is_gcd_scale x2
  109. 0109specialize crt_is_gcd_scale T
  110. 0110specialize crt_is_gcd_scale n
  111. 0111specialize crt_is_gcd_scale P
  112. 0112apply crt_is_gcd_scale
  113. 0113trans a * b
  114. 0114exact hT
  115. 0115rewrite haquot_witness
  116. 0116trans ga * (x * b)
  117. 0117apply mul_assoc
  118. 0118rewrite crt_product_witness_witness
  119. 0119refl
  120. 0120exact hnquot_witness
  121. 0121rewrite heq
  122. 0122exact hP
  123. 0123exact hbase

Separate complete second-wave branches: Full G011 proof · Alpha v27.