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 | |- ( ( A e. CC /\ A =/= 0 ) -> ( 0 / A ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl | |- ( ( A e. CC /\ A =/= 0 ) -> A e. CC ) |
|
| 2 | 1 | mul01d | |- ( ( A e. CC /\ A =/= 0 ) -> ( A x. 0 ) = 0 ) |
| 3 | 0cn | |- 0 e. CC |
|
| 4 | divmul | |- ( ( 0 e. CC /\ 0 e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( 0 / A ) = 0 <-> ( A x. 0 ) = 0 ) ) |
|
| 5 | 3 3 4 | mp3an12 | |- ( ( A e. CC /\ A =/= 0 ) -> ( ( 0 / A ) = 0 <-> ( A x. 0 ) = 0 ) ) |
| 6 | 2 5 | mpbird | |- ( ( A e. CC /\ A =/= 0 ) -> ( 0 / A ) = 0 ) |