Proofgold Address

Param nat_p^nat_p : ι → ο
Param SNo^SNo : ι → ο
Param ordinal^ordinal : ι → ο
Known ordinal_SNo^ordinal_SNo : ∀ x0 . ordinal x0 ⟶ SNo x0
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem nat_p_SNo^nat_p_SNo : ∀ x0 . nat_p x0 ⟶ SNo x0 (proof)
Param omega^omega : ι
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Theorem omega_SNo^omega_SNo : ∀ x0 . x0 ∈ omega ⟶ SNo x0 (proof)
Param binunion^binunion : ι → ι → ι
Param minus_CSNo^minus_CSNo : ι → ι
Definition int_alt1^int := binunion omega (prim5 omega minus_CSNo)
Param minus_SNo^minus_SNo : ι → ι
Known a3283..^{int_SNo_cases} : ∀ x0 : ι → ο . (∀ x1 . x1 ∈ omega ⟶ x0 x1) ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 (minus_SNo x1)) ⟶ ∀ x1 . x1 ∈ int_alt1 ⟶ x0 x1
Known SNo_minus_SNo^{SNo_minus_SNo} : ∀ x0 . SNo x0 ⟶ SNo (minus_SNo x0)
Theorem 0c7a0.. : ∀ x0 . x0 ∈ int_alt1 ⟶ SNo x0 (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Param ordsucc^ordsucc : ι → ι
Known nat_inv^nat_inv : ∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known minus_SNo_0^minus_SNo_0 : minus_SNo 0 = 0
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Param SNoLt^SNoLt : ι → ι → ο
Known SNoLt_irref^SNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Param SNoLe^SNoLe : ι → ι → ο
Known SNoLeLt_tra^SNoLeLt_tra : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x1 ⟶ SNoLt x1 x2 ⟶ SNoLt x0 x2
Known SNo_0^SNo_0 : SNo 0
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordinal_Subq_SNoLe^{ordinal_Subq_SNoLe} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ x0 ⊆ x1 ⟶ SNoLe x0 x1
Known ordinal_Empty^{ordinal_Empty} : ordinal 0
Known Subq_Empty^Subq_Empty : ∀ x0 . 0 ⊆ x0
Known minus_SNo_Lt_contra1^{minus_SNo_Lt_contra1} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLt (minus_SNo x0) x1 ⟶ SNoLt (minus_SNo x1) x0
Known ordinal_In_SNoLt^{ordinal_In_SNoLt} : ∀ x0 . ordinal x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ SNoLt x1 x0
Known nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Theorem nonpos_nonneg_0^{nonpos_nonneg_0} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ x0 = minus_SNo x1 ⟶ and (x0 = 0) (x1 = 0) (proof)
Param mul_SNo^mul_SNo : ι → ι → ι
Known mul_SNo_com^mul_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 x1 = mul_SNo x1 x0
Known mul_SNo_minus_distrL^{mul_SNo_minus_distrL} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1)
Theorem mul_SNo_minus_distrR^{mul_minus_SNo_distrR} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1) (proof)
Param add_SNo^add_SNo : ι → ι → ι
Known minus_SNo_invol^{minus_SNo_invol} : ∀ x0 . SNo x0 ⟶ minus_SNo (minus_SNo x0) = x0
Known add_SNo_minus_R2^{add_SNo_minus_R2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (add_SNo x0 x1) (minus_SNo x1) = x0
Theorem add_SNo_minus_R2'^{add_SNo_minus_R2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (add_SNo x0 (minus_SNo x1)) x1 = x0 (proof)
Known add_SNo_com^add_SNo_com : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 x1 = add_SNo x1 x0
Known SNo_add_SNo^SNo_add_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (add_SNo x0 x1)
Theorem add_SNo_minus_L2^{add_SNo_minus_L2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1 (proof)
Theorem add_SNo_minus_SNo_prop2^{add_SNo_minus_SNo_prop2} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ add_SNo x0 (add_SNo (minus_SNo x0) x1) = x1 (proof)
Param setminus^setminus : ι → ι → ι
Definition 98d78.. := λ x0 x1 x2 . and (and (and (x0 ∈ omega) (x1 ∈ omega)) (x2 ∈ setminus omega 1)) (or (∀ x3 : ο . (∀ x4 . and (x4 ∈ omega) (add_SNo x0 (mul_SNo x4 x2) = x1) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (x4 ∈ omega) (add_SNo x1 (mul_SNo x4 x2) = x0) ⟶ x3) ⟶ x3))
Definition divides_int_alt1^divides_int := λ x0 x1 . and (and (x0 ∈ int_alt1) (x1 ∈ int_alt1)) (∀ x2 : ο . (∀ x3 . and (x3 ∈ int_alt1) (mul_SNo x0 x3 = x1) ⟶ x2) ⟶ x2)
Definition 6ccc6.. := λ x0 x1 x2 . and (and (and (x0 ∈ int_alt1) (x1 ∈ int_alt1)) (x2 ∈ setminus omega 1)) (divides_int_alt1 x2 (add_SNo x0 (minus_SNo x1)))
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Theorem 7224d.. : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . x1 ∈ setminus omega 1 ⟶ x0 x1) ⟶ (∀ x1 . x1 ∈ setminus omega 1 ⟶ x0 (minus_SNo x1)) ⟶ ∀ x1 . x1 ∈ int_alt1 ⟶ x0 x1 (proof)
Theorem c2ee5.. : ∀ x0 . x0 ∈ int_alt1 ⟶ ∀ x1 : ο . (x0 = 0 ⟶ x1) ⟶ (x0 ∈ setminus omega 1 ⟶ x1) ⟶ (∀ x2 . x2 ∈ setminus omega 1 ⟶ x0 = minus_SNo x2 ⟶ x1) ⟶ x1 (proof)
Param mul_nat^mul_nat : ι → ι → ι
Definition divides_nat^divides_nat := λ x0 x1 . and (and (x0 ∈ omega) (x1 ∈ omega)) (∀ x2 : ο . (∀ x3 . and (x3 ∈ omega) (mul_nat x0 x3 = x1) ⟶ x2) ⟶ x2)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known c3d99..^{Subq_omega_int} : omega ⊆ int_alt1
Known mul_nat_mul_SNo^{mul_nat_mul_SNo} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_nat x0 x1 = mul_SNo x0 x1
Theorem 2f07e.. : ∀ x0 x1 . divides_nat x0 x1 ⟶ divides_int_alt1 x0 x1 (proof)
Known binunionE^binunionE : ∀ x0 x1 x2 . x2 ∈ binunion x0 x1 ⟶ or (x2 ∈ x0) (x2 ∈ x1)
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_0^nat_0 : nat_p 0
Known mul_nat_0R^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known ReplE_impred^ReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ prim5 x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known minus_SNo_minus_CSNo^{minus_SNo_minus_CSNo} : ∀ x0 . SNo x0 ⟶ minus_SNo x0 = minus_CSNo x0
Known mul_SNo_In_omega^{mul_SNo_In_omega} : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ mul_SNo x0 x1 ∈ omega
Theorem e7fac.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ divides_int_alt1 x0 x1 ⟶ divides_nat x0 x1 (proof)
Definition coprime_nat^coprime_nat := λ x0 x1 . and (and (x0 ∈ omega) (x1 ∈ omega)) (∀ x2 . x2 ∈ setminus omega 1 ⟶ divides_nat x2 x0 ⟶ divides_nat x2 x1 ⟶ x2 = 1)
Definition 76fc5..^coprime_int := λ x0 x1 . and (and (x0 ∈ int_alt1) (x1 ∈ int_alt1)) (∀ x2 . x2 ∈ setminus omega 1 ⟶ divides_int_alt1 x2 x0 ⟶ divides_int_alt1 x2 x1 ⟶ x2 = 1)
Known setminusE1^setminusE1 : ∀ x0 x1 x2 . x2 ∈ setminus x0 x1 ⟶ x2 ∈ x0
Theorem 9ab3b.. : ∀ x0 x1 . coprime_nat x0 x1 ⟶ 76fc5.. x0 x1 (proof)
Theorem 92a45.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ 76fc5.. x0 x1 ⟶ coprime_nat x0 x1 (proof)
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Known a0aa5..^int_add_SNo : ∀ x0 . x0 ∈ int_alt1 ⟶ ∀ x1 . x1 ∈ int_alt1 ⟶ add_SNo x0 x1 ∈ int_alt1
Known daaad..^{int_minus_SNo} : ∀ x0 . x0 ∈ int_alt1 ⟶ minus_SNo x0 ∈ int_alt1
Known 1b4d5..^{int_minus_SNo_omega} : ∀ x0 . x0 ∈ omega ⟶ minus_SNo x0 ∈ int_alt1
Known add_SNo_cancel_R^{add_SNo_cancel_R} : ∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ add_SNo x0 x1 = add_SNo x2 x1 ⟶ x0 = x2
Known SNo_mul_SNo^SNo_mul_SNo : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNo (mul_SNo x0 x1)
Theorem 0d560.. : ∀ x0 x1 x2 . 98d78.. x0 x1 x2 ⟶ 6ccc6.. x0 x1 x2 (proof)
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known minus_add_SNo_distr^{minus_add_SNo_distr} : ∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo x1)
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem d2c77.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ ∀ x2 . 6ccc6.. x0 x1 x2 ⟶ 98d78.. x0 x1 x2 (proof)