Complementary divisors and finite involutions — exact evidence

Exact theorem nodes and inherited prerequisites

• DI0001 positive_divisor_quotient_exists_unique · actual bundle node 127
• DI0002 divisor_complement_exists · actual bundle node 128
• DI0003 divisor_complement_functional · actual bundle node 129
• DI0004 divisor_complement_positive_equation · actual bundle node 130
• DI0005 divisor_complement_symmetric · actual bundle node 131
• DI0006 divisor_complement_bounded · actual bundle node 132
• DI0007 divisor_complement_prefix_exists · actual bundle node 133
• DI0008 divisor_complement_prefix_lookup · actual bundle node 134
• DI0009 divisor_complement_prefix_permutation · actual bundle node 135
• DI000A positive_divisor_involution_exists · actual bundle node 136
• DI000B divisor_complement_prefix_involution · actual bundle node 137
• DI000C divisor_complement_prefix_positive_quotient · actual bundle node 138
• beta_at_unique · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall b c i x y. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x) -> ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y) -> x = y

• beta_prefix_extend · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall k b e s. exists z c. (((exists h. h + S s = S ((S k) * c)) /\ exists q. z = q * S ((S k) * c) + s) /\ forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. z = q * S ((S i) * c) + a))

• divisor_le_nonzero · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall d n. ~(n = 0) -> (exists q. n = d * q) -> exists k. k + d = n

• eq_decidable · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall a b. a = b \/ ~(a = b)

• factor_nonzero_left · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall n c d. ~(n = 0) -> n = c * d -> ~(c = 0)

• factor_nonzero_right · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall n c d. ~(n = 0) -> n = c * d -> ~(d = 0)

• factor_permutation_below_zero_impossible · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall i. (exists pfp_gap_empty. pfp_gap_empty + S (i) = (0)) -> false

• finite_bounded_injective_surjective · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall n b c. (forall fp_i_pigeon_bounded. (exists fp_gap_pigeon_bounded_index. fp_gap_pigeon_bounded_index + S fp_i_pigeon_bounded = n) -> exists fp_value_pigeon_bounded. ((((exists ff_h_pigeon_bounded_entry. ff_h_pigeon_bounded_entry + S (fp_value_pigeon_bounded) = S ((S (fp_i_pigeon_bounded)) * c)) /\ exists ff_q_pigeon_bounded_entry. b = ff_q_pigeon_bounded_entry * S ((S (fp_i_pigeon_bounded)) * c) + (fp_value_pigeon_bounded))) /\ (exists fp_gap_pigeon_bounded_value. fp_gap_pigeon_bounded_value + S fp_value_pigeon_bounded = n))) -> (forall fp_i_pigeon_injective fp_j_pigeon_injective fp_value_pigeon_injective. (exists fp_gap_pigeon_injective_i. fp_gap_pigeon_injective_i + S fp_i_pigeon_injective = n) -> (exists fp_gap_pigeon_injective_j. fp_gap_pigeon_injective_j + S fp_j_pigeon_injective = n) -> (((exists ff_h_pigeon_injective_left. ff_h_pigeon_injective_left + S (fp_value_pigeon_injective) = S ((S (fp_i_pigeon_injective)) * c)) /\ exists ff_q_pigeon_injective_left. b = ff_q_pigeon_injective_left * S ((S (fp_i_pigeon_injective)) * c) + (fp_value_pigeon_injective))) -> (((exists ff_h_pigeon_injective_right. ff_h_pigeon_injective_right + S (fp_value_pigeon_injective) = S ((S (fp_j_pigeon_injective)) * c)) /\ exists ff_q_pigeon_injective_right. b = ff_q_pigeon_injective_right * S ((S (fp_j_pigeon_injective)) * c) + (fp_value_pigeon_injective))) -> fp_i_pigeon_injective = fp_j_pigeon_injective) -> (forall fp_value_pigeon_surjective. (exists fp_gap_pigeon_surjective_value. fp_gap_pigeon_surjective_value + S fp_value_pigeon_surjective = n) -> exists fp_i_pigeon_surjective. ((exists fp_gap_pigeon_surjective_index. fp_gap_pigeon_surjective_index + S fp_i_pigeon_surjective = n) /\ (((exists ff_h_pigeon_surjective_entry. ff_h_pigeon_surjective_entry + S (fp_value_pigeon_surjective) = S ((S (fp_i_pigeon_surjective)) * c)) /\ exists ff_q_pigeon_surjective_entry. b = ff_q_pigeon_surjective_entry * S ((S (fp_i_pigeon_surjective)) * c) + (fp_value_pigeon_surjective)))))

• finite_lt_succ_eq_or_lt · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall n x. (exists h. h + S x = S n) -> x = n \/ exists h. h + S x = n

• le_of_succ_le_succ · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall a b. (exists k. k + S a = S b) -> exists r. r + a = b

• mul_comm · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall n m. n * m = m * n

• mul_left_cancel_nonzero · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall a b c. ~(a = 0) -> a * b = a * c -> b = c

• multiple_decidable_nonzero · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall d n. ~(d = 0) -> (exists q. n = d * q) \/ ~(exists q. n = d * q)

• succ_le_succ · checked inherited prerequisite
  Exact statement in the checked dependency cone

  forall a b. (exists k. k + a = b) -> exists r. r + S a = S b