JT0032

jordan_canonical_crt_tuple_exists

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

Construct an actual tuple bounded by the product modulus with both prescribed residue tuples.

Exact expanded first-order arithmetic statement

forall m n b c d e k. ~(m=0) -> ~(n=0) -> (forall jt_divisor_canonicalcrtcoprime. (exists jt_factor_canonicalcrtcoprimea. (m)=(jt_divisor_canonicalcrtcoprime)*jt_factor_canonicalcrtcoprimea) -> (exists jt_factor_canonicalcrtcoprimeb. (n)=(jt_divisor_canonicalcrtcoprime)*jt_factor_canonicalcrtcoprimeb) -> jt_divisor_canonicalcrtcoprime=1) -> exists f g. ((forall jt_index_canonicalcrtexistsbound. (exists jt_gap_canonicalcrtexistsboundindex. jt_gap_canonicalcrtexistsboundindex+S (jt_index_canonicalcrtexistsbound)=(k)) -> exists jt_value_canonicalcrtexistsbound. ((((exists fs_h_jt_canonicalcrtexistsboundat. fs_h_jt_canonicalcrtexistsboundat + S (jt_value_canonicalcrtexistsbound) = S ((S (jt_index_canonicalcrtexistsbound)) * g)) /\ exists fs_q_jt_canonicalcrtexistsboundat. f = fs_q_jt_canonicalcrtexistsboundat * S ((S (jt_index_canonicalcrtexistsbound)) * g) + (jt_value_canonicalcrtexistsbound))) /\ (exists jt_gap_canonicalcrtexistsboundvalue. jt_gap_canonicalcrtexistsboundvalue+S (jt_value_canonicalcrtexistsbound)=(m*n)))) /\ (((forall jt_index_canonicalcrtexistsleft jt_left_canonicalcrtexistsleft jt_right_canonicalcrtexistsleft. (exists jt_gap_canonicalcrtexistsleftindex. jt_gap_canonicalcrtexistsleftindex+S (jt_index_canonicalcrtexistsleft)=(k)) -> (((exists fs_h_jt_canonicalcrtexistsleftleft. fs_h_jt_canonicalcrtexistsleftleft + S (jt_left_canonicalcrtexistsleft) = S ((S (jt_index_canonicalcrtexistsleft)) * g)) /\ exists fs_q_jt_canonicalcrtexistsleftleft. f = fs_q_jt_canonicalcrtexistsleftleft * S ((S (jt_index_canonicalcrtexistsleft)) * g) + (jt_left_canonicalcrtexistsleft))) -> (((exists fs_h_jt_canonicalcrtexistsleftright. fs_h_jt_canonicalcrtexistsleftright + S (jt_right_canonicalcrtexistsleft) = S ((S (jt_index_canonicalcrtexistsleft)) * c)) /\ exists fs_q_jt_canonicalcrtexistsleftright. b = fs_q_jt_canonicalcrtexistsleftright * S ((S (jt_index_canonicalcrtexistsleft)) * c) + (jt_right_canonicalcrtexistsleft))) -> (exists jt_left_canonicalcrtexistsleftmod jt_right_canonicalcrtexistsleftmod. (jt_left_canonicalcrtexistsleft)+(m)*jt_left_canonicalcrtexistsleftmod=(jt_right_canonicalcrtexistsleft)+(m)*jt_right_canonicalcrtexistsleftmod)) /\ (forall jt_index_canonicalcrtexistsright jt_left_canonicalcrtexistsright jt_right_canonicalcrtexistsright. (exists jt_gap_canonicalcrtexistsrightindex. jt_gap_canonicalcrtexistsrightindex+S (jt_index_canonicalcrtexistsright)=(k)) -> (((exists fs_h_jt_canonicalcrtexistsrightleft. fs_h_jt_canonicalcrtexistsrightleft + S (jt_left_canonicalcrtexistsright) = S ((S (jt_index_canonicalcrtexistsright)) * g)) /\ exists fs_q_jt_canonicalcrtexistsrightleft. f = fs_q_jt_canonicalcrtexistsrightleft * S ((S (jt_index_canonicalcrtexistsright)) * g) + (jt_left_canonicalcrtexistsright))) -> (((exists fs_h_jt_canonicalcrtexistsrightright. fs_h_jt_canonicalcrtexistsrightright + S (jt_right_canonicalcrtexistsright) = S ((S (jt_index_canonicalcrtexistsright)) * e)) /\ exists fs_q_jt_canonicalcrtexistsrightright. d = fs_q_jt_canonicalcrtexistsrightright * S ((S (jt_index_canonicalcrtexistsright)) * e) + (jt_right_canonicalcrtexistsright))) -> (exists jt_left_canonicalcrtexistsrightmod jt_right_canonicalcrtexistsrightmod. (jt_left_canonicalcrtexistsright)+(n)*jt_left_canonicalcrtexistsrightmod=(jt_right_canonicalcrtexistsright)+(n)*jt_right_canonicalcrtexistsrightmod)))))

