BT00VE

primorial_interval_pairwise_coprime

Alpha body-checked · checked-use disabled

Distinct positions in an interval decode coprime selector factors.

Exact expanded PA statement

forall a b c l. (forall bpr_index_bpipc_source. (exists bpr_gap_bpipc_source_bound. bpr_gap_bpipc_source_bound + S (bpr_index_bpipc_source) = l) -> exists bpr_value_bpipc_source. ((((exists bpr_height_bpipc_source_decoded. bpr_height_bpipc_source_decoded + S (bpr_value_bpipc_source) = S ((S (bpr_index_bpipc_source)) * c)) /\ exists bpr_quotient_bpipc_source_decoded. b = bpr_quotient_bpipc_source_decoded * S ((S (bpr_index_bpipc_source)) * c) + (bpr_value_bpipc_source))) /\ (((((~(S (a + bpr_index_bpipc_source) = 1) /\ forall bpr_left_bpipc_source_choice_prime bpr_right_bpipc_source_choice_prime. S (a + bpr_index_bpipc_source) = bpr_left_bpipc_source_choice_prime * bpr_right_bpipc_source_choice_prime -> bpr_left_bpipc_source_choice_prime = 1 \/ bpr_right_bpipc_source_choice_prime = 1)) /\ bpr_value_bpipc_source = S (a + bpr_index_bpipc_source)) \/ (~((~(S (a + bpr_index_bpipc_source) = 1) /\ forall bpr_left_bpipc_source_choice_prime bpr_right_bpipc_source_choice_prime. S (a + bpr_index_bpipc_source) = bpr_left_bpipc_source_choice_prime * bpr_right_bpipc_source_choice_prime -> bpr_left_bpipc_source_choice_prime = 1 \/ bpr_right_bpipc_source_choice_prime = 1)) /\ bpr_value_bpipc_source = 1))))) -> (forall bpr_left_index_bpipc_result bpr_right_index_bpipc_result bpr_left_value_bpipc_result bpr_right_value_bpipc_result. (exists bpr_gap_bpipc_result_left_bound. bpr_gap_bpipc_result_left_bound + S (bpr_left_index_bpipc_result) = l) -> (exists bpr_gap_bpipc_result_right_bound. bpr_gap_bpipc_result_right_bound + S (bpr_right_index_bpipc_result) = l) -> (((exists bpr_height_bpipc_result_left_at. bpr_height_bpipc_result_left_at + S (bpr_left_value_bpipc_result) = S ((S (bpr_left_index_bpipc_result)) * c)) /\ exists bpr_quotient_bpipc_result_left_at. b = bpr_quotient_bpipc_result_left_at * S ((S (bpr_left_index_bpipc_result)) * c) + (bpr_left_value_bpipc_result))) -> (((exists bpr_height_bpipc_result_right_at. bpr_height_bpipc_result_right_at + S (bpr_right_value_bpipc_result) = S ((S (bpr_right_index_bpipc_result)) * c)) /\ exists bpr_quotient_bpipc_result_right_at. b = bpr_quotient_bpipc_result_right_at * S ((S (bpr_right_index_bpipc_result)) * c) + (bpr_right_value_bpipc_result))) -> ~(bpr_left_index_bpipc_result = bpr_right_index_bpipc_result) -> (forall bpr_coprime_divisor_bpipc_result_coprime. (exists bpr_coprime_left_factor_bpipc_result_coprime. bpr_left_value_bpipc_result = bpr_coprime_divisor_bpipc_result_coprime * bpr_coprime_left_factor_bpipc_result_coprime) -> (exists bpr_coprime_right_factor_bpipc_result_coprime. bpr_right_value_bpipc_result = bpr_coprime_divisor_bpipc_result_coprime * bpr_coprime_right_factor_bpipc_result_coprime) -> bpr_coprime_divisor_bpipc_result_coprime = 1))

Structural proof guide

Distinct positions in an interval decode coprime selector factors.

Direct prerequisites: beta_at_unique, add_left_cancel, distinct_primes_coprime, coprime_one_left, coprime_one_right. The authored body proceeds by case analysis (15), intermediate claims (10), equality transport (7).

Proof neighborhood

Direct dependencies

BT0042 beta_at_unique BT000V add_left_cancel BT008S distinct_primes_coprime BT002Y coprime_one_left BT002X coprime_one_right

Direct dependents

