Metamath Proof Explorer
Description: Quotient of two negatives. (Contributed by Mario Carneiro, 27May2016)


Ref 
Expression 

Hypotheses 
div1d.1 
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) 


divcld.2 
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) 


divcld.3 
⊢ ( 𝜑 → 𝐵 ≠ 0 ) 

Assertion 
div2negd 
⊢ ( 𝜑 → (  𝐴 /  𝐵 ) = ( 𝐴 / 𝐵 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

div1d.1 
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) 
2 

divcld.2 
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) 
3 

divcld.3 
⊢ ( 𝜑 → 𝐵 ≠ 0 ) 
4 

div2neg 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → (  𝐴 /  𝐵 ) = ( 𝐴 / 𝐵 ) ) 
5 
1 2 3 4

syl3anc 
⊢ ( 𝜑 → (  𝐴 /  𝐵 ) = ( 𝐴 / 𝐵 ) ) 