Constructive proof overview

Generated structural guide

Construct an actual tuple bounded by the product modulus with both prescribed residue tuples.

The unchanged tactic script uses 9 declared prerequisites and contains 131 exact native proof lines.

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

Proof neighborhood

Direct dependencies

JT002C jordan_crt_tuple_exists mul_ne_zero Alpha theorem; checked-use authorized JT002F jordan_tuple_normalize_exists JT0031 jordan_tuple_congruence_divisor mul_comm Alpha theorem; checked-use authorized JT0030 jordan_tuple_congruence_trans JT000E jordan_tuple_congruence_symm JT002D jordan_crt_tuple_left JT002E jordan_crt_tuple_right

Direct dependents

JT0033 jordan_primitive_crt_tuple_exists

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

131 script commands · 24 reading checkpoints · 6 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 (7)
jordan crt tuple existsjordan tuple normalize existsjordan tuple congruence divisorjordan tuple congruence transjordan tuple congruence symmjordan crt tuple leftjordan crt tuple right

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 m
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro k
  8. L8
    intro hm
  9. L9
    intro hn
  10. L10
    intro hcop
02Establish hfamilyL11–20

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

  1. L11
    have hfamily : ∀ L. ∃ f. ∃ g. JordanTupleCRT(m,n,b,c,d,e,f,g,L)Definitions: JordanTupleCRT
  2. L12
    specialize jordan_crt_tuple_exists (m)
  3. L13
    specialize jordan_crt_tuple_exists (n)
  4. L14
    specialize jordan_crt_tuple_exists (b)
  5. L15
    specialize jordan_crt_tuple_exists (c)
  6. L16
    specialize jordan_crt_tuple_exists (d)
  7. L17
    specialize jordan_crt_tuple_exists (e)
  8. L18
    apply jordan_crt_tuple_exists
  9. L19
    exact hm
  10. L20
    exact hn
03Use earlier factsL21–21

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

  1. L21
    exact hcop
04Establish hrawL22–24

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

  1. L22
    have hraw : ∃ f. ∃ g. JordanTupleCRT(m,n,b,c,d,e,f,g,k)Definitions: JordanTupleCRT
  2. L23
    specialize hfamily (k)
  3. L24
    apply hfamily
05Separate the logical casesL25–26

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

  1. L25
    cases hraw
  2. L26
    cases hraw_witness
06Establish hproductL27–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul ne zero.

  1. L27
    have hproduct : ~(m*n=0)
  2. L28
    intro hz
  3. L29
    specialize mul_ne_zero (m)
  4. L30
    specialize mul_ne_zero (n)
  5. L31
    apply mul_ne_zero
  6. L32
    exact hm
  7. L33
    exact hn
  8. L34
    exact hz
07Establish hnormL35–41

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

  1. L35
    have hnorm : ∃ u. ∃ v. BetaPrefixInto(u,v,k,m · n) ∧ JordanTupleCongruence(m · n,x,x1,u,v,k)Definitions: BetaPrefixIntoJordanTupleCongruence
  2. L36
    specialize jordan_tuple_normalize_exists (m*n)
  3. L37
    specialize jordan_tuple_normalize_exists (x)
  4. L38
    specialize jordan_tuple_normalize_exists (x1)
  5. L39
    specialize jordan_tuple_normalize_exists (k)
  6. L40
    apply jordan_tuple_normalize_exists
  7. L41
    exact hproduct
08Separate the logical casesL42–44

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

  1. L42
    cases hnorm
  2. L43
    cases hnorm_witness
  3. L44
    cases hnorm_witness_witness
09Construct an explicit witnessL45–46

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

  1. L45
    exists x2
  2. L46
    exists x3
10Separate the logical casesL47–47

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

  1. L47
    split
11Use earlier factsL48–48

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

  1. L48
    exact hnorm_witness_witness_left
