PA00BK · theorem

scaled_pair_order_terminal_power_mod_predecessor

Alpha v34 checked-use theorem · independently closed; not Stable

A completed terminal scaled pairing sends a^h to the predecessor p-1 modulo p.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ a. ∀ n. ∀ u. ∀ v. ∀ b. ∀ c. ∀ h. ∀ A. p = S n → Prime(p) → ScaledInversePrefix(p,a,n,u,v,n) → n = h + h → (∀ x. ∀ y. ∀ z. Lt(x,h + h) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,h + h,z)) ∧ ((∀ x. Lt(x,h + h) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(b,c,h + h)) → (∀ x. Lt(x,h) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,S z))) → Pow(a,h,A) → ModEq(p,A,n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime PD0008 ModEq PD0013 BetaAt PD0020 Pow PD0025 InjectivePrefix PD0027 ContainsPrefix PD0039 ScaledInversePrefix

16 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0014 Product PD0023 Factorial PD0024 BoundedPrefix PD0025 InjectivePrefix

16 occurrences

Exact expanded native-PA statement
forall p a n u v b c h A. p = S n -> ((~(p = 1) /\ forall esi_prime_left_enr_prime esi_prime_right_enr_prime. p = esi_prime_left_enr_prime * esi_prime_right_enr_prime -> esi_prime_left_enr_prime = 1 \/ esi_prime_right_enr_prime = 1)) -> (forall esip_index_enr_prefix. (exists esip_gap_enr_prefix_prefix_bound. esip_gap_enr_prefix_prefix_bound + S (esip_index_enr_prefix) = n) -> exists esip_mate_enr_prefix. ((((exists ff_h_esip_enr_prefix_entry. ff_h_esip_enr_prefix_entry + S (esip_mate_enr_prefix) = S ((S (esip_index_enr_prefix)) * v)) /\ exists ff_q_esip_enr_prefix_entry. u = ff_q_esip_enr_prefix_entry * S ((S (esip_index_enr_prefix)) * v) + (esip_mate_enr_prefix))) /\ ((exists esip_gap_enr_prefix_relation_index_bound. esip_gap_enr_prefix_relation_index_bound + S (esip_index_enr_prefix) = n) /\ ((((~((S esip_index_enr_prefix) = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_left_bound. esip_gap_enr_prefix_relation_scaled_left_bound + S (S esip_index_enr_prefix) = p))) /\ (((~(esip_mate_enr_prefix = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_right_bound. esip_gap_enr_prefix_relation_scaled_right_bound + S (esip_mate_enr_prefix) = p))) /\ (exists esi_mod_left_enr_prefix_relation_scaled_mod esi_mod_right_enr_prefix_relation_scaled_mod. ((S esip_index_enr_prefix) * esip_mate_enr_prefix) + p * esi_mod_left_enr_prefix_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_relation_scaled_mod))))))) -> n = h + h -> (((forall espo_position_enr_terminal_state_closed espo_source_enr_terminal_state_closed espo_mate_enr_terminal_state_closed. (exists wpo_gap_enr_terminal_state_closed_position_bound. wpo_gap_enr_terminal_state_closed_position_bound + S (espo_position_enr_terminal_state_closed) = h + h) -> (((exists wpo_beta_height_enr_terminal_state_closed_source_entry. wpo_beta_height_enr_terminal_state_closed_source_entry + S (espo_source_enr_terminal_state_closed) = S ((S (espo_position_enr_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_source_entry. b = wpo_beta_quotient_enr_terminal_state_closed_source_entry * S ((S (espo_position_enr_terminal_state_closed)) * c) + (espo_source_enr_terminal_state_closed))) -> (((exists wpo_beta_height_enr_terminal_state_closed_scaled_entry. wpo_beta_height_enr_terminal_state_closed_scaled_entry + S (S espo_mate_enr_terminal_state_closed) = S ((S (espo_source_enr_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_scaled_entry. u = wpo_beta_quotient_enr_terminal_state_closed_scaled_entry * S ((S (espo_source_enr_terminal_state_closed)) * v) + (S espo_mate_enr_terminal_state_closed))) -> exists espo_mate_position_enr_terminal_state_closed. ((exists wpo_gap_enr_terminal_state_closed_mate_bound. wpo_gap_enr_terminal_state_closed_mate_bound + S (espo_mate_position_enr_terminal_state_closed) = h + h) /\ (((exists wpo_beta_height_enr_terminal_state_closed_mate_entry. wpo_beta_height_enr_terminal_state_closed_mate_entry + S (espo_mate_enr_terminal_state_closed) = S ((S (espo_mate_position_enr_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_closed_mate_entry. b = wpo_beta_quotient_enr_terminal_state_closed_mate_entry * S ((S (espo_mate_position_enr_terminal_state_closed)) * c) + (espo_mate_enr_terminal_state_closed))))) /\ (((forall fom_index_enr_terminal_state_bounded. (exists fom_gap_enr_terminal_state_bounded_index_bound. fom_gap_enr_terminal_state_bounded_index_bound + S (fom_index_enr_terminal_state_bounded) = h + h) -> exists fom_value_enr_terminal_state_bounded. ((((exists fom_beta_height_enr_terminal_state_bounded_entry. fom_beta_height_enr_terminal_state_bounded_entry + S (fom_value_enr_terminal_state_bounded) = S ((S (fom_index_enr_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_enr_terminal_state_bounded_entry. b = fom_beta_quotient_enr_terminal_state_bounded_entry * S ((S (fom_index_enr_terminal_state_bounded)) * c) + (fom_value_enr_terminal_state_bounded))) /\ (exists fom_gap_enr_terminal_state_bounded_value_bound. fom_gap_enr_terminal_state_bounded_value_bound + S (fom_value_enr_terminal_state_bounded) = n))) /\ (forall wpo_injective_left_enr_terminal_state_injective wpo_injective_right_enr_terminal_state_injective wpo_injective_value_enr_terminal_state_injective. (exists wpo_gap_enr_terminal_state_injective_left_bound. wpo_gap_enr_terminal_state_injective_left_bound + S (wpo_injective_left_enr_terminal_state_injective) = h + h) -> (exists wpo_gap_enr_terminal_state_injective_right_bound. wpo_gap_enr_terminal_state_injective_right_bound + S (wpo_injective_right_enr_terminal_state_injective) = h + h) -> (((exists wpo_beta_height_enr_terminal_state_injective_left_entry. wpo_beta_height_enr_terminal_state_injective_left_entry + S (wpo_injective_value_enr_terminal_state_injective) = S ((S (wpo_injective_left_enr_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_injective_left_entry. b = wpo_beta_quotient_enr_terminal_state_injective_left_entry * S ((S (wpo_injective_left_enr_terminal_state_injective)) * c) + (wpo_injective_value_enr_terminal_state_injective))) -> (((exists wpo_beta_height_enr_terminal_state_injective_right_entry. wpo_beta_height_enr_terminal_state_injective_right_entry + S (wpo_injective_value_enr_terminal_state_injective) = S ((S (wpo_injective_right_enr_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_enr_terminal_state_injective_right_entry. b = wpo_beta_quotient_enr_terminal_state_injective_right_entry * S ((S (wpo_injective_right_enr_terminal_state_injective)) * c) + (wpo_injective_value_enr_terminal_state_injective))) -> wpo_injective_left_enr_terminal_state_injective = wpo_injective_right_enr_terminal_state_injective))))) -> (forall espi_pair_enr_history. (exists wpo_gap_enr_history_pair_bound. wpo_gap_enr_history_pair_bound + S (espi_pair_enr_history) = h) -> exists espi_left_enr_history espi_right_enr_history. (((((exists wpo_beta_height_enr_history_left_entry. wpo_beta_height_enr_history_left_entry + S (espi_left_enr_history) = S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c)) /\ exists wpo_beta_quotient_enr_history_left_entry. b = wpo_beta_quotient_enr_history_left_entry * S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c) + (espi_left_enr_history))) /\ (((((exists wpo_beta_height_enr_history_right_entry. wpo_beta_height_enr_history_right_entry + S (espi_right_enr_history) = S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c)) /\ exists wpo_beta_quotient_enr_history_right_entry. b = wpo_beta_quotient_enr_history_right_entry * S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c) + (espi_right_enr_history))) /\ (((exists wpo_beta_height_enr_history_scaled_edge. wpo_beta_height_enr_history_scaled_edge + S (S espi_right_enr_history) = S ((S (espi_left_enr_history)) * v)) /\ exists wpo_beta_quotient_enr_history_scaled_edge. u = wpo_beta_quotient_enr_history_scaled_edge * S ((S (espi_left_enr_history)) * v) + (S espi_right_enr_history)))))))) -> (exists ff_b_enr_terminal_power ff_c_enr_terminal_power. ((forall ff_i_enr_terminal_power_repeat. (exists ff_lt_enr_terminal_power_repeat_bound. ff_lt_enr_terminal_power_repeat_bound + S ff_i_enr_terminal_power_repeat = h) -> (((exists ff_h_enr_terminal_power_repeat_decoded. ff_h_enr_terminal_power_repeat_decoded + S (a) = S ((S (ff_i_enr_terminal_power_repeat)) * ff_c_enr_terminal_power)) /\ exists ff_q_enr_terminal_power_repeat_decoded. ff_b_enr_terminal_power = ff_q_enr_terminal_power_repeat_decoded * S ((S (ff_i_enr_terminal_power_repeat)) * ff_c_enr_terminal_power) + (a)))) /\ (exists ff_u_enr_terminal_power_product ff_v_enr_terminal_power_product. ((((exists ff_h_enr_terminal_power_product_start. ff_h_enr_terminal_power_product_start + S (1) = S ((S (0)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_start. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_start * S ((S (0)) * ff_v_enr_terminal_power_product) + (1))) /\ ((((exists ff_h_enr_terminal_power_product_terminal. ff_h_enr_terminal_power_product_terminal + S (A) = S ((S (h)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_terminal. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_terminal * S ((S (h)) * ff_v_enr_terminal_power_product) + (A))) /\ forall ff_i_enr_terminal_power_product. (exists ff_lt_enr_terminal_power_product_bound. ff_lt_enr_terminal_power_product_bound + S ff_i_enr_terminal_power_product = h) -> exists ff_p_enr_terminal_power_product ff_r_enr_terminal_power_product ff_s_enr_terminal_power_product. ((((exists ff_h_enr_terminal_power_product_factor. ff_h_enr_terminal_power_product_factor + S (ff_p_enr_terminal_power_product) = S ((S (ff_i_enr_terminal_power_product)) * ff_c_enr_terminal_power)) /\ exists ff_q_enr_terminal_power_product_factor. ff_b_enr_terminal_power = ff_q_enr_terminal_power_product_factor * S ((S (ff_i_enr_terminal_power_product)) * ff_c_enr_terminal_power) + (ff_p_enr_terminal_power_product))) /\ ((((exists ff_h_enr_terminal_power_product_partial. ff_h_enr_terminal_power_product_partial + S (ff_r_enr_terminal_power_product) = S ((S (ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_partial. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_partial * S ((S (ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product) + (ff_r_enr_terminal_power_product))) /\ ((((exists ff_h_enr_terminal_power_product_successor. ff_h_enr_terminal_power_product_successor + S (ff_s_enr_terminal_power_product) = S ((S (S ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product)) /\ exists ff_q_enr_terminal_power_product_successor. ff_u_enr_terminal_power_product = ff_q_enr_terminal_power_product_successor * S ((S (S ff_i_enr_terminal_power_product)) * ff_v_enr_terminal_power_product) + (ff_s_enr_terminal_power_product))) /\ ff_s_enr_terminal_power_product = ff_r_enr_terminal_power_product * ff_p_enr_terminal_power_product)))))))) -> (exists wpp_mod_left_enr_terminal_result wpp_mod_right_enr_terminal_result. (A) + p * wpp_mod_left_enr_terminal_result = (n) + p * wpp_mod_right_enr_terminal_result)

Proof neighborhood

Direct theorem prerequisites

PA008C beta_successor_lift_exists PA009X scaled_pair_order_successor_lift_adjacent_targets PA003X beta_product_exists PA00A0 beta_adjacent_target_pairs_product_power PA0060 factorial_exists PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00BJ prime_factorial_wilson_congruence PA003L mod_eq_symm PA0024 mod_eq_trans

Direct theorem dependents

PA00BL scaled_inverse_nonresidue_half_power_mod_predecessor

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

114 script commands · 22 reading checkpoints · 12 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (9)
beta successor lift existsscaled pair order successor lift adjacent targetsbeta product existsbeta adjacent target pairs product powerfactorial existsscaled pair order successor lift product is factorialprime factorial wilson congruencemod eq symmmod eq trans
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro u
  5. L5
    intro v
  6. L6
    intro b
  7. L7
    intro c
  8. L8
    intro h
  9. L9
    intro A
  10. L10
    intro hpn
02Fix variables and assumptionsL11–16

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hp
  2. L12
    intro hprefix
  3. L13
    intro heven
  4. L14
    intro hstate
  5. L15
    intro hhistory
  6. L16
    intro hpower
03Separate the logical casesL17–18

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L17
    cases hstate
  2. L18
    cases hstate_right
04Establish hlift_existsL19–23

Establish this local claim before using it. It is not an additional assumption.

  1. L19
    have hlift_exists : ∃ f. ∃ g. ∀ x. ∀ y. Lt(x,n) → BetaAt(b,c,x,y) → BetaAt(f,g,x,S y)Definitions: Lt(x,n)BetaAt(b,c,x,y)BetaAt(f,g,x,S y)Original native command in the exact edition
  2. L20
    specialize beta_successor_lift_exists b
  3. L21
    specialize beta_successor_lift_exists c
  4. L22
    specialize beta_successor_lift_exists n
  5. L23
    exact beta_successor_lift_exists
05Separate the logical casesL24–25

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L24
    cases hlift_exists
  2. L25
    cases hlift_exists_witness
06Establish hpairsL26–35

Establish this local claim before using it. It is not an additional assumption.

  1. L26
    have hpairs : ∀ wpp_pair_enr_target_pairs_x. ∀ wpp_left_enr_target_pairs_x. ∀ wpp_right_enr_target_pairs_x. Lt(wpp_pair_enr_target_pairs_x,h) → BetaAt(x,x1,wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x,wpp_left_enr_target_pairs_x) → BetaAt(x,x1,S (wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x),wpp_right_enr_target_pairs_x) → ModEq(p,wpp_left_enr_target_pairs_x · wpp_right_enr_target_pairs_x,a)Definitions: Lt(wpp_pair_enr_target_pairs_x,h)BetaAt(x,x1,wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x,wpp_left_enr_target_pairs_x)BetaAt(x,x1,S (wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x),wpp_right_enr_target_pairs_x)ModEq(p,wpp_left_enr_target_pairs_x · wpp_right_enr_target_pairs_x,a)Original native command in the exact edition
  2. L27
    specialize scaled_pair_order_successor_lift_adjacent_targets p
  3. L28
    specialize scaled_pair_order_successor_lift_adjacent_targets a
  4. L29
    specialize scaled_pair_order_successor_lift_adjacent_targets n
  5. L30
    specialize scaled_pair_order_successor_lift_adjacent_targets u
  6. L31
    specialize scaled_pair_order_successor_lift_adjacent_targets v
  7. L32
    specialize scaled_pair_order_successor_lift_adjacent_targets b
  8. L33
    specialize scaled_pair_order_successor_lift_adjacent_targets c
  9. L34
    specialize scaled_pair_order_successor_lift_adjacent_targets x
  10. L35
    specialize scaled_pair_order_successor_lift_adjacent_targets x1
07Use earlier factsL36–42

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L36
    specialize scaled_pair_order_successor_lift_adjacent_targets h
  2. L37
    apply scaled_pair_order_successor_lift_adjacent_targets
  3. L38
    exact heven
  4. L39
    exact hprefix
  5. L40
    exact hstate_right_left
  6. L41
    exact hhistory
  7. L42
    exact hlift_exists_witness_witness
08Establish hproduct_existsL43–47

Establish this local claim before using it. It is not an additional assumption.

  1. L43
    have hproduct_exists : ∃ Q. Product(x,x1,n,Q)Definitions: Product(x,x1,n,Q)Original native command in the exact edition
  2. L44
    specialize beta_product_exists x
  3. L45
    specialize beta_product_exists x1
  4. L46
    specialize beta_product_exists n
  5. L47
    exact beta_product_exists
09Separate the logical casesL48–48

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L48
    cases hproduct_exists
10Establish hproduct_evenL49–53

Establish this local claim before using it. It is not an additional assumption.

  1. L49
    have hproduct_even : Product(x,x1,h + h,x2)Definitions: Product(x,x1,h + h,x2)Original native command in the exact edition
  2. L50
    rewrite <- heven
  3. L51
    rewrite <- heven
  4. L52
    rewrite <- heven
  5. L53
    exact hproduct_exists_witness
11Establish hproduct_powerL54–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta adjacent target pairs product power.

  1. L54
    have hproduct_power : ModEq(p,x2,A)Definitions: ModEq(p,x2,A)Original native command in the exact edition
  2. L55
    specialize beta_adjacent_target_pairs_product_power p
  3. L56
    specialize beta_adjacent_target_pairs_product_power a
  4. L57
    specialize beta_adjacent_target_pairs_product_power x
  5. L58
    specialize beta_adjacent_target_pairs_product_power x1
  6. L59
    specialize beta_adjacent_target_pairs_product_power h
  7. L60
    specialize beta_adjacent_target_pairs_product_power x2
  8. L61
    specialize beta_adjacent_target_pairs_product_power A
  9. L62
    apply beta_adjacent_target_pairs_product_power
  10. L63
    exact hpairs
12Use earlier factsL64–65

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L64
    exact hproduct_even
  2. L65
    exact hpower
13Establish hfactorial_existsL66–68

Establish this local claim before using it. It is not an additional assumption.

  1. L66
    have hfactorial_exists : ∃ F. Factorial(n,F)Definitions: Factorial(n,F)Original native command in the exact edition
  2. L67
    specialize factorial_exists n
  3. L68
    exact factorial_exists
14Separate the logical casesL69–69

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L69
    cases hfactorial_exists
15Establish hbounded_nL70–72

Establish this local claim before using it. It is not an additional assumption.

  1. L70
    have hbounded_n : BoundedPrefix(b,c,n)Definitions: BoundedPrefix(b,c,n)Original native command in the exact edition
  2. L71
    rewrite heven
  3. L72
    exact hstate_right_left
16Establish hinjective_nL73–76

Establish this local claim before using it. It is not an additional assumption.

  1. L73
    have hinjective_n : InjectivePrefix(b,c,n)Definitions: InjectivePrefix(b,c,n)Original native command in the exact edition
  2. L74
    rewrite heven
  3. L75
    rewrite heven
  4. L76
    exact hstate_right_right
17Establish hQFL77–86

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled pair order successor lift product is factorial.

  1. L77
    have hQF : x2 = x3
  2. L78
    specialize scaled_pair_order_successor_lift_product_is_factorial b
  3. L79
    specialize scaled_pair_order_successor_lift_product_is_factorial c
  4. L80
    specialize scaled_pair_order_successor_lift_product_is_factorial x
  5. L81
    specialize scaled_pair_order_successor_lift_product_is_factorial x1
  6. L82
    specialize scaled_pair_order_successor_lift_product_is_factorial n
  7. L83
    specialize scaled_pair_order_successor_lift_product_is_factorial x2
  8. L84
    specialize scaled_pair_order_successor_lift_product_is_factorial x3
  9. L85
    apply scaled_pair_order_successor_lift_product_is_factorial
  10. L86
    exact hbounded_n
18Use earlier factsL87–90

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L87
    exact hinjective_n
  2. L88
    exact hlift_exists_witness_witness
  3. L89
    exact hproduct_exists_witness
  4. L90
    exact hfactorial_exists_witness
19Establish hpower_productL91–96

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L91
    have hpower_product : ModEq(p,A,x2)Definitions: ModEq(p,A,x2)Original native command in the exact edition
  2. L92
    specialize mod_eq_symm p
  3. L93
    specialize mod_eq_symm x2
  4. L94
    specialize mod_eq_symm A
  5. L95
    apply mod_eq_symm
  6. L96
    exact hproduct_power
20Establish hpower_factorialL97–99

Establish this local claim before using it. It is not an additional assumption.

  1. L97
    have hpower_factorial : ModEq(p,A,x3)Definitions: ModEq(p,A,x3)Original native command in the exact edition
  2. L98
    rewrite <- hQF
  3. L99
    exact hpower_product
21Establish hfactorial_modL100–109

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime factorial wilson congruence.

  1. L100
    have hfactorial_mod : ModEq(p,x3,n)Definitions: ModEq(p,x3,n)Original native command in the exact edition
  2. L101
    specialize prime_factorial_wilson_congruence p
  3. L102
    specialize prime_factorial_wilson_congruence n
  4. L103
    specialize prime_factorial_wilson_congruence x3
  5. L104
    apply prime_factorial_wilson_congruence
  6. L105
    exact hpn
  7. L106
    exact hp
  8. L107
    exact hfactorial_exists_witness
  9. L108
    specialize mod_eq_trans p
  10. L109
    specialize mod_eq_trans A
22Use earlier factsL110–114

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L110
    specialize mod_eq_trans x3
  2. L111
    specialize mod_eq_trans n
  3. L112
    apply mod_eq_trans
  4. L113
    exact hpower_factorial
  5. L114
    exact hfactorial_mod

Library-wide reading audit

Original defined command ledger · 114 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro b
  7. 0007intro c
  8. 0008intro h
  9. 0009intro A
  10. 0010intro hpn
  11. 0011intro hp
  12. 0012intro hprefix
  13. 0013intro heven
  14. 0014intro hstate
  15. 0015intro hhistory
  16. 0016intro hpower
  17. 0017cases hstate
  18. 0018cases hstate_right
  19. 0019have hlift_exists : ∃ f. ∃ g. ∀ x. ∀ y. Lt(x,n) → BetaAt(b,c,x,y) → BetaAt(f,g,x,S y)
    Exact native replay linehave hlift_exists : exists f g. (forall wsl_index_enr_lift_n wsl_value_enr_lift_n. (exists wpo_gap_enr_lift_n_bound. wpo_gap_enr_lift_n_bound + S (wsl_index_enr_lift_n) = n) -> (((exists wpo_beta_height_enr_lift_n_source. wpo_beta_height_enr_lift_n_source + S (wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * c)) /\ exists wpo_beta_quotient_enr_lift_n_source. b = wpo_beta_quotient_enr_lift_n_source * S ((S (wsl_index_enr_lift_n)) * c) + (wsl_value_enr_lift_n))) -> (((exists wpo_beta_height_enr_lift_n_target. wpo_beta_height_enr_lift_n_target + S (S wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * g)) /\ exists wpo_beta_quotient_enr_lift_n_target. f = wpo_beta_quotient_enr_lift_n_target * S ((S (wsl_index_enr_lift_n)) * g) + (S wsl_value_enr_lift_n))))
  20. 0020specialize beta_successor_lift_exists b
  21. 0021specialize beta_successor_lift_exists c
  22. 0022specialize beta_successor_lift_exists n
  23. 0023exact beta_successor_lift_exists
  24. 0024cases hlift_exists
  25. 0025cases hlift_exists_witness
  26. 0026have hpairs : ∀ wpp_pair_enr_target_pairs_x. ∀ wpp_left_enr_target_pairs_x. ∀ wpp_right_enr_target_pairs_x. Lt(wpp_pair_enr_target_pairs_x,h) → BetaAt(x,x1,wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x,wpp_left_enr_target_pairs_x) → BetaAt(x,x1,S (wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x),wpp_right_enr_target_pairs_x) → ModEq(p,wpp_left_enr_target_pairs_x · wpp_right_enr_target_pairs_x,a)
    Exact native replay linehave hpairs : forall wpp_pair_enr_target_pairs_x wpp_left_enr_target_pairs_x wpp_right_enr_target_pairs_x. (exists wpp_gap_enr_target_pairs_x_pair_bound. wpp_gap_enr_target_pairs_x_pair_bound + S (wpp_pair_enr_target_pairs_x) = h) -> (((exists wpp_beta_height_enr_target_pairs_x_left_entry. wpp_beta_height_enr_target_pairs_x_left_entry + S (wpp_left_enr_target_pairs_x) = S ((S ((wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x))) * x1)) /\ exists wpp_beta_quotient_enr_target_pairs_x_left_entry. x = wpp_beta_quotient_enr_target_pairs_x_left_entry * S ((S ((wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x))) * x1) + (wpp_left_enr_target_pairs_x))) -> (((exists wpp_beta_height_enr_target_pairs_x_right_entry. wpp_beta_height_enr_target_pairs_x_right_entry + S (wpp_right_enr_target_pairs_x) = S ((S (S (wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x))) * x1)) /\ exists wpp_beta_quotient_enr_target_pairs_x_right_entry. x = wpp_beta_quotient_enr_target_pairs_x_right_entry * S ((S (S (wpp_pair_enr_target_pairs_x + wpp_pair_enr_target_pairs_x))) * x1) + (wpp_right_enr_target_pairs_x))) -> (exists wpp_mod_left_enr_target_pairs_x_pair_mod wpp_mod_right_enr_target_pairs_x_pair_mod. (wpp_left_enr_target_pairs_x * wpp_right_enr_target_pairs_x) + p * wpp_mod_left_enr_target_pairs_x_pair_mod = (a) + p * wpp_mod_right_enr_target_pairs_x_pair_mod)
  27. 0027specialize scaled_pair_order_successor_lift_adjacent_targets p
  28. 0028specialize scaled_pair_order_successor_lift_adjacent_targets a
  29. 0029specialize scaled_pair_order_successor_lift_adjacent_targets n
  30. 0030specialize scaled_pair_order_successor_lift_adjacent_targets u
  31. 0031specialize scaled_pair_order_successor_lift_adjacent_targets v
  32. 0032specialize scaled_pair_order_successor_lift_adjacent_targets b
  33. 0033specialize scaled_pair_order_successor_lift_adjacent_targets c
  34. 0034specialize scaled_pair_order_successor_lift_adjacent_targets x
  35. 0035specialize scaled_pair_order_successor_lift_adjacent_targets x1
  36. 0036specialize scaled_pair_order_successor_lift_adjacent_targets h
  37. 0037apply scaled_pair_order_successor_lift_adjacent_targets
  38. 0038exact heven
  39. 0039exact hprefix
  40. 0040exact hstate_right_left
  41. 0041exact hhistory
  42. 0042exact hlift_exists_witness_witness
  43. 0043have hproduct_exists : ∃ Q. Product(x,x1,n,Q)
    Exact native replay linehave hproduct_exists : exists Q. exists ff_u_enr_terminal_product_x ff_v_enr_terminal_product_x. ((((exists ff_h_enr_terminal_product_x_start. ff_h_enr_terminal_product_x_start + S (1) = S ((S (0)) * ff_v_enr_terminal_product_x)) /\ exists ff_q_enr_terminal_product_x_start. ff_u_enr_terminal_product_x = ff_q_enr_terminal_product_x_start * S ((S (0)) * ff_v_enr_terminal_product_x) + (1))) /\ ((((exists ff_h_enr_terminal_product_x_terminal. ff_h_enr_terminal_product_x_terminal + S (Q) = S ((S (n)) * ff_v_enr_terminal_product_x)) /\ exists ff_q_enr_terminal_product_x_terminal. ff_u_enr_terminal_product_x = ff_q_enr_terminal_product_x_terminal * S ((S (n)) * ff_v_enr_terminal_product_x) + (Q))) /\ forall ff_i_enr_terminal_product_x. (exists ff_lt_enr_terminal_product_x_bound. ff_lt_enr_terminal_product_x_bound + S ff_i_enr_terminal_product_x = n) -> exists ff_p_enr_terminal_product_x ff_r_enr_terminal_product_x ff_s_enr_terminal_product_x. ((((exists ff_h_enr_terminal_product_x_factor. ff_h_enr_terminal_product_x_factor + S (ff_p_enr_terminal_product_x) = S ((S (ff_i_enr_terminal_product_x)) * x1)) /\ exists ff_q_enr_terminal_product_x_factor. x = ff_q_enr_terminal_product_x_factor * S ((S (ff_i_enr_terminal_product_x)) * x1) + (ff_p_enr_terminal_product_x))) /\ ((((exists ff_h_enr_terminal_product_x_partial. ff_h_enr_terminal_product_x_partial + S (ff_r_enr_terminal_product_x) = S ((S (ff_i_enr_terminal_product_x)) * ff_v_enr_terminal_product_x)) /\ exists ff_q_enr_terminal_product_x_partial. ff_u_enr_terminal_product_x = ff_q_enr_terminal_product_x_partial * S ((S (ff_i_enr_terminal_product_x)) * ff_v_enr_terminal_product_x) + (ff_r_enr_terminal_product_x))) /\ ((((exists ff_h_enr_terminal_product_x_successor. ff_h_enr_terminal_product_x_successor + S (ff_s_enr_terminal_product_x) = S ((S (S ff_i_enr_terminal_product_x)) * ff_v_enr_terminal_product_x)) /\ exists ff_q_enr_terminal_product_x_successor. ff_u_enr_terminal_product_x = ff_q_enr_terminal_product_x_successor * S ((S (S ff_i_enr_terminal_product_x)) * ff_v_enr_terminal_product_x) + (ff_s_enr_terminal_product_x))) /\ ff_s_enr_terminal_product_x = ff_r_enr_terminal_product_x * ff_p_enr_terminal_product_x)))))
  44. 0044specialize beta_product_exists x
  45. 0045specialize beta_product_exists x1
  46. 0046specialize beta_product_exists n
  47. 0047exact beta_product_exists
  48. 0048cases hproduct_exists
  49. 0049have hproduct_even : Product(x,x1,h + h,x2)
    Exact native replay linehave hproduct_even : exists ff_u_enr_terminal_product_even ff_v_enr_terminal_product_even. ((((exists ff_h_enr_terminal_product_even_start. ff_h_enr_terminal_product_even_start + S (1) = S ((S (0)) * ff_v_enr_terminal_product_even)) /\ exists ff_q_enr_terminal_product_even_start. ff_u_enr_terminal_product_even = ff_q_enr_terminal_product_even_start * S ((S (0)) * ff_v_enr_terminal_product_even) + (1))) /\ ((((exists ff_h_enr_terminal_product_even_terminal. ff_h_enr_terminal_product_even_terminal + S (x2) = S ((S (h + h)) * ff_v_enr_terminal_product_even)) /\ exists ff_q_enr_terminal_product_even_terminal. ff_u_enr_terminal_product_even = ff_q_enr_terminal_product_even_terminal * S ((S (h + h)) * ff_v_enr_terminal_product_even) + (x2))) /\ forall ff_i_enr_terminal_product_even. (exists ff_lt_enr_terminal_product_even_bound. ff_lt_enr_terminal_product_even_bound + S ff_i_enr_terminal_product_even = h + h) -> exists ff_p_enr_terminal_product_even ff_r_enr_terminal_product_even ff_s_enr_terminal_product_even. ((((exists ff_h_enr_terminal_product_even_factor. ff_h_enr_terminal_product_even_factor + S (ff_p_enr_terminal_product_even) = S ((S (ff_i_enr_terminal_product_even)) * x1)) /\ exists ff_q_enr_terminal_product_even_factor. x = ff_q_enr_terminal_product_even_factor * S ((S (ff_i_enr_terminal_product_even)) * x1) + (ff_p_enr_terminal_product_even))) /\ ((((exists ff_h_enr_terminal_product_even_partial. ff_h_enr_terminal_product_even_partial + S (ff_r_enr_terminal_product_even) = S ((S (ff_i_enr_terminal_product_even)) * ff_v_enr_terminal_product_even)) /\ exists ff_q_enr_terminal_product_even_partial. ff_u_enr_terminal_product_even = ff_q_enr_terminal_product_even_partial * S ((S (ff_i_enr_terminal_product_even)) * ff_v_enr_terminal_product_even) + (ff_r_enr_terminal_product_even))) /\ ((((exists ff_h_enr_terminal_product_even_successor. ff_h_enr_terminal_product_even_successor + S (ff_s_enr_terminal_product_even) = S ((S (S ff_i_enr_terminal_product_even)) * ff_v_enr_terminal_product_even)) /\ exists ff_q_enr_terminal_product_even_successor. ff_u_enr_terminal_product_even = ff_q_enr_terminal_product_even_successor * S ((S (S ff_i_enr_terminal_product_even)) * ff_v_enr_terminal_product_even) + (ff_s_enr_terminal_product_even))) /\ ff_s_enr_terminal_product_even = ff_r_enr_terminal_product_even * ff_p_enr_terminal_product_even)))))
  50. 0050rewrite <- heven
  51. 0051rewrite <- heven
  52. 0052rewrite <- heven
  53. 0053exact hproduct_exists_witness
  54. 0054have hproduct_power : ModEq(p,x2,A)
    Exact native replay linehave hproduct_power : exists wpp_mod_left_enr_product_mod_power wpp_mod_right_enr_product_mod_power. (x2) + p * wpp_mod_left_enr_product_mod_power = (A) + p * wpp_mod_right_enr_product_mod_power
  55. 0055specialize beta_adjacent_target_pairs_product_power p
  56. 0056specialize beta_adjacent_target_pairs_product_power a
  57. 0057specialize beta_adjacent_target_pairs_product_power x
  58. 0058specialize beta_adjacent_target_pairs_product_power x1
  59. 0059specialize beta_adjacent_target_pairs_product_power h
  60. 0060specialize beta_adjacent_target_pairs_product_power x2
  61. 0061specialize beta_adjacent_target_pairs_product_power A
  62. 0062apply beta_adjacent_target_pairs_product_power
  63. 0063exact hpairs
  64. 0064exact hproduct_even
  65. 0065exact hpower
  66. 0066have hfactorial_exists : ∃ F. Factorial(n,F)
    Exact native replay linehave hfactorial_exists : exists F. (exists ff_b_enr_terminal_factorial ff_c_enr_terminal_factorial. ((forall ff_i_enr_terminal_factorial_range. (exists ff_lt_enr_terminal_factorial_range_bound. ff_lt_enr_terminal_factorial_range_bound + S ff_i_enr_terminal_factorial_range = n) -> (((exists ff_h_enr_terminal_factorial_range_decoded. ff_h_enr_terminal_factorial_range_decoded + S (1 + ff_i_enr_terminal_factorial_range) = S ((S (ff_i_enr_terminal_factorial_range)) * ff_c_enr_terminal_factorial)) /\ exists ff_q_enr_terminal_factorial_range_decoded. ff_b_enr_terminal_factorial = ff_q_enr_terminal_factorial_range_decoded * S ((S (ff_i_enr_terminal_factorial_range)) * ff_c_enr_terminal_factorial) + (1 + ff_i_enr_terminal_factorial_range)))) /\ (exists ff_u_enr_terminal_factorial_product ff_v_enr_terminal_factorial_product. ((((exists ff_h_enr_terminal_factorial_product_start. ff_h_enr_terminal_factorial_product_start + S (1) = S ((S (0)) * ff_v_enr_terminal_factorial_product)) /\ exists ff_q_enr_terminal_factorial_product_start. ff_u_enr_terminal_factorial_product = ff_q_enr_terminal_factorial_product_start * S ((S (0)) * ff_v_enr_terminal_factorial_product) + (1))) /\ ((((exists ff_h_enr_terminal_factorial_product_terminal. ff_h_enr_terminal_factorial_product_terminal + S (F) = S ((S (n)) * ff_v_enr_terminal_factorial_product)) /\ exists ff_q_enr_terminal_factorial_product_terminal. ff_u_enr_terminal_factorial_product = ff_q_enr_terminal_factorial_product_terminal * S ((S (n)) * ff_v_enr_terminal_factorial_product) + (F))) /\ forall ff_i_enr_terminal_factorial_product. (exists ff_lt_enr_terminal_factorial_product_bound. ff_lt_enr_terminal_factorial_product_bound + S ff_i_enr_terminal_factorial_product = n) -> exists ff_p_enr_terminal_factorial_product ff_r_enr_terminal_factorial_product ff_s_enr_terminal_factorial_product. ((((exists ff_h_enr_terminal_factorial_product_factor. ff_h_enr_terminal_factorial_product_factor + S (ff_p_enr_terminal_factorial_product) = S ((S (ff_i_enr_terminal_factorial_product)) * ff_c_enr_terminal_factorial)) /\ exists ff_q_enr_terminal_factorial_product_factor. ff_b_enr_terminal_factorial = ff_q_enr_terminal_factorial_product_factor * S ((S (ff_i_enr_terminal_factorial_product)) * ff_c_enr_terminal_factorial) + (ff_p_enr_terminal_factorial_product))) /\ ((((exists ff_h_enr_terminal_factorial_product_partial. ff_h_enr_terminal_factorial_product_partial + S (ff_r_enr_terminal_factorial_product) = S ((S (ff_i_enr_terminal_factorial_product)) * ff_v_enr_terminal_factorial_product)) /\ exists ff_q_enr_terminal_factorial_product_partial. ff_u_enr_terminal_factorial_product = ff_q_enr_terminal_factorial_product_partial * S ((S (ff_i_enr_terminal_factorial_product)) * ff_v_enr_terminal_factorial_product) + (ff_r_enr_terminal_factorial_product))) /\ ((((exists ff_h_enr_terminal_factorial_product_successor. ff_h_enr_terminal_factorial_product_successor + S (ff_s_enr_terminal_factorial_product) = S ((S (S ff_i_enr_terminal_factorial_product)) * ff_v_enr_terminal_factorial_product)) /\ exists ff_q_enr_terminal_factorial_product_successor. ff_u_enr_terminal_factorial_product = ff_q_enr_terminal_factorial_product_successor * S ((S (S ff_i_enr_terminal_factorial_product)) * ff_v_enr_terminal_factorial_product) + (ff_s_enr_terminal_factorial_product))) /\ ff_s_enr_terminal_factorial_product = ff_r_enr_terminal_factorial_product * ff_p_enr_terminal_factorial_product))))))))
  67. 0067specialize factorial_exists n
  68. 0068exact factorial_exists
  69. 0069cases hfactorial_exists
  70. 0070have hbounded_n : BoundedPrefix(b,c,n)
    Exact native replay linehave hbounded_n : forall fom_index_enr_generic_bounded. (exists fom_gap_enr_generic_bounded_index_bound. fom_gap_enr_generic_bounded_index_bound + S (fom_index_enr_generic_bounded) = n) -> exists fom_value_enr_generic_bounded. ((((exists fom_beta_height_enr_generic_bounded_entry. fom_beta_height_enr_generic_bounded_entry + S (fom_value_enr_generic_bounded) = S ((S (fom_index_enr_generic_bounded)) * c)) /\ exists fom_beta_quotient_enr_generic_bounded_entry. b = fom_beta_quotient_enr_generic_bounded_entry * S ((S (fom_index_enr_generic_bounded)) * c) + (fom_value_enr_generic_bounded))) /\ (exists fom_gap_enr_generic_bounded_value_bound. fom_gap_enr_generic_bounded_value_bound + S (fom_value_enr_generic_bounded) = n))
  71. 0071rewrite heven
  72. 0072exact hstate_right_left
  73. 0073have hinjective_n : InjectivePrefix(b,c,n)
    Exact native replay linehave hinjective_n : forall wpo_injective_left_enr_generic_injective wpo_injective_right_enr_generic_injective wpo_injective_value_enr_generic_injective. (exists wpo_gap_enr_generic_injective_left_bound. wpo_gap_enr_generic_injective_left_bound + S (wpo_injective_left_enr_generic_injective) = n) -> (exists wpo_gap_enr_generic_injective_right_bound. wpo_gap_enr_generic_injective_right_bound + S (wpo_injective_right_enr_generic_injective) = n) -> (((exists wpo_beta_height_enr_generic_injective_left_entry. wpo_beta_height_enr_generic_injective_left_entry + S (wpo_injective_value_enr_generic_injective) = S ((S (wpo_injective_left_enr_generic_injective)) * c)) /\ exists wpo_beta_quotient_enr_generic_injective_left_entry. b = wpo_beta_quotient_enr_generic_injective_left_entry * S ((S (wpo_injective_left_enr_generic_injective)) * c) + (wpo_injective_value_enr_generic_injective))) -> (((exists wpo_beta_height_enr_generic_injective_right_entry. wpo_beta_height_enr_generic_injective_right_entry + S (wpo_injective_value_enr_generic_injective) = S ((S (wpo_injective_right_enr_generic_injective)) * c)) /\ exists wpo_beta_quotient_enr_generic_injective_right_entry. b = wpo_beta_quotient_enr_generic_injective_right_entry * S ((S (wpo_injective_right_enr_generic_injective)) * c) + (wpo_injective_value_enr_generic_injective))) -> wpo_injective_left_enr_generic_injective = wpo_injective_right_enr_generic_injective
  74. 0074rewrite heven
  75. 0075rewrite heven
  76. 0076exact hstate_right_right
  77. 0077have hQF : x2 = x3
  78. 0078specialize scaled_pair_order_successor_lift_product_is_factorial b
  79. 0079specialize scaled_pair_order_successor_lift_product_is_factorial c
  80. 0080specialize scaled_pair_order_successor_lift_product_is_factorial x
  81. 0081specialize scaled_pair_order_successor_lift_product_is_factorial x1
  82. 0082specialize scaled_pair_order_successor_lift_product_is_factorial n
  83. 0083specialize scaled_pair_order_successor_lift_product_is_factorial x2
  84. 0084specialize scaled_pair_order_successor_lift_product_is_factorial x3
  85. 0085apply scaled_pair_order_successor_lift_product_is_factorial
  86. 0086exact hbounded_n
  87. 0087exact hinjective_n
  88. 0088exact hlift_exists_witness_witness
  89. 0089exact hproduct_exists_witness
  90. 0090exact hfactorial_exists_witness
  91. 0091have hpower_product : ModEq(p,A,x2)
    Exact native replay linehave hpower_product : exists wpp_mod_left_enr_power_mod_product wpp_mod_right_enr_power_mod_product. (A) + p * wpp_mod_left_enr_power_mod_product = (x2) + p * wpp_mod_right_enr_power_mod_product
  92. 0092specialize mod_eq_symm p
  93. 0093specialize mod_eq_symm x2
  94. 0094specialize mod_eq_symm A
  95. 0095apply mod_eq_symm
  96. 0096exact hproduct_power
  97. 0097have hpower_factorial : ModEq(p,A,x3)
    Exact native replay linehave hpower_factorial : exists wpp_mod_left_enr_power_mod_factorial wpp_mod_right_enr_power_mod_factorial. (A) + p * wpp_mod_left_enr_power_mod_factorial = (x3) + p * wpp_mod_right_enr_power_mod_factorial
  98. 0098rewrite <- hQF
  99. 0099exact hpower_product
  100. 0100have hfactorial_mod : ModEq(p,x3,n)
    Exact native replay linehave hfactorial_mod : exists wpp_mod_left_enr_factorial_mod_predecessor wpp_mod_right_enr_factorial_mod_predecessor. (x3) + p * wpp_mod_left_enr_factorial_mod_predecessor = (n) + p * wpp_mod_right_enr_factorial_mod_predecessor
  101. 0101specialize prime_factorial_wilson_congruence p
  102. 0102specialize prime_factorial_wilson_congruence n
  103. 0103specialize prime_factorial_wilson_congruence x3
  104. 0104apply prime_factorial_wilson_congruence
  105. 0105exact hpn
  106. 0106exact hp
  107. 0107exact hfactorial_exists_witness
  108. 0108specialize mod_eq_trans p
  109. 0109specialize mod_eq_trans A
  110. 0110specialize mod_eq_trans x3
  111. 0111specialize mod_eq_trans n
  112. 0112apply mod_eq_trans
  113. 0113exact hpower_factorial
  114. 0114exact hfactorial_mod