BT011E

double_scaled_remainder_lift

Alpha body-checked · checked-use disabled

Compose the two bounded scaling steps used by the 521 certificate.

Exact expanded PA statement

forall d x q t s r u v. x = d * q + t -> 11 * t = d * s + r -> 2 * r + 37 = d * u + v -> 2 * (11 * x) + 37 = d * (2 * (11 * q + s) + u) + v

Structural proof guide

Compose the two bounded scaling steps used by the 521 certificate.

Direct prerequisites: scaled_remainder_lift. The authored body proceeds by intermediate claims (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT011C scaled_remainder_lift

Direct dependents

BT011N prime_five_hundred_twenty_one

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro d
  2. 0002intro x
  3. 0003intro q
  4. 0004intro t
  5. 0005intro s
  6. 0006intro r
  7. 0007intro u
  8. 0008intro v
  9. 0009intro hx
  10. 0010intro hfirst_tail
  11. 0011intro hsecond_tail
  12. 0012have hfirst : 11 * x = d * (11 * q + s) + r
  13. 0013trans 11 * x + 0
  14. 0014symm
  15. 0015apply PA3
  16. 0016specialize scaled_remainder_lift d
  17. 0017specialize scaled_remainder_lift x
  18. 0018specialize scaled_remainder_lift q
  19. 0019specialize scaled_remainder_lift t
  20. 0020specialize scaled_remainder_lift 11
  21. 0021specialize scaled_remainder_lift 0
  22. 0022specialize scaled_remainder_lift s
  23. 0023specialize scaled_remainder_lift r
  24. 0024apply scaled_remainder_lift
  25. 0025exact hx
  26. 0026rewrite PA3
  27. 0027exact hfirst_tail
  28. 0028specialize scaled_remainder_lift d
  29. 0029specialize scaled_remainder_lift (11 * x)
  30. 0030specialize scaled_remainder_lift (11 * q + s)
  31. 0031specialize scaled_remainder_lift r
  32. 0032specialize scaled_remainder_lift 2
  33. 0033specialize scaled_remainder_lift 37
  34. 0034specialize scaled_remainder_lift u
  35. 0035specialize scaled_remainder_lift v
  36. 0036apply scaled_remainder_lift
  37. 0037exact hfirst
  38. 0038exact hsecond_tail