Theorem edomidom

Description: Every Euclidean domain is an integral domain. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Hypothesis	edomidom.1	⊢ ( 𝜑 → 𝐷 ∈ EDomn )
Assertion	edomidom	⊢ ( 𝜑 → 𝐷 ∈ IDomn )

Proof

Step	Hyp	Ref	Expression
1		edomidom.1	⊢ ( 𝜑 → 𝐷 ∈ EDomn )
2		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
3		eqid	⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
4		eqid	⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
5		eqid	⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
6		eqid	⊢ ( ( EuclF ‘ 𝐷 ) ↾ ( ( Base ‘ 𝐷 ) ∖ { ( 0g ‘ 𝐷 ) } ) ) = ( ( EuclF ‘ 𝐷 ) ↾ ( ( Base ‘ 𝐷 ) ∖ { ( 0g ‘ 𝐷 ) } ) )
7	2 3 4 5 6	isedom	⊢ ( 𝐷 ∈ EDomn ↔ ( 𝐷 ∈ IDomn ∧ ( ( ( EuclF ‘ 𝐷 ) ↾ ( ( Base ‘ 𝐷 ) ∖ { ( 0g ‘ 𝐷 ) } ) ) : ( ( Base ‘ 𝐷 ) ∖ { ( 0g ‘ 𝐷 ) } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑦 ∈ ( ( Base ‘ 𝐷 ) ∖ { ( 0g ‘ 𝐷 ) } ) ∃ 𝑞 ∈ ( Base ‘ 𝐷 ) ∃ 𝑟 ∈ ( Base ‘ 𝐷 ) ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐷 ) 𝑞 ) ( +g ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑟 = ( 0g ‘ 𝐷 ) ∨ ( ( ( EuclF ‘ 𝐷 ) ↾ ( ( Base ‘ 𝐷 ) ∖ { ( 0g ‘ 𝐷 ) } ) ) ‘ 𝑟 ) < ( ( ( EuclF ‘ 𝐷 ) ↾ ( ( Base ‘ 𝐷 ) ∖ { ( 0g ‘ 𝐷 ) } ) ) ‘ 𝑦 ) ) ) ) ) )
8	7	simplbi	⊢ ( 𝐷 ∈ EDomn → 𝐷 ∈ IDomn )
9	1 8	syl	⊢ ( 𝜑 → 𝐷 ∈ IDomn )