PA0028

binary_crt_fold_step

Stable checked-use theorem · independently closed

One binary CRT extension preserves every old congruence whose modulus divides the accumulated product.

Exact expanded PA statement

forall P n x b. ~(P = 0) -> ~(n = 0) -> (forall d. (exists u. P = d * u) -> (exists v. n = d * v) -> d = 1) -> exists z. ((forall m a. (exists k. P = m * k) -> (exists u v. x + m * u = a + m * v) -> exists r s. z + m * r = a + m * s) /\ exists q r. z + n * q = b + n * r)

Structural proof guide

Generated structural guide

One binary CRT extension preserves every old congruence whose modulus divides the accumulated product.

Use the direct prerequisites binary_crt, mod_eq_of_mod_eq_multiple, mod_eq_trans as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (2).

Referenced ingredients

PA0026 binary_crt PA0027 mod_eq_of_mod_eq_multiple PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA0026 binary_crt PA0027 mod_eq_of_mod_eq_multiple PA0024 mod_eq_trans

Direct dependents

PA002G beta_exclusive_recode_congruence_step PA002X beta_prefix_extend

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro P
  2. 0002intro n
  3. 0003intro x
  4. 0004intro b
  5. 0005intro hP
  6. 0006intro hn
  7. 0007intro hcop
  8. 0008have hcrt : exists z. (exists u v. z + P * u = x + P * v) /\ (exists q r. z + n * q = b + n * r)
  9. 0009specialize binary_crt P
  10. 0010specialize binary_crt n
  11. 0011specialize binary_crt x
  12. 0012specialize binary_crt b
  13. 0013apply binary_crt
  14. 0014exact hP
  15. 0015exact hn
  16. 0016exact hcop
  17. 0017cases hcrt
  18. 0018cases hcrt_witness
  19. 0019exists x1
  20. 0020split
  21. 0021intro m
  22. 0022intro a
  23. 0023intro hmP
  24. 0024intro hxa
  25. 0025have hzx : exists u v. x1 + m * u = x + m * v
  26. 0026specialize mod_eq_of_mod_eq_multiple m
  27. 0027specialize mod_eq_of_mod_eq_multiple P
  28. 0028specialize mod_eq_of_mod_eq_multiple x1
  29. 0029specialize mod_eq_of_mod_eq_multiple x
  30. 0030apply mod_eq_of_mod_eq_multiple
  31. 0031exact hmP
  32. 0032exact hcrt_witness_left
  33. 0033specialize mod_eq_trans m
  34. 0034specialize mod_eq_trans x1
  35. 0035specialize mod_eq_trans x
  36. 0036specialize mod_eq_trans a
  37. 0037apply mod_eq_trans
  38. 0038exact hzx
  39. 0039exact hxa
  40. 0040exact hcrt_witness_right