Description: The product of two nonzero numbers is nonzero. (Contributed by NM, 15-Feb-1995)
Ref | Expression | ||
---|---|---|---|
Hypotheses | muln0.1 | |- A e. CC |
|
muln0.2 | |- B e. CC |
||
muln0.3 | |- A =/= 0 |
||
muln0.4 | |- B =/= 0 |
||
Assertion | mulne0i | |- ( A x. B ) =/= 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muln0.1 | |- A e. CC |
|
2 | muln0.2 | |- B e. CC |
|
3 | muln0.3 | |- A =/= 0 |
|
4 | muln0.4 | |- B =/= 0 |
|
5 | mulne0 | |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A x. B ) =/= 0 ) |
|
6 | 1 3 2 4 5 | mp4an | |- ( A x. B ) =/= 0 |