Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Apply nat_ind with λ x1 . equip (mul_nat x0 x1) (setprod x0 x1) leaving 2 subgoals.
Apply mul_nat_0R with x0, λ x1 x2 . equip x2 (setprod x0 0).
Claim L1: setprod x0 0 = 0
Apply Empty_eq with setprod x0 0.
Let x1 of type ι be given.
Assume H1: x1 ∈ setprod x0 0.
Apply EmptyE with ap x1 1.
Apply ap1_Sigma with x0, λ x2 . 0, x1.
The subproof is completed by applying H1.
Apply L1 with λ x1 x2 . equip 0 x2.
The subproof is completed by applying equip_ref with 0.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Assume H2: equip (mul_nat x0 x1) (setprod x0 x1).
Apply mul_nat_SR with x0, x1, λ x2 x3 . equip x3 (setprod x0 (ordsucc x1)) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply equip_tra with add_nat x0 (mul_nat x0 x1), setsum x0 (mul_nat x0 x1), setprod x0 (ordsucc x1) leaving 2 subgoals.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with x0, mul_nat x0 x1, x0, mul_nat x0 x1 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply mul_nat_p with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying equip_ref with x0.
The subproof is completed by applying equip_ref with mul_nat x0 x1.
Apply H2 with equip (setsum x0 (mul_nat x0 x1)) (setprod x0 (ordsucc x1)).
Let x2 of type ι → ι be given.
Assume H3: bij (mul_nat x0 x1) (setprod x0 x1) x2.
Apply H3 with equip (setsum x0 (mul_nat x0 x1)) (setprod x0 (ordsucc x1)).
Assume H4: and (∀ x3 . x3 ∈ mul_nat x0 x1 ⟶ x2 x3 ∈ setprod x0 x1) (∀ x3 . x3 ∈ mul_nat x0 x1 ⟶ ∀ x4 . x4 ∈ mul_nat x0 x1 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4).
Apply H4 with (∀ x3 . x3 ∈ setprod x0 x1 ⟶ ∃ x4 . and (x4 ∈ mul_nat x0 x1) (x2 x4 = x3)) ⟶ equip (setsum x0 (mul_nat x0 x1)) (setprod x0 (ordsucc x1)).
Assume H5: ∀ x3 . x3 ∈ mul_nat x0 x1 ⟶ x2 x3 ∈ setprod x0 x1.
Assume H6: ∀ x3 . x3 ∈ mul_nat x0 x1 ⟶ ∀ x4 . x4 ∈ mul_nat x0 x1 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Assume H7: ∀ x3 . x3 ∈ setprod x0 x1 ⟶ ∃ x4 . and (x4 ∈ mul_nat x0 x1) (x2 x4 = x3).
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Let x3 of type ο be given.
Assume H11: ∀ x4 : ι → ι . bij (setsum x0 (mul_nat x0 x1)) (setprod x0 (ordsucc x1)) x4 ⟶ x3.
Apply H11 with combine_funcs x0 (mul_nat x0 x1) (λ x4 . lam 2 (λ x5 . If_i (x5 = 0) x4 x1)) x2.
...
■