Description: A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | drngmuleq0.b | ||
drngmuleq0.o | |||
drngmuleq0.t | |||
drngmuleq0.r | |||
drngmuleq0.x | |||
drngmuleq0.y | |||
Assertion | drngmulne0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drngmuleq0.b | ||
2 | drngmuleq0.o | ||
3 | drngmuleq0.t | ||
4 | drngmuleq0.r | ||
5 | drngmuleq0.x | ||
6 | drngmuleq0.y | ||
7 | 1 2 3 4 5 6 | drngmul0or | |
8 | 7 | necon3abid | |
9 | neanior | ||
10 | 8 9 | bitr4di |