12Separate the logical casesL49–49

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

  1. L49
    split
13Establish hsmallL50–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple congruence divisor.

  1. L50
    have hsmall : JordanTupleCongruence(m,x,x1,x2,x3,k)Definitions: JordanTupleCongruence
  2. L51
    specialize jordan_tuple_congruence_divisor (m)
  3. L52
    specialize jordan_tuple_congruence_divisor (m*n)
  4. L53
    specialize jordan_tuple_congruence_divisor (x)
  5. L54
    specialize jordan_tuple_congruence_divisor (x1)
  6. L55
    specialize jordan_tuple_congruence_divisor (x2)
  7. L56
    specialize jordan_tuple_congruence_divisor (x3)
  8. L57
    specialize jordan_tuple_congruence_divisor (k)
  9. L58
    apply jordan_tuple_congruence_divisor
14Construct an explicit witnessL59–59

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

  1. L59
    exists n
15Calculate and transport equalitiesL60–60

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

  1. L60
    refl
16Use earlier factsL61–70

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

  1. L61
    exact hnorm_witness_witness_right
  2. L62
    specialize jordan_tuple_congruence_trans (m)
  3. L63
    specialize jordan_tuple_congruence_trans (x2)
  4. L64
    specialize jordan_tuple_congruence_trans (x3)
  5. L65
    specialize jordan_tuple_congruence_trans (x)
  6. L66
    specialize jordan_tuple_congruence_trans (x1)
  7. L67
    specialize jordan_tuple_congruence_trans (b)
  8. L68
    specialize jordan_tuple_congruence_trans (c)
  9. L69
    specialize jordan_tuple_congruence_trans (k)
  10. L70
    apply jordan_tuple_congruence_trans
17Use earlier factsL71–80

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

  1. L71
    specialize jordan_tuple_congruence_symm (m)
  2. L72
    specialize jordan_tuple_congruence_symm (x)
  3. L73
    specialize jordan_tuple_congruence_symm (x1)
  4. L74
    specialize jordan_tuple_congruence_symm (x2)
  5. L75
    specialize jordan_tuple_congruence_symm (x3)
  6. L76
    specialize jordan_tuple_congruence_symm (k)
  7. L77
    apply jordan_tuple_congruence_symm
  8. L78
    exact hsmall
  9. L79
    specialize jordan_crt_tuple_left (m)
  10. L80
    specialize jordan_crt_tuple_left (n)
18Use earlier factsL81–89

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

  1. L81
    specialize jordan_crt_tuple_left (b)
  2. L82
    specialize jordan_crt_tuple_left (c)
  3. L83
    specialize jordan_crt_tuple_left (d)
  4. L84
    specialize jordan_crt_tuple_left (e)
  5. L85
    specialize jordan_crt_tuple_left (x)
  6. L86
    specialize jordan_crt_tuple_left (x1)
  7. L87
    specialize jordan_crt_tuple_left (k)
  8. L88
    apply jordan_crt_tuple_left
  9. L89
    exact hraw_witness_witness
19Establish hsmallL90–98

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple congruence divisor.

  1. L90
    have hsmall : JordanTupleCongruence(n,x,x1,x2,x3,k)Definitions: JordanTupleCongruence
  2. L91
    specialize jordan_tuple_congruence_divisor (n)
  3. L92
    specialize jordan_tuple_congruence_divisor (m*n)
  4. L93
    specialize jordan_tuple_congruence_divisor (x)
  5. L94
    specialize jordan_tuple_congruence_divisor (x1)
  6. L95
    specialize jordan_tuple_congruence_divisor (x2)
  7. L96
    specialize jordan_tuple_congruence_divisor (x3)
  8. L97
    specialize jordan_tuple_congruence_divisor (k)
  9. L98
    apply jordan_tuple_congruence_divisor
20Construct an explicit witnessL99–99

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

  1. L99
    exists m
21Use earlier factsL100–109

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

  1. L100
    specialize mul_comm (m)
  2. L101
    specialize mul_comm (n)
  3. L102
    apply mul_comm
  4. L103
    exact hnorm_witness_witness_right
  5. L104
    specialize jordan_tuple_congruence_trans (n)
  6. L105
    specialize jordan_tuple_congruence_trans (x2)
  7. L106
    specialize jordan_tuple_congruence_trans (x3)
  8. L107
    specialize jordan_tuple_congruence_trans (x)
  9. L108
    specialize jordan_tuple_congruence_trans (x1)
  10. L109
    specialize jordan_tuple_congruence_trans (d)
