Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ omega.
Assume H1: prime_nat x0.
Assume H2: b3e62.. x0 1 4.
Apply H1 with ∃ x1 . and (x1 ∈ omega) (∃ x2 . and (x2 ∈ omega) (x0 = add_SNo (mul_SNo x1 x1) (mul_SNo x2 x2))).
Assume H3: and (x0 ∈ omega) (1 ∈ x0).
Apply H3 with (∀ x1 . x1 ∈ omega ⟶ divides_nat x1 x0 ⟶ or (x1 = 1) (x1 = x0)) ⟶ ∃ x1 . and (x1 ∈ omega) (∃ x2 . and (x2 ∈ omega) (x0 = add_SNo (mul_SNo x1 x1) (mul_SNo x2 x2))).
Assume H4: x0 ∈ omega.
Assume H5: 1 ∈ x0.
Assume H6: ∀ x1 . x1 ∈ omega ⟶ divides_nat x1 x0 ⟶ or (x1 = 1) (x1 = x0).
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Apply Subq_finite with setexp x0 3, {x1 ∈ setexp omega 3|add_SNo (mul_SNo (ap x1 0) (ap x1 0)) (mul_SNo 4 (mul_SNo (ap x1 1) (ap x1 2))) = x0}, ∃ x1 . and (x1 ∈ omega) (∃ x2 . and (x2 ∈ omega) (x0 = add_SNo (mul_SNo x1 x1) (mul_SNo x2 x2))) leaving 3 subgoals.
Let x1 of type ο be given.
Assume H16: ∀ x2 . and (x2 ∈ omega) (equip (setexp x0 3) x2) ⟶ x1.
Apply H16 with exp_nat x0 3.
Apply andI with exp_nat x0 3 ∈ omega, equip (setexp x0 3) (exp_nat x0 3) leaving 2 subgoals.
Apply nat_p_omega with exp_nat x0 3.
Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with x0, 3 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying nat_3.
Apply equip_sym with exp_nat x0 3, setexp x0 3.
Apply unknownprop_bd08de5a4f85615a4f39f41286eceda7f514fc0714cf10e88acda1a639744bfc with x0, 3 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying nat_3.
Let x1 of type ι be given.
Assume H16: x1 ∈ {x2 ∈ setexp omega 3|add_SNo (mul_SNo (ap x2 0) (ap x2 0)) (mul_SNo 4 (mul_SNo (ap x2 1) (ap x2 2))) = x0}.
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Claim L35: ...
...
Apply Pi_eta with 3, λ x2 . omega, x1, λ x2 x3 . x2 ∈ setexp x0 3 leaving 2 subgoals.
Apply L13 with x1.
The subproof is completed by applying H16.
Apply lam_Pi with 3, λ x2 . x0, λ x2 . ap x1 x2.
Let x2 of type ι be given.
Assume H36: x2 ∈ 3.
Apply cases_3 with x2, λ x3 . ap x1 x3 ∈ x0 leaving 4 subgoals.
The subproof is completed by applying H36.
Apply ordinal_In_Or_Subq with ap x1 0, x0, ap x1 0 ∈ x0 leaving 4 subgoals.
Apply nat_p_ordinal with ap x1 0.
Apply omega_nat_p with ap x1 0.
The subproof is completed by applying L17.
The subproof is completed by applying L9.
Assume H37: ap x1 0 ∈ x0.
The subproof is completed by applying H37.
Assume H37: x0 ⊆ ap x1 0.
Apply FalseE with ap x1 0 ∈ x0.
Apply SNoLt_irref with x0.
Apply SNoLeLt_tra with x0, mul_SNo (ap x1 0) ..., ... leaving 5 subgoals.
...
...
...
...
...
...
...
...
■