Metamath Proof Explorer

Theorem edomediv

Description: Apply a Euclidean division in a Euclidean domain. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses edomediv.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
edomediv.z ⊢ 0 = ( 0g ‘ 𝐷 )
edomediv.p ⊢ + = ( +g ‘ 𝐷 )
edomediv.m ⊢ · = ( .r ‘ 𝐷 )
edomediv.e ⊢ 𝐸 = ( EuclF ‘ 𝐷 )
edomediv.d ⊢ ( 𝜑 → 𝐷 ∈ EDomn )
edomediv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
edomediv.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ∖ { 0 } ) )
Assertion edomediv ( 𝜑 → ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 edomediv.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 edomediv.z ⊢ 0 = ( 0g ‘ 𝐷 )
3 edomediv.p ⊢ + = ( +g ‘ 𝐷 )
4 edomediv.m ⊢ · = ( .r ‘ 𝐷 )
5 edomediv.e ⊢ 𝐸 = ( EuclF ‘ 𝐷 )
6 edomediv.d ⊢ ( 𝜑 → 𝐷 ∈ EDomn )
7 edomediv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 edomediv.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ∖ { 0 } ) )
9 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ↔ 𝑋 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ) )
10 9 anbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ↔ ( 𝑋 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) )
11 10 2rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ↔ ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑋 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) )
12 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 · 𝑞 ) = ( 𝑌 · 𝑞 ) )
13 12 oveq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 · 𝑞 ) + 𝑟 ) = ( ( 𝑌 · 𝑞 ) + 𝑟 ) )
14 13 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑋 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ↔ 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ) )
15 fveq2 ⊢ ( 𝑦 = 𝑌 → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) = ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) )
16 15 breq2d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ↔ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) )
17 16 orbi2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ↔ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ) )
18 14 17 anbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ↔ ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ) ) )
19 18 2rexbidv ⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑋 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ↔ ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ) ) )
20 5 reseq1i ⊢ ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) = ( ( EuclF ‘ 𝐷 ) ↾ ( 𝐵 ∖ { 0 } ) )
21 1 2 3 4 20 isedom ⊢ ( 𝐷 ∈ EDomn ↔ ( 𝐷 ∈ IDomn ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) ) )
22 6 21 sylib ⊢ ( 𝜑 → ( 𝐷 ∈ IDomn ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) ) )
23 22 simprrd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
24 11 19 23 7 8 rspc2dv ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ) )
25 biort ⊢ ( 𝑟 = 0 → ( 𝑟 = 0 ↔ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ) )
26 biort ⊢ ( 𝑟 = 0 → ( 𝑟 = 0 ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) )
27 25 26 bitr3d ⊢ ( 𝑟 = 0 → ( ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) )
28 27 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 = 0 ) → ( ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) )
29 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ 𝐵 )
30 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → 𝑟 ≠ 0 )
31 29 30 eldifsnd ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → 𝑟 ∈ ( 𝐵 ∖ { 0 } ) )
32 31 fvresd ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) = ( 𝐸 ‘ 𝑟 ) )
33 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → 𝑌 ∈ ( 𝐵 ∖ { 0 } ) )
34 33 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) = ( 𝐸 ‘ 𝑌 ) )
35 34 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) = ( 𝐸 ‘ 𝑌 ) )
36 32 35 breq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ↔ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) )
37 36 orbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑟 ≠ 0 ) → ( ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) )
38 28 37 pm2.61dane ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ↔ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) )
39 38 anbi2d ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ) ↔ ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) ) )
40 39 anasss ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ) ↔ ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) ) )
41 40 2rexbidva ⊢ ( 𝜑 → ( ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑌 ) ) ) ↔ ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) ) )
42 24 41 mpbid ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑋 = ( ( 𝑌 · 𝑞 ) + 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( 𝐸 ‘ 𝑟 ) < ( 𝐸 ‘ 𝑌 ) ) ) )