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
∀ b. ∀ c. ∀ l. ∀ n. ∀ z. (∀ x. ∀ y. ∀ m. ∀ k. Lt(x,l) → Lt(y,l) → BetaAt(b,c,x,m) → BetaAt(b,c,y,k) → ¬x = y → Coprime(m,k)) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → Dvd(y,z)) → Product(b,c,l,n) → Dvd(n,z)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
10 occurrences
In local proof propositions
19 occurrences
Exact expanded native-PA statement
forall b c l n z. (forall bpr_left_index_bpcpdcm_pairwise bpr_right_index_bpcpdcm_pairwise bpr_left_value_bpcpdcm_pairwise bpr_right_value_bpcpdcm_pairwise. (exists bpr_gap_bpcpdcm_pairwise_left_bound. bpr_gap_bpcpdcm_pairwise_left_bound + S (bpr_left_index_bpcpdcm_pairwise) = l) -> (exists bpr_gap_bpcpdcm_pairwise_right_bound. bpr_gap_bpcpdcm_pairwise_right_bound + S (bpr_right_index_bpcpdcm_pairwise) = l) -> (((exists bpr_height_bpcpdcm_pairwise_left_at. bpr_height_bpcpdcm_pairwise_left_at + S (bpr_left_value_bpcpdcm_pairwise) = S ((S (bpr_left_index_bpcpdcm_pairwise)) * c)) /\ exists bpr_quotient_bpcpdcm_pairwise_left_at. b = bpr_quotient_bpcpdcm_pairwise_left_at * S ((S (bpr_left_index_bpcpdcm_pairwise)) * c) + (bpr_left_value_bpcpdcm_pairwise))) -> (((exists bpr_height_bpcpdcm_pairwise_right_at. bpr_height_bpcpdcm_pairwise_right_at + S (bpr_right_value_bpcpdcm_pairwise) = S ((S (bpr_right_index_bpcpdcm_pairwise)) * c)) /\ exists bpr_quotient_bpcpdcm_pairwise_right_at. b = bpr_quotient_bpcpdcm_pairwise_right_at * S ((S (bpr_right_index_bpcpdcm_pairwise)) * c) + (bpr_right_value_bpcpdcm_pairwise))) -> ~(bpr_left_index_bpcpdcm_pairwise = bpr_right_index_bpcpdcm_pairwise) -> (forall bpr_coprime_divisor_bpcpdcm_pairwise_coprime. (exists bpr_coprime_left_factor_bpcpdcm_pairwise_coprime. bpr_left_value_bpcpdcm_pairwise = bpr_coprime_divisor_bpcpdcm_pairwise_coprime * bpr_coprime_left_factor_bpcpdcm_pairwise_coprime) -> (exists bpr_coprime_right_factor_bpcpdcm_pairwise_coprime. bpr_right_value_bpcpdcm_pairwise = bpr_coprime_divisor_bpcpdcm_pairwise_coprime * bpr_coprime_right_factor_bpcpdcm_pairwise_coprime) -> bpr_coprime_divisor_bpcpdcm_pairwise_coprime = 1)) -> (forall bpr_divisor_index_bpcpdcm_pointwise bpr_divisor_value_bpcpdcm_pointwise. (exists bpr_gap_bpcpdcm_pointwise_index_bound. bpr_gap_bpcpdcm_pointwise_index_bound + S (bpr_divisor_index_bpcpdcm_pointwise) = l) -> (((exists bpr_height_bpcpdcm_pointwise_decoded. bpr_height_bpcpdcm_pointwise_decoded + S (bpr_divisor_value_bpcpdcm_pointwise) = S ((S (bpr_divisor_index_bpcpdcm_pointwise)) * c)) /\ exists bpr_quotient_bpcpdcm_pointwise_decoded. b = bpr_quotient_bpcpdcm_pointwise_decoded * S ((S (bpr_divisor_index_bpcpdcm_pointwise)) * c) + (bpr_divisor_value_bpcpdcm_pointwise))) -> exists bpr_quotient_bpcpdcm_pointwise_result. z = bpr_divisor_value_bpcpdcm_pointwise * bpr_quotient_bpcpdcm_pointwise_result) -> (exists ff_u_bpcpdcm_source ff_v_bpcpdcm_source. ((((exists ff_h_bpcpdcm_source_start. ff_h_bpcpdcm_source_start + S (1) = S ((S (0)) * ff_v_bpcpdcm_source)) /\ exists ff_q_bpcpdcm_source_start. ff_u_bpcpdcm_source = ff_q_bpcpdcm_source_start * S ((S (0)) * ff_v_bpcpdcm_source) + (1))) /\ ((((exists ff_h_bpcpdcm_source_terminal. ff_h_bpcpdcm_source_terminal + S (n) = S ((S (l)) * ff_v_bpcpdcm_source)) /\ exists ff_q_bpcpdcm_source_terminal. ff_u_bpcpdcm_source = ff_q_bpcpdcm_source_terminal * S ((S (l)) * ff_v_bpcpdcm_source) + (n))) /\ forall ff_i_bpcpdcm_source. (exists ff_lt_bpcpdcm_source_bound. ff_lt_bpcpdcm_source_bound + S ff_i_bpcpdcm_source = l) -> exists ff_p_bpcpdcm_source ff_r_bpcpdcm_source ff_s_bpcpdcm_source. ((((exists ff_h_bpcpdcm_source_factor. ff_h_bpcpdcm_source_factor + S (ff_p_bpcpdcm_source) = S ((S (ff_i_bpcpdcm_source)) * c)) /\ exists ff_q_bpcpdcm_source_factor. b = ff_q_bpcpdcm_source_factor * S ((S (ff_i_bpcpdcm_source)) * c) + (ff_p_bpcpdcm_source))) /\ ((((exists ff_h_bpcpdcm_source_partial. ff_h_bpcpdcm_source_partial + S (ff_r_bpcpdcm_source) = S ((S (ff_i_bpcpdcm_source)) * ff_v_bpcpdcm_source)) /\ exists ff_q_bpcpdcm_source_partial. ff_u_bpcpdcm_source = ff_q_bpcpdcm_source_partial * S ((S (ff_i_bpcpdcm_source)) * ff_v_bpcpdcm_source) + (ff_r_bpcpdcm_source))) /\ ((((exists ff_h_bpcpdcm_source_successor. ff_h_bpcpdcm_source_successor + S (ff_s_bpcpdcm_source) = S ((S (S ff_i_bpcpdcm_source)) * ff_v_bpcpdcm_source)) /\ exists ff_q_bpcpdcm_source_successor. ff_u_bpcpdcm_source = ff_q_bpcpdcm_source_successor * S ((S (S ff_i_bpcpdcm_source)) * ff_v_bpcpdcm_source) + (ff_s_bpcpdcm_source))) /\ ff_s_bpcpdcm_source = ff_r_bpcpdcm_source * ff_p_bpcpdcm_source)))))) -> (exists bpr_quotient_bpcpdcm_result. z = (n) * bpr_quotient_bpcpdcm_result)Proof neighborhood
Direct theorem prerequisites
BT005I beta_product_zero BT005J beta_product_succ_decompose BT0018 le_succ BT000E le_refl BT0027 one_multiple BT001B lt_irrefl_expanded BT00DH beta_product_pointwise_coprime BT00BG coprime_product_is_lcmDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
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.
Named ingredients (8)
01Fix variables and assumptionsL1–2
02Induction on lL3–8
03Establish hnL9–18
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product zero.
04Fix variables and assumptionsL19–22
05Establish hdecompositionL23–29
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.
- L23
have hdecomposition : ∃ p. ∃ r. BetaAt(b,c,l,p) ∧ (Product(b,c,l,r) ∧ n = r · p)Definitions: BetaAt(b,c,l,p)Product(b,c,l,r)Original native command in the exact edition - L24
specialize beta_product_succ_decompose b - L25
specialize beta_product_succ_decompose c - L26
specialize beta_product_succ_decompose l - L27
specialize beta_product_succ_decompose n - L28
apply beta_product_succ_decompose - L29
exact hproduct
06Separate the logical casesL30–33
07Establish hprefix_pairwiseL34–43
Establish this local claim before using it. It is not an additional assumption.
- L34Definitions: Lt(bpr_left_index_bpcpdcm_prefix_pairwise,l)Lt(bpr_right_index_bpcpdcm_prefix_pairwise,l)BetaAt(b,c,bpr_left_index_bpcpdcm_prefix_pairwise,bpr_left_value_bpcpdcm_prefix_pairwise)BetaAt(b,c,bpr_right_index_bpcpdcm_prefix_pairwise,bpr_right_value_bpcpdcm_prefix_pairwise)Coprime(bpr_left_value_bpcpdcm_prefix_pairwise,bpr_right_value_bpcpdcm_prefix_pairwise)Original native command in the exact edition
have hprefix_pairwise · expand full local formula (646 characters)
have hprefix_pairwise : ∀ bpr_left_index_bpcpdcm_prefix_pairwise. ∀ bpr_right_index_bpcpdcm_prefix_pairwise. ∀ bpr_left_value_bpcpdcm_prefix_pairwise. ∀ bpr_right_value_bpcpdcm_prefix_pairwise. Lt(bpr_left_index_bpcpdcm_prefix_pairwise,l) → Lt(bpr_right_index_bpcpdcm_prefix_pairwise,l) → BetaAt(b,c,bpr_left_index_bpcpdcm_prefix_pairwise,bpr_left_value_bpcpdcm_prefix_pairwise) → BetaAt(b,c,bpr_right_index_bpcpdcm_prefix_pairwise,bpr_right_value_bpcpdcm_prefix_pairwise) → ¬bpr_left_index_bpcpdcm_prefix_pairwise = bpr_right_index_bpcpdcm_prefix_pairwise → Coprime(bpr_left_value_bpcpdcm_prefix_pairwise,bpr_right_value_bpcpdcm_prefix_pairwise) - L35
intro i - L36
intro j - L37
intro p - L38
intro q - L39
intro hi - L40
intro hj - L41
intro hp - L42
intro hq - L43
intro hij
08Use earlier factsL44–53
Instantiate or apply named facts and discharge the corresponding proof obligations.
09Use earlier factsL54–59
10Establish hprefix_pointwiseL60–69
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hpointwise.
- L60
have hprefix_pointwise : ∀ bpr_divisor_index_bpcpdcm_prefix_pointwise. ∀ bpr_divisor_value_bpcpdcm_prefix_pointwise. Lt(bpr_divisor_index_bpcpdcm_prefix_pointwise,l) → BetaAt(b,c,bpr_divisor_index_bpcpdcm_prefix_pointwise,bpr_divisor_value_bpcpdcm_prefix_pointwise) → Dvd(bpr_divisor_value_bpcpdcm_prefix_pointwise,z)Definitions: Lt(bpr_divisor_index_bpcpdcm_prefix_pointwise,l)BetaAt(b,c,bpr_divisor_index_bpcpdcm_prefix_pointwise,bpr_divisor_value_bpcpdcm_prefix_pointwise)Dvd(bpr_divisor_value_bpcpdcm_prefix_pointwise,z)Original native command in the exact edition - L61
intro i - L62
intro p - L63
intro hi - L64
intro hp - L65
specialize hpointwise i - L66
specialize hpointwise p - L67
apply hpointwise - L68
specialize le_succ (S i) - L69
specialize le_succ l
11Use earlier factsL70–72
12Establish hprefix_dividesL73–79
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
13Establish hlast_dividesL80–86
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hpointwise.
14Establish hcoprimeL87–96
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product pointwise coprime.
- L87
- L88
specialize beta_product_pointwise_coprime x - L89
specialize beta_product_pointwise_coprime b - L90
specialize beta_product_pointwise_coprime c - L91
specialize beta_product_pointwise_coprime l - L92
specialize beta_product_pointwise_coprime x1 - L93
apply beta_product_pointwise_coprime - L94
intro i - L95
intro q - L96
intro hi
15Fix variables and assumptionsL97–97
Work with arbitrary variables or the premises of the current implication.
- L97
intro hq
16Use earlier factsL98–107
Instantiate or apply named facts and discharge the corresponding proof obligations.
17Use earlier factsL108–110
18Fix variables and assumptionsL111–111
Work with arbitrary variables or the premises of the current implication.
- L111
intro hil
19Calculate and transport equalitiesL112–112
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L112
rewrite hil at hi
20Use earlier factsL113–116
21Establish hlcmL117–121
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply coprime product is lcm.
- L117
have hlcm : Dvd(x1,x1 · x) ∧ Dvd(x,x1 · x) ∧ (∀ y. Dvd(x1,y) → Dvd(x,y) → Dvd(x1 · x,y))Definitions: Dvd(x1,x1 · x)Dvd(x,x1 · x)Dvd(x1,y)Dvd(x,y)Dvd(x1 · x,y)Original native command in the exact edition - L118
specialize coprime_product_is_lcm x1 - L119
specialize coprime_product_is_lcm x - L120
apply coprime_product_is_lcm - L121
exact hcoprime
22Separate the logical casesL122–123
23Establish hresultL124–130
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hlcm right.
Original defined command ledger · 130 lines
- 0001
intro b - 0002
intro c - 0003
induction l - 0004
intro n - 0005
intro z - 0006
intro hpairwise - 0007
intro hpointwise - 0008
intro hproduct - 0009
have hn : n = 1 - 0010
specialize beta_product_zero b - 0011
specialize beta_product_zero c - 0012
specialize beta_product_zero n - 0013
apply beta_product_zero - 0014
exact hproduct - 0015
rewrite hn - 0016
specialize one_multiple z - 0017
exact one_multiple - 0018
intro n - 0019
intro z - 0020
intro hpairwise - 0021
intro hpointwise - 0022
intro hproduct - 0023
have hdecomposition : ∃ p. ∃ r. BetaAt(b,c,l,p) ∧ (Product(b,c,l,r) ∧ n = r · p)Exact native replay line
have hdecomposition : exists p r. (((exists bpr_height_bpcpdcm_last. bpr_height_bpcpdcm_last + S (p) = S ((S (l)) * c)) /\ exists bpr_quotient_bpcpdcm_last. b = bpr_quotient_bpcpdcm_last * S ((S (l)) * c) + (p))) /\ ((exists ff_u_bpcpdcm_prefix ff_v_bpcpdcm_prefix. ((((exists ff_h_bpcpdcm_prefix_start. ff_h_bpcpdcm_prefix_start + S (1) = S ((S (0)) * ff_v_bpcpdcm_prefix)) /\ exists ff_q_bpcpdcm_prefix_start. ff_u_bpcpdcm_prefix = ff_q_bpcpdcm_prefix_start * S ((S (0)) * ff_v_bpcpdcm_prefix) + (1))) /\ ((((exists ff_h_bpcpdcm_prefix_terminal. ff_h_bpcpdcm_prefix_terminal + S (r) = S ((S (l)) * ff_v_bpcpdcm_prefix)) /\ exists ff_q_bpcpdcm_prefix_terminal. ff_u_bpcpdcm_prefix = ff_q_bpcpdcm_prefix_terminal * S ((S (l)) * ff_v_bpcpdcm_prefix) + (r))) /\ forall ff_i_bpcpdcm_prefix. (exists ff_lt_bpcpdcm_prefix_bound. ff_lt_bpcpdcm_prefix_bound + S ff_i_bpcpdcm_prefix = l) -> exists ff_p_bpcpdcm_prefix ff_r_bpcpdcm_prefix ff_s_bpcpdcm_prefix. ((((exists ff_h_bpcpdcm_prefix_factor. ff_h_bpcpdcm_prefix_factor + S (ff_p_bpcpdcm_prefix) = S ((S (ff_i_bpcpdcm_prefix)) * c)) /\ exists ff_q_bpcpdcm_prefix_factor. b = ff_q_bpcpdcm_prefix_factor * S ((S (ff_i_bpcpdcm_prefix)) * c) + (ff_p_bpcpdcm_prefix))) /\ ((((exists ff_h_bpcpdcm_prefix_partial. ff_h_bpcpdcm_prefix_partial + S (ff_r_bpcpdcm_prefix) = S ((S (ff_i_bpcpdcm_prefix)) * ff_v_bpcpdcm_prefix)) /\ exists ff_q_bpcpdcm_prefix_partial. ff_u_bpcpdcm_prefix = ff_q_bpcpdcm_prefix_partial * S ((S (ff_i_bpcpdcm_prefix)) * ff_v_bpcpdcm_prefix) + (ff_r_bpcpdcm_prefix))) /\ ((((exists ff_h_bpcpdcm_prefix_successor. ff_h_bpcpdcm_prefix_successor + S (ff_s_bpcpdcm_prefix) = S ((S (S ff_i_bpcpdcm_prefix)) * ff_v_bpcpdcm_prefix)) /\ exists ff_q_bpcpdcm_prefix_successor. ff_u_bpcpdcm_prefix = ff_q_bpcpdcm_prefix_successor * S ((S (S ff_i_bpcpdcm_prefix)) * ff_v_bpcpdcm_prefix) + (ff_s_bpcpdcm_prefix))) /\ ff_s_bpcpdcm_prefix = ff_r_bpcpdcm_prefix * ff_p_bpcpdcm_prefix)))))) /\ n = r * p) - 0024
specialize beta_product_succ_decompose b - 0025
specialize beta_product_succ_decompose c - 0026
specialize beta_product_succ_decompose l - 0027
specialize beta_product_succ_decompose n - 0028
apply beta_product_succ_decompose - 0029
exact hproduct - 0030
cases hdecomposition - 0031
cases hdecomposition_witness - 0032
cases hdecomposition_witness_witness - 0033
cases hdecomposition_witness_witness_right - 0034
have hprefix_pairwise : ∀ bpr_left_index_bpcpdcm_prefix_pairwise. ∀ bpr_right_index_bpcpdcm_prefix_pairwise. ∀ bpr_left_value_bpcpdcm_prefix_pairwise. ∀ bpr_right_value_bpcpdcm_prefix_pairwise. Lt(bpr_left_index_bpcpdcm_prefix_pairwise,l) → Lt(bpr_right_index_bpcpdcm_prefix_pairwise,l) → BetaAt(b,c,bpr_left_index_bpcpdcm_prefix_pairwise,bpr_left_value_bpcpdcm_prefix_pairwise) → BetaAt(b,c,bpr_right_index_bpcpdcm_prefix_pairwise,bpr_right_value_bpcpdcm_prefix_pairwise) → ¬bpr_left_index_bpcpdcm_prefix_pairwise = bpr_right_index_bpcpdcm_prefix_pairwise → Coprime(bpr_left_value_bpcpdcm_prefix_pairwise,bpr_right_value_bpcpdcm_prefix_pairwise)Exact native replay line
have hprefix_pairwise : forall bpr_left_index_bpcpdcm_prefix_pairwise bpr_right_index_bpcpdcm_prefix_pairwise bpr_left_value_bpcpdcm_prefix_pairwise bpr_right_value_bpcpdcm_prefix_pairwise. (exists bpr_gap_bpcpdcm_prefix_pairwise_left_bound. bpr_gap_bpcpdcm_prefix_pairwise_left_bound + S (bpr_left_index_bpcpdcm_prefix_pairwise) = l) -> (exists bpr_gap_bpcpdcm_prefix_pairwise_right_bound. bpr_gap_bpcpdcm_prefix_pairwise_right_bound + S (bpr_right_index_bpcpdcm_prefix_pairwise) = l) -> (((exists bpr_height_bpcpdcm_prefix_pairwise_left_at. bpr_height_bpcpdcm_prefix_pairwise_left_at + S (bpr_left_value_bpcpdcm_prefix_pairwise) = S ((S (bpr_left_index_bpcpdcm_prefix_pairwise)) * c)) /\ exists bpr_quotient_bpcpdcm_prefix_pairwise_left_at. b = bpr_quotient_bpcpdcm_prefix_pairwise_left_at * S ((S (bpr_left_index_bpcpdcm_prefix_pairwise)) * c) + (bpr_left_value_bpcpdcm_prefix_pairwise))) -> (((exists bpr_height_bpcpdcm_prefix_pairwise_right_at. bpr_height_bpcpdcm_prefix_pairwise_right_at + S (bpr_right_value_bpcpdcm_prefix_pairwise) = S ((S (bpr_right_index_bpcpdcm_prefix_pairwise)) * c)) /\ exists bpr_quotient_bpcpdcm_prefix_pairwise_right_at. b = bpr_quotient_bpcpdcm_prefix_pairwise_right_at * S ((S (bpr_right_index_bpcpdcm_prefix_pairwise)) * c) + (bpr_right_value_bpcpdcm_prefix_pairwise))) -> ~(bpr_left_index_bpcpdcm_prefix_pairwise = bpr_right_index_bpcpdcm_prefix_pairwise) -> (forall bpr_coprime_divisor_bpcpdcm_prefix_pairwise_coprime. (exists bpr_coprime_left_factor_bpcpdcm_prefix_pairwise_coprime. bpr_left_value_bpcpdcm_prefix_pairwise = bpr_coprime_divisor_bpcpdcm_prefix_pairwise_coprime * bpr_coprime_left_factor_bpcpdcm_prefix_pairwise_coprime) -> (exists bpr_coprime_right_factor_bpcpdcm_prefix_pairwise_coprime. bpr_right_value_bpcpdcm_prefix_pairwise = bpr_coprime_divisor_bpcpdcm_prefix_pairwise_coprime * bpr_coprime_right_factor_bpcpdcm_prefix_pairwise_coprime) -> bpr_coprime_divisor_bpcpdcm_prefix_pairwise_coprime = 1) - 0035
intro i - 0036
intro j - 0037
intro p - 0038
intro q - 0039
intro hi - 0040
intro hj - 0041
intro hp - 0042
intro hq - 0043
intro hij - 0044
specialize hpairwise i - 0045
specialize hpairwise j - 0046
specialize hpairwise p - 0047
specialize hpairwise q - 0048
apply hpairwise - 0049
specialize le_succ (S i) - 0050
specialize le_succ l - 0051
apply le_succ - 0052
exact hi - 0053
specialize le_succ (S j) - 0054
specialize le_succ l - 0055
apply le_succ - 0056
exact hj - 0057
exact hp - 0058
exact hq - 0059
exact hij - 0060
have hprefix_pointwise : ∀ bpr_divisor_index_bpcpdcm_prefix_pointwise. ∀ bpr_divisor_value_bpcpdcm_prefix_pointwise. Lt(bpr_divisor_index_bpcpdcm_prefix_pointwise,l) → BetaAt(b,c,bpr_divisor_index_bpcpdcm_prefix_pointwise,bpr_divisor_value_bpcpdcm_prefix_pointwise) → Dvd(bpr_divisor_value_bpcpdcm_prefix_pointwise,z)Exact native replay line
have hprefix_pointwise : forall bpr_divisor_index_bpcpdcm_prefix_pointwise bpr_divisor_value_bpcpdcm_prefix_pointwise. (exists bpr_gap_bpcpdcm_prefix_pointwise_index_bound. bpr_gap_bpcpdcm_prefix_pointwise_index_bound + S (bpr_divisor_index_bpcpdcm_prefix_pointwise) = l) -> (((exists bpr_height_bpcpdcm_prefix_pointwise_decoded. bpr_height_bpcpdcm_prefix_pointwise_decoded + S (bpr_divisor_value_bpcpdcm_prefix_pointwise) = S ((S (bpr_divisor_index_bpcpdcm_prefix_pointwise)) * c)) /\ exists bpr_quotient_bpcpdcm_prefix_pointwise_decoded. b = bpr_quotient_bpcpdcm_prefix_pointwise_decoded * S ((S (bpr_divisor_index_bpcpdcm_prefix_pointwise)) * c) + (bpr_divisor_value_bpcpdcm_prefix_pointwise))) -> exists bpr_quotient_bpcpdcm_prefix_pointwise_result. z = bpr_divisor_value_bpcpdcm_prefix_pointwise * bpr_quotient_bpcpdcm_prefix_pointwise_result - 0061
intro i - 0062
intro p - 0063
intro hi - 0064
intro hp - 0065
specialize hpointwise i - 0066
specialize hpointwise p - 0067
apply hpointwise - 0068
specialize le_succ (S i) - 0069
specialize le_succ l - 0070
apply le_succ - 0071
exact hi - 0072
exact hp - 0073
have hprefix_divides : Dvd(x1,z)Exact native replay line
have hprefix_divides : exists q. z = x1 * q - 0074
specialize IH x1 - 0075
specialize IH z - 0076
apply IH - 0077
exact hprefix_pairwise - 0078
exact hprefix_pointwise - 0079
exact hdecomposition_witness_witness_right_left - 0080
have hlast_divides : Dvd(x,z)Exact native replay line
have hlast_divides : exists q. z = x * q - 0081
specialize hpointwise l - 0082
specialize hpointwise x - 0083
apply hpointwise - 0084
specialize le_refl (S l) - 0085
exact le_refl - 0086
exact hdecomposition_witness_witness_left - 0087
have hcoprime : Coprime(x1,x)Exact native replay line
have hcoprime : forall bpr_coprime_divisor_bpcpdcm_local_coprime. (exists bpr_coprime_left_factor_bpcpdcm_local_coprime. x1 = bpr_coprime_divisor_bpcpdcm_local_coprime * bpr_coprime_left_factor_bpcpdcm_local_coprime) -> (exists bpr_coprime_right_factor_bpcpdcm_local_coprime. x = bpr_coprime_divisor_bpcpdcm_local_coprime * bpr_coprime_right_factor_bpcpdcm_local_coprime) -> bpr_coprime_divisor_bpcpdcm_local_coprime = 1 - 0088
specialize beta_product_pointwise_coprime x - 0089
specialize beta_product_pointwise_coprime b - 0090
specialize beta_product_pointwise_coprime c - 0091
specialize beta_product_pointwise_coprime l - 0092
specialize beta_product_pointwise_coprime x1 - 0093
apply beta_product_pointwise_coprime - 0094
intro i - 0095
intro q - 0096
intro hi - 0097
intro hq - 0098
specialize hpairwise i - 0099
specialize hpairwise l - 0100
specialize hpairwise q - 0101
specialize hpairwise x - 0102
apply hpairwise - 0103
specialize le_succ (S i) - 0104
specialize le_succ l - 0105
apply le_succ - 0106
exact hi - 0107
specialize le_refl (S l) - 0108
exact le_refl - 0109
exact hq - 0110
exact hdecomposition_witness_witness_left - 0111
intro hil - 0112
rewrite hil at hi - 0113
specialize lt_irrefl_expanded l - 0114
apply lt_irrefl_expanded - 0115
exact hi - 0116
exact hdecomposition_witness_witness_right_left - 0117
have hlcm : Dvd(x1,x1 · x) ∧ Dvd(x,x1 · x) ∧ (∀ y. Dvd(x1,y) → Dvd(x,y) → Dvd(x1 · x,y))Exact native replay line
have hlcm : ((((exists u. x1 * x = x1 * u) /\ exists v. x1 * x = x * v) /\ forall t. (exists a. t = x1 * a) -> (exists d. t = x * d) -> exists q. t = (x1 * x) * q)) - 0118
specialize coprime_product_is_lcm x1 - 0119
specialize coprime_product_is_lcm x - 0120
apply coprime_product_is_lcm - 0121
exact hcoprime - 0122
cases hlcm - 0123
cases hlcm_left - 0124
have hresult : Dvd(x1 · x,z)Exact native replay line
have hresult : exists q. z = (x1 * x) * q - 0125
specialize hlcm_right z - 0126
apply hlcm_right - 0127
exact hprefix_divides - 0128
exact hlast_divides - 0129
rewrite hdecomposition_witness_witness_right_right - 0130
exact hresult