This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1div0OLD

Description: Obsolete version of 1div0 as of 5-Jun-2025. (Contributed by Mario Carneiro, 1-Apr-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion 1div0OLD ( 1 / 0 ) = ∅

Proof

Step Hyp Ref Expression
1 df-div ⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
2 riotaex ⊢ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) ∈ V
3 1 2 dmmpo ⊢ dom / = ( ℂ × ( ℂ ∖ { 0 } ) )
4 eqid ⊢ 0 = 0
5 eldifsni ⊢ ( 0 ∈ ( ℂ ∖ { 0 } ) → 0 ≠ 0 )
6 5 adantl ⊢ ( ( 1 ∈ ℂ ∧ 0 ∈ ( ℂ ∖ { 0 } ) ) → 0 ≠ 0 )
7 6 necon2bi ⊢ ( 0 = 0 → ¬ ( 1 ∈ ℂ ∧ 0 ∈ ( ℂ ∖ { 0 } ) ) )
8 4 7 ax-mp ⊢ ¬ ( 1 ∈ ℂ ∧ 0 ∈ ( ℂ ∖ { 0 } ) )
9 ndmovg ⊢ ( ( dom / = ( ℂ × ( ℂ ∖ { 0 } ) ) ∧ ¬ ( 1 ∈ ℂ ∧ 0 ∈ ( ℂ ∖ { 0 } ) ) ) → ( 1 / 0 ) = ∅ )
10 3 8 9 mp2an ⊢ ( 1 / 0 ) = ∅