Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_e218ed8cf74f73d11b13279ecb43db2e902573ebd411cc1f7c1f71620f4a5da3 with omega, rational leaving 2 subgoals.
Apply Subq_atleastp with omega, rational.
Apply Subq_tra with omega, int, rational leaving 2 subgoals.
The subproof is completed by applying Subq_omega_int.
Apply Subq_tra with int, SNoS_ omega, rational leaving 2 subgoals.
The subproof is completed by applying Subq_int_SNoS_omega.
The subproof is completed by applying Subq_SNoS_omega_rational.
Claim L0: ...
...
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Let x0 of type ο be given.
Assume H8: ∀ x1 : ι → ι . inj rational omega x1 ⟶ x0.
Apply H8 with λ x1 . If_i (SNoLe 0 x1) (nat_pair 0 (nat_pair ((λ x2 . prim0 (λ x3 . and (x3 ∈ omega) (x2 = div_SNo x3 ((λ x4 . prim0 (λ x5 . and (x5 ∈ omega) (∃ x6 . and (x6 ∈ omega) (x4 = div_SNo x6 x5)))) x2)))) x1) ((λ x2 . prim0 (λ x3 . and (x3 ∈ omega) (∃ x4 . and (x4 ∈ omega) (x2 = div_SNo x4 x3)))) x1))) (nat_pair 1 (nat_pair ((λ x2 . prim0 (λ x3 . and (x3 ∈ omega) (x2 = div_SNo x3 ((λ x4 . prim0 (λ x5 . and (x5 ∈ omega) (∃ x6 . and (x6 ∈ omega) (x4 = div_SNo x6 x5)))) x2)))) (minus_SNo x1)) ((λ x2 . prim0 (λ x3 . and (x3 ∈ omega) (∃ x4 . and (x4 ∈ omega) (x2 = div_SNo x4 x3)))) (minus_SNo x1)))).
Apply andI with ∀ x1 . x1 ∈ rational ⟶ (λ x2 . If_i (SNoLe 0 x2) (nat_pair 0 (nat_pair ((λ x3 . prim0 (λ x4 . and (x4 ∈ omega) (x3 = div_SNo x4 ((λ x5 . prim0 (λ x6 . and (x6 ∈ omega) (∃ x7 . and (x7 ∈ omega) (x5 = div_SNo x7 x6)))) x3)))) x2) ((λ x3 . prim0 (λ x4 . and (x4 ∈ omega) (∃ x5 . and (x5 ∈ omega) (x3 = div_SNo x5 x4)))) x2))) (nat_pair 1 (nat_pair ((λ x3 . prim0 (λ x4 . and (x4 ∈ omega) (x3 = div_SNo x4 ((λ x5 . prim0 (λ x6 . and (x6 ∈ omega) (∃ x7 . and (x7 ∈ omega) (x5 = div_SNo x7 x6)))) x3)))) (minus_SNo x2)) ((λ x3 . prim0 (λ x4 . and (x4 ∈ omega) (∃ x5 . and (x5 ∈ omega) (x3 = div_SNo x5 x4)))) (minus_SNo x2))))) x1 ∈ omega, ∀ x1 . ... ⟶ ∀ x2 . ... ⟶ (λ x3 . If_i (SNoLe 0 x3) (nat_pair 0 (nat_pair ((λ x4 . prim0 (λ x5 . and (x5 ∈ omega) (x4 = div_SNo x5 ((λ x6 . prim0 (λ x7 . and (x7 ∈ omega) ...)) ...)))) ...) ...)) ...) ... = ... ⟶ x1 = x2 leaving 2 subgoals.
...
...
■