This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem div2sub

Description: Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion div2sub ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐷 − 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
2 subcl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 − 𝐷 ) ∈ ℂ )
3 2 3adant3 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) → ( 𝐶 − 𝐷 ) ∈ ℂ )
4 subeq0 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐶 − 𝐷 ) = 0 ↔ 𝐶 = 𝐷 ) )
5 4 necon3bid ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐶 − 𝐷 ) ≠ 0 ↔ 𝐶 ≠ 𝐷 ) )
6 5 biimp3ar ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) → ( 𝐶 − 𝐷 ) ≠ 0 )
7 3 6 jca ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) → ( ( 𝐶 − 𝐷 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ≠ 0 ) )
8 div2neg ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ≠ 0 ) → ( - ( 𝐴 − 𝐵 ) / - ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) )
9 8 3expb ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( ( 𝐶 − 𝐷 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ≠ 0 ) ) → ( - ( 𝐴 − 𝐵 ) / - ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) )
10 1 7 9 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) ) → ( - ( 𝐴 − 𝐵 ) / - ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) )
11 negsubdi2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) )
12 negsubdi2 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → - ( 𝐶 − 𝐷 ) = ( 𝐷 − 𝐶 ) )
13 12 3adant3 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) → - ( 𝐶 − 𝐷 ) = ( 𝐷 − 𝐶 ) )
14 11 13 oveqan12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) ) → ( - ( 𝐴 − 𝐵 ) / - ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐷 − 𝐶 ) ) )
15 10 14 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐷 − 𝐶 ) ) )