22Use earlier factsL110–119

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

  1. L110
    specialize jordan_tuple_congruence_trans (e)
  2. L111
    specialize jordan_tuple_congruence_trans (k)
  3. L112
    apply jordan_tuple_congruence_trans
  4. L113
    specialize jordan_tuple_congruence_symm (n)
  5. L114
    specialize jordan_tuple_congruence_symm (x)
  6. L115
    specialize jordan_tuple_congruence_symm (x1)
  7. L116
    specialize jordan_tuple_congruence_symm (x2)
  8. L117
    specialize jordan_tuple_congruence_symm (x3)
  9. L118
    specialize jordan_tuple_congruence_symm (k)
  10. L119
    apply jordan_tuple_congruence_symm
23Use earlier factsL120–129

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

  1. L120
    exact hsmall
  2. L121
    specialize jordan_crt_tuple_right (m)
  3. L122
    specialize jordan_crt_tuple_right (n)
  4. L123
    specialize jordan_crt_tuple_right (b)
  5. L124
    specialize jordan_crt_tuple_right (c)
  6. L125
    specialize jordan_crt_tuple_right (d)
  7. L126
    specialize jordan_crt_tuple_right (e)
  8. L127
    specialize jordan_crt_tuple_right (x)
  9. L128
    specialize jordan_crt_tuple_right (x1)
  10. L129
    specialize jordan_crt_tuple_right (k)
24Use earlier factsL130–131

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

  1. L130
    apply jordan_crt_tuple_right
  2. L131
    exact hraw_witness_witness

Library-wide reading audit

