BT00U6

primorial_factor_choice_functional

Alpha body-checked · checked-use disabled

The prime-or-one selector factor at a fixed index is unique.

Exact expanded PA statement

forall i a z. (((((~(S (i) = 1) /\ forall bpr_left_bpfcf_left_prime bpr_right_bpfcf_left_prime. S (i) = bpr_left_bpfcf_left_prime * bpr_right_bpfcf_left_prime -> bpr_left_bpfcf_left_prime = 1 \/ bpr_right_bpfcf_left_prime = 1)) /\ a = S (i)) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpfcf_left_prime bpr_right_bpfcf_left_prime. S (i) = bpr_left_bpfcf_left_prime * bpr_right_bpfcf_left_prime -> bpr_left_bpfcf_left_prime = 1 \/ bpr_right_bpfcf_left_prime = 1)) /\ a = 1))) -> (((((~(S (i) = 1) /\ forall bpr_left_bpfcf_right_prime bpr_right_bpfcf_right_prime. S (i) = bpr_left_bpfcf_right_prime * bpr_right_bpfcf_right_prime -> bpr_left_bpfcf_right_prime = 1 \/ bpr_right_bpfcf_right_prime = 1)) /\ z = S (i)) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpfcf_right_prime bpr_right_bpfcf_right_prime. S (i) = bpr_left_bpfcf_right_prime * bpr_right_bpfcf_right_prime -> bpr_left_bpfcf_right_prime = 1 \/ bpr_right_bpfcf_right_prime = 1)) /\ z = 1))) -> a = z

Structural proof guide

The prime-or-one selector factor at a fixed index is unique.

Direct prerequisites: none. The authored body proceeds by case analysis (9).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT00UW primorial_interval_factor_prefix_shift

Formal native tactic body

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

  1. 0001intro i
  2. 0002intro a
  3. 0003intro z
  4. 0004intro hleft
  5. 0005intro hright
  6. 0006cases hleft
  7. 0007cases hleft_left
  8. 0008cases hright
  9. 0009cases hright_left
  10. 0010trans S i
  11. 0011exact hleft_left_right
  12. 0012symm
  13. 0013exact hright_left_right
  14. 0014cases hright_right
  15. 0015exfalso
  16. 0016apply hright_right_left
  17. 0017exact hleft_left_left
  18. 0018cases hleft_right
  19. 0019cases hright
  20. 0020cases hright_left
  21. 0021exfalso
  22. 0022apply hleft_right_left
  23. 0023exact hright_left_left
  24. 0024cases hright_right
  25. 0025trans 1
  26. 0026exact hleft_right_right
  27. 0027symm
  28. 0028exact hright_right_right