Description: Obsolete version of div0 as of 9-Jul-2025. (Contributed by NM, 14-Mar-2005) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | div0OLD | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ ) | |
| 2 | 1 | mul01d | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · 0 ) = 0 ) |
| 3 | 0cn | ⊢ 0 ∈ ℂ | |
| 4 | divmul | ⊢ ( ( 0 ∈ ℂ ∧ 0 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 0 / 𝐴 ) = 0 ↔ ( 𝐴 · 0 ) = 0 ) ) | |
| 5 | 3 3 4 | mp3an12 | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 0 / 𝐴 ) = 0 ↔ ( 𝐴 · 0 ) = 0 ) ) |
| 6 | 2 5 | mpbird | ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 ) |