Original exact command ledger · 131 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro k
  8. 0008intro hm
  9. 0009intro hn
  10. 0010intro hcop
  11. 0011have hfamily : forall L. exists f g. forall jt_index_canonicalfamily. (exists jt_gap_canonicalfamilyindex. jt_gap_canonicalfamilyindex+S (jt_index_canonicalfamily)=(L)) -> exists jt_left_canonicalfamily jt_right_canonicalfamily jt_output_canonicalfamily. ((((exists fs_h_jt_canonicalfamilyleft. fs_h_jt_canonicalfamilyleft + S (jt_left_canonicalfamily) = S ((S (jt_index_canonicalfamily)) * c)) /\ exists fs_q_jt_canonicalfamilyleft. b = fs_q_jt_canonicalfamilyleft * S ((S (jt_index_canonicalfamily)) * c) + (jt_left_canonicalfamily))) /\ (((((exists fs_h_jt_canonicalfamilyright. fs_h_jt_canonicalfamilyright + S (jt_right_canonicalfamily) = S ((S (jt_index_canonicalfamily)) * e)) /\ exists fs_q_jt_canonicalfamilyright. d = fs_q_jt_canonicalfamilyright * S ((S (jt_index_canonicalfamily)) * e) + (jt_right_canonicalfamily))) /\ (((((exists fs_h_jt_canonicalfamilyoutput. fs_h_jt_canonicalfamilyoutput + S (jt_output_canonicalfamily) = S ((S (jt_index_canonicalfamily)) * g)) /\ exists fs_q_jt_canonicalfamilyoutput. f = fs_q_jt_canonicalfamilyoutput * S ((S (jt_index_canonicalfamily)) * g) + (jt_output_canonicalfamily))) /\ (((exists jt_left_canonicalfamilymodleft jt_right_canonicalfamilymodleft. (jt_output_canonicalfamily)+(m)*jt_left_canonicalfamilymodleft=(jt_left_canonicalfamily)+(m)*jt_right_canonicalfamilymodleft) /\ (exists jt_left_canonicalfamilymodright jt_right_canonicalfamilymodright. (jt_output_canonicalfamily)+(n)*jt_left_canonicalfamilymodright=(jt_right_canonicalfamily)+(n)*jt_right_canonicalfamilymodright))))))))
  12. 0012specialize jordan_crt_tuple_exists (m)
  13. 0013specialize jordan_crt_tuple_exists (n)
  14. 0014specialize jordan_crt_tuple_exists (b)
  15. 0015specialize jordan_crt_tuple_exists (c)
  16. 0016specialize jordan_crt_tuple_exists (d)
  17. 0017specialize jordan_crt_tuple_exists (e)
  18. 0018apply jordan_crt_tuple_exists
  19. 0019exact hm
  20. 0020exact hn
  21. 0021exact hcop
  22. 0022have hraw : exists f g. forall jt_index_canonicalraw. (exists jt_gap_canonicalrawindex. jt_gap_canonicalrawindex+S (jt_index_canonicalraw)=(k)) -> exists jt_left_canonicalraw jt_right_canonicalraw jt_output_canonicalraw. ((((exists fs_h_jt_canonicalrawleft. fs_h_jt_canonicalrawleft + S (jt_left_canonicalraw) = S ((S (jt_index_canonicalraw)) * c)) /\ exists fs_q_jt_canonicalrawleft. b = fs_q_jt_canonicalrawleft * S ((S (jt_index_canonicalraw)) * c) + (jt_left_canonicalraw))) /\ (((((exists fs_h_jt_canonicalrawright. fs_h_jt_canonicalrawright + S (jt_right_canonicalraw) = S ((S (jt_index_canonicalraw)) * e)) /\ exists fs_q_jt_canonicalrawright. d = fs_q_jt_canonicalrawright * S ((S (jt_index_canonicalraw)) * e) + (jt_right_canonicalraw))) /\ (((((exists fs_h_jt_canonicalrawoutput. fs_h_jt_canonicalrawoutput + S (jt_output_canonicalraw) = S ((S (jt_index_canonicalraw)) * g)) /\ exists fs_q_jt_canonicalrawoutput. f = fs_q_jt_canonicalrawoutput * S ((S (jt_index_canonicalraw)) * g) + (jt_output_canonicalraw))) /\ (((exists jt_left_canonicalrawmodleft jt_right_canonicalrawmodleft. (jt_output_canonicalraw)+(m)*jt_left_canonicalrawmodleft=(jt_left_canonicalraw)+(m)*jt_right_canonicalrawmodleft) /\ (exists jt_left_canonicalrawmodright jt_right_canonicalrawmodright. (jt_output_canonicalraw)+(n)*jt_left_canonicalrawmodright=(jt_right_canonicalraw)+(n)*jt_right_canonicalrawmodright))))))))
  23. 0023specialize hfamily (k)
  24. 0024apply hfamily
  25. 0025cases hraw
  26. 0026cases hraw_witness
  27. 0027have hproduct : ~(m*n=0)
  28. 0028intro hz
  29. 0029specialize mul_ne_zero (m)
  30. 0030specialize mul_ne_zero (n)
  31. 0031apply mul_ne_zero
  32. 0032exact hm
  33. 0033exact hn
  34. 0034exact hz
  35. 0035have hnorm : exists u v. ((forall jt_index_canonicalbound. (exists jt_gap_canonicalboundindex. jt_gap_canonicalboundindex+S (jt_index_canonicalbound)=(k)) -> exists jt_value_canonicalbound. ((((exists fs_h_jt_canonicalboundat. fs_h_jt_canonicalboundat + S (jt_value_canonicalbound) = S ((S (jt_index_canonicalbound)) * v)) /\ exists fs_q_jt_canonicalboundat. u = fs_q_jt_canonicalboundat * S ((S (jt_index_canonicalbound)) * v) + (jt_value_canonicalbound))) /\ (exists jt_gap_canonicalboundvalue. jt_gap_canonicalboundvalue+S (jt_value_canonicalbound)=(m*n)))) /\ (forall jt_index_canonicalmod jt_left_canonicalmod jt_right_canonicalmod. (exists jt_gap_canonicalmodindex. jt_gap_canonicalmodindex+S (jt_index_canonicalmod)=(k)) -> (((exists fs_h_jt_canonicalmodleft. fs_h_jt_canonicalmodleft + S (jt_left_canonicalmod) = S ((S (jt_index_canonicalmod)) * x1)) /\ exists fs_q_jt_canonicalmodleft. x = fs_q_jt_canonicalmodleft * S ((S (jt_index_canonicalmod)) * x1) + (jt_left_canonicalmod))) -> (((exists fs_h_jt_canonicalmodright. fs_h_jt_canonicalmodright + S (jt_right_canonicalmod) = S ((S (jt_index_canonicalmod)) * v)) /\ exists fs_q_jt_canonicalmodright. u = fs_q_jt_canonicalmodright * S ((S (jt_index_canonicalmod)) * v) + (jt_right_canonicalmod))) -> (exists jt_left_canonicalmodmod jt_right_canonicalmodmod. (jt_left_canonicalmod)+(m*n)*jt_left_canonicalmodmod=(jt_right_canonicalmod)+(m*n)*jt_right_canonicalmodmod)))
  36. 0036specialize jordan_tuple_normalize_exists (m*n)
  37. 0037specialize jordan_tuple_normalize_exists (x)
  38. 0038specialize jordan_tuple_normalize_exists (x1)
  39. 0039specialize jordan_tuple_normalize_exists (k)
  40. 0040apply jordan_tuple_normalize_exists
  41. 0041exact hproduct
  42. 0042cases hnorm
  43. 0043cases hnorm_witness
  44. 0044cases hnorm_witness_witness
  45. 0045exists x2
  46. 0046exists x3
  47. 0047split
  48. 0048exact hnorm_witness_witness_left
  49. 0049split
  50. 0050have hsmall : forall jt_index_canonicalsmallleft jt_left_canonicalsmallleft jt_right_canonicalsmallleft. (exists jt_gap_canonicalsmallleftindex. jt_gap_canonicalsmallleftindex+S (jt_index_canonicalsmallleft)=(k)) -> (((exists fs_h_jt_canonicalsmallleftleft. fs_h_jt_canonicalsmallleftleft + S (jt_left_canonicalsmallleft) = S ((S (jt_index_canonicalsmallleft)) * x1)) /\ exists fs_q_jt_canonicalsmallleftleft. x = fs_q_jt_canonicalsmallleftleft * S ((S (jt_index_canonicalsmallleft)) * x1) + (jt_left_canonicalsmallleft))) -> (((exists fs_h_jt_canonicalsmallleftright. fs_h_jt_canonicalsmallleftright + S (jt_right_canonicalsmallleft) = S ((S (jt_index_canonicalsmallleft)) * x3)) /\ exists fs_q_jt_canonicalsmallleftright. x2 = fs_q_jt_canonicalsmallleftright * S ((S (jt_index_canonicalsmallleft)) * x3) + (jt_right_canonicalsmallleft))) -> (exists jt_left_canonicalsmallleftmod jt_right_canonicalsmallleftmod. (jt_left_canonicalsmallleft)+(m)*jt_left_canonicalsmallleftmod=(jt_right_canonicalsmallleft)+(m)*jt_right_canonicalsmallleftmod)
  51. 0051specialize jordan_tuple_congruence_divisor (m)
  52. 0052specialize jordan_tuple_congruence_divisor (m*n)
  53. 0053specialize jordan_tuple_congruence_divisor (x)
  54. 0054specialize jordan_tuple_congruence_divisor (x1)
  55. 0055specialize jordan_tuple_congruence_divisor (x2)
  56. 0056specialize jordan_tuple_congruence_divisor (x3)
  57. 0057specialize jordan_tuple_congruence_divisor (k)
  58. 0058apply jordan_tuple_congruence_divisor
  59. 0059exists n
  60. 0060refl
  61. 0061exact hnorm_witness_witness_right
  62. 0062specialize jordan_tuple_congruence_trans (m)
  63. 0063specialize jordan_tuple_congruence_trans (x2)
  64. 0064specialize jordan_tuple_congruence_trans (x3)
  65. 0065specialize jordan_tuple_congruence_trans (x)
  66. 0066specialize jordan_tuple_congruence_trans (x1)
  67. 0067specialize jordan_tuple_congruence_trans (b)
  68. 0068specialize jordan_tuple_congruence_trans (c)
  69. 0069specialize jordan_tuple_congruence_trans (k)
  70. 0070apply jordan_tuple_congruence_trans
  71. 0071specialize jordan_tuple_congruence_symm (m)
  72. 0072specialize jordan_tuple_congruence_symm (x)
  73. 0073specialize jordan_tuple_congruence_symm (x1)
  74. 0074specialize jordan_tuple_congruence_symm (x2)
  75. 0075specialize jordan_tuple_congruence_symm (x3)
  76. 0076specialize jordan_tuple_congruence_symm (k)
  77. 0077apply jordan_tuple_congruence_symm
  78. 0078exact hsmall
  79. 0079specialize jordan_crt_tuple_left (m)
  80. 0080specialize jordan_crt_tuple_left (n)
  81. 0081specialize jordan_crt_tuple_left (b)
  82. 0082specialize jordan_crt_tuple_left (c)
  83. 0083specialize jordan_crt_tuple_left (d)
  84. 0084specialize jordan_crt_tuple_left (e)
  85. 0085specialize jordan_crt_tuple_left (x)
  86. 0086specialize jordan_crt_tuple_left (x1)
  87. 0087specialize jordan_crt_tuple_left (k)
  88. 0088apply jordan_crt_tuple_left
  89. 0089exact hraw_witness_witness
  90. 0090have hsmall : forall jt_index_canonicalsmallright jt_left_canonicalsmallright jt_right_canonicalsmallright. (exists jt_gap_canonicalsmallrightindex. jt_gap_canonicalsmallrightindex+S (jt_index_canonicalsmallright)=(k)) -> (((exists fs_h_jt_canonicalsmallrightleft. fs_h_jt_canonicalsmallrightleft + S (jt_left_canonicalsmallright) = S ((S (jt_index_canonicalsmallright)) * x1)) /\ exists fs_q_jt_canonicalsmallrightleft. x = fs_q_jt_canonicalsmallrightleft * S ((S (jt_index_canonicalsmallright)) * x1) + (jt_left_canonicalsmallright))) -> (((exists fs_h_jt_canonicalsmallrightright. fs_h_jt_canonicalsmallrightright + S (jt_right_canonicalsmallright) = S ((S (jt_index_canonicalsmallright)) * x3)) /\ exists fs_q_jt_canonicalsmallrightright. x2 = fs_q_jt_canonicalsmallrightright * S ((S (jt_index_canonicalsmallright)) * x3) + (jt_right_canonicalsmallright))) -> (exists jt_left_canonicalsmallrightmod jt_right_canonicalsmallrightmod. (jt_left_canonicalsmallright)+(n)*jt_left_canonicalsmallrightmod=(jt_right_canonicalsmallright)+(n)*jt_right_canonicalsmallrightmod)
  91. 0091specialize jordan_tuple_congruence_divisor (n)
  92. 0092specialize jordan_tuple_congruence_divisor (m*n)
  93. 0093specialize jordan_tuple_congruence_divisor (x)
  94. 0094specialize jordan_tuple_congruence_divisor (x1)
  95. 0095specialize jordan_tuple_congruence_divisor (x2)
  96. 0096specialize jordan_tuple_congruence_divisor (x3)
  97. 0097specialize jordan_tuple_congruence_divisor (k)
  98. 0098apply jordan_tuple_congruence_divisor
  99. 0099exists m
  100. 0100specialize mul_comm (m)
  101. 0101specialize mul_comm (n)
  102. 0102apply mul_comm
  103. 0103exact hnorm_witness_witness_right
  104. 0104specialize jordan_tuple_congruence_trans (n)
  105. 0105specialize jordan_tuple_congruence_trans (x2)
  106. 0106specialize jordan_tuple_congruence_trans (x3)
  107. 0107specialize jordan_tuple_congruence_trans (x)
  108. 0108specialize jordan_tuple_congruence_trans (x1)
  109. 0109specialize jordan_tuple_congruence_trans (d)
  110. 0110specialize jordan_tuple_congruence_trans (e)
  111. 0111specialize jordan_tuple_congruence_trans (k)
  112. 0112apply jordan_tuple_congruence_trans
  113. 0113specialize jordan_tuple_congruence_symm (n)
  114. 0114specialize jordan_tuple_congruence_symm (x)
  115. 0115specialize jordan_tuple_congruence_symm (x1)
  116. 0116specialize jordan_tuple_congruence_symm (x2)
  117. 0117specialize jordan_tuple_congruence_symm (x3)
  118. 0118specialize jordan_tuple_congruence_symm (k)
  119. 0119apply jordan_tuple_congruence_symm
  120. 0120exact hsmall
  121. 0121specialize jordan_crt_tuple_right (m)
  122. 0122specialize jordan_crt_tuple_right (n)
  123. 0123specialize jordan_crt_tuple_right (b)
  124. 0124specialize jordan_crt_tuple_right (c)
  125. 0125specialize jordan_crt_tuple_right (d)
  126. 0126specialize jordan_crt_tuple_right (e)
  127. 0127specialize jordan_crt_tuple_right (x)
  128. 0128specialize jordan_crt_tuple_right (x1)
  129. 0129specialize jordan_crt_tuple_right (k)
  130. 0130apply jordan_crt_tuple_right
  131. 0131exact hraw_witness_witness