BT00VF primorial_interval_divides_choose_between

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro hprefix
  6. 0006intro i
  7. 0007intro j
  8. 0008intro p
  9. 0009intro q
  10. 0010intro hi
  11. 0011intro hj
  12. 0012intro hp
  13. 0013intro hq
  14. 0014intro hij
  15. 0015have hleft : exists x. (((exists bpr_height_bpipc_left_entry. bpr_height_bpipc_left_entry + S (x) = S ((S (i)) * c)) /\ exists bpr_quotient_bpipc_left_entry. b = bpr_quotient_bpipc_left_entry * S ((S (i)) * c) + (x))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpipc_left_choice_prime bpr_right_bpipc_left_choice_prime. S (a + i) = bpr_left_bpipc_left_choice_prime * bpr_right_bpipc_left_choice_prime -> bpr_left_bpipc_left_choice_prime = 1 \/ bpr_right_bpipc_left_choice_prime = 1)) /\ x = S (a + i)) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpipc_left_choice_prime bpr_right_bpipc_left_choice_prime. S (a + i) = bpr_left_bpipc_left_choice_prime * bpr_right_bpipc_left_choice_prime -> bpr_left_bpipc_left_choice_prime = 1 \/ bpr_right_bpipc_left_choice_prime = 1)) /\ x = 1)))
  16. 0016apply hprefix
  17. 0017exact hi
  18. 0018cases hleft
  19. 0019cases hleft_witness
  20. 0020have hright : exists x1. (((exists bpr_height_bpipc_right_entry. bpr_height_bpipc_right_entry + S (x1) = S ((S (j)) * c)) /\ exists bpr_quotient_bpipc_right_entry. b = bpr_quotient_bpipc_right_entry * S ((S (j)) * c) + (x1))) /\ (((((~(S (a + j) = 1) /\ forall bpr_left_bpipc_right_choice_prime bpr_right_bpipc_right_choice_prime. S (a + j) = bpr_left_bpipc_right_choice_prime * bpr_right_bpipc_right_choice_prime -> bpr_left_bpipc_right_choice_prime = 1 \/ bpr_right_bpipc_right_choice_prime = 1)) /\ x1 = S (a + j)) \/ (~((~(S (a + j) = 1) /\ forall bpr_left_bpipc_right_choice_prime bpr_right_bpipc_right_choice_prime. S (a + j) = bpr_left_bpipc_right_choice_prime * bpr_right_bpipc_right_choice_prime -> bpr_left_bpipc_right_choice_prime = 1 \/ bpr_right_bpipc_right_choice_prime = 1)) /\ x1 = 1)))
  21. 0021apply hprefix
  22. 0022exact hj
  23. 0023cases hright
  24. 0024cases hright_witness
  25. 0025have hxp : x = p
  26. 0026specialize beta_at_unique b
  27. 0027specialize beta_at_unique c
  28. 0028specialize beta_at_unique i
  29. 0029specialize beta_at_unique x
  30. 0030specialize beta_at_unique p
  31. 0031apply beta_at_unique
  32. 0032exact hleft_witness_left
  33. 0033exact hp
  34. 0034have hxq : x1 = q
  35. 0035specialize beta_at_unique b
  36. 0036specialize beta_at_unique c
  37. 0037specialize beta_at_unique j
  38. 0038specialize beta_at_unique x1
  39. 0039specialize beta_at_unique q
  40. 0040apply beta_at_unique
  41. 0041exact hright_witness_left
  42. 0042exact hq
  43. 0043cases hleft_witness_right
  44. 0044cases hright_witness_right
  45. 0045cases hleft_witness_right_left
  46. 0046cases hright_witness_right_left
  47. 0047have hp_candidate : p = S (a + i)
  48. 0048trans x
  49. 0049symm
  50. 0050exact hxp
  51. 0051exact hleft_witness_right_left_right
  52. 0052have hq_candidate : q = S (a + j)
  53. 0053trans x1
  54. 0054symm
  55. 0055exact hxq
  56. 0056exact hright_witness_right_left_right
  57. 0057specialize distinct_primes_coprime p
  58. 0058specialize distinct_primes_coprime q
  59. 0059apply distinct_primes_coprime
  60. 0060rewrite hp_candidate
  61. 0061rewrite hp_candidate
  62. 0062exact hleft_witness_right_left_left
  63. 0063rewrite hq_candidate
  64. 0064rewrite hq_candidate
  65. 0065exact hright_witness_right_left_left
  66. 0066intro hpq
  67. 0067apply hij
  68. 0068specialize add_left_cancel a
  69. 0069specialize add_left_cancel i
  70. 0070specialize add_left_cancel j
  71. 0071apply add_left_cancel
  72. 0072apply PA2
  73. 0073trans p
  74. 0074symm
  75. 0075exact hp_candidate
  76. 0076trans q
  77. 0077exact hpq
  78. 0078exact hq_candidate
  79. 0079cases hleft_witness_right_left
  80. 0080cases hright_witness_right_right
  81. 0081have hp_candidate : p = S (a + i)
  82. 0082trans x
  83. 0083symm
  84. 0084exact hxp
  85. 0085exact hleft_witness_right_left_right
  86. 0086have hq_one : q = 1
  87. 0087trans x1
  88. 0088symm
  89. 0089exact hxq
  90. 0090exact hright_witness_right_right_right
  91. 0091rewrite hq_one
  92. 0092specialize coprime_one_right p
  93. 0093exact coprime_one_right
  94. 0094cases hright_witness_right
  95. 0095cases hleft_witness_right_right
  96. 0096cases hright_witness_right_left
  97. 0097have hp_one : p = 1
  98. 0098trans x
  99. 0099symm
  100. 0100exact hxp
  101. 0101exact hleft_witness_right_right_right
  102. 0102rewrite hp_one
  103. 0103specialize coprime_one_left q
  104. 0104exact coprime_one_left
  105. 0105cases hleft_witness_right_right
  106. 0106cases hright_witness_right_right
  107. 0107have hp_one : p = 1
  108. 0108trans x
  109. 0109symm
  110. 0110exact hxp
  111. 0111exact hleft_witness_right_right_right
  112. 0112rewrite hp_one
  113. 0113specialize coprime_one_left q
  114. 0114exact coprime_one_left