Description: A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | drngmuleq0.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
drngmuleq0.o | ⊢ 0 = ( 0g ‘ 𝑅 ) | ||
drngmuleq0.t | ⊢ · = ( .r ‘ 𝑅 ) | ||
drngmuleq0.r | ⊢ ( 𝜑 → 𝑅 ∈ DivRing ) | ||
drngmuleq0.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) | ||
drngmuleq0.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) | ||
Assertion | drngmulne0 | ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drngmuleq0.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
2 | drngmuleq0.o | ⊢ 0 = ( 0g ‘ 𝑅 ) | |
3 | drngmuleq0.t | ⊢ · = ( .r ‘ 𝑅 ) | |
4 | drngmuleq0.r | ⊢ ( 𝜑 → 𝑅 ∈ DivRing ) | |
5 | drngmuleq0.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) | |
6 | drngmuleq0.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) | |
7 | 1 2 3 4 5 6 | drngmul0or | ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) ) |
8 | 7 | necon3abid | ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) ) |
9 | neanior | ⊢ ( ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) | |
10 | 8 9 | bitr4di | ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) ) |