Proofgold Address

Definition d3f3c.. := Power 0
Definition 33cc2.. := Power d3f3c..
Definition 99f52.. := Power 33cc2..
Definition 6a551.. := Power 99f52..
Known 97a83..^{atleastp_E_impred} : ∀ x0 x1 . atleastp x0 x1 ⟶ ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3 ⟶ x2) ⟶ x2
Known e6daf..^injE_impred : ∀ x0 x1 . ∀ x2 : ι → ι . inj x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . In x4 x0 ⟶ In (x2 x4) x1) ⟶ (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ x3) ⟶ x3
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Known 9ea3e..^Inj1_setsum : ∀ x0 x1 x2 . In x2 x1 ⟶ In (Inj1 x2) (setsum x0 x1)
Known f2c89..^{Empty_In_Power} : ∀ x0 . In 0 (Power x0)
Theorem 53760.. : ∀ x0 x1 x2 . atleastp (setsum 0 6a551..) 0 ⟶ False (proof)