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

Metamath Proof Explorer

Theorem lineq

Description: Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019)

Ref Expression
Hypotheses lineq.a 
|- ( ph -> A e. CC )
lineq.b 
|- ( ph -> B e. CC )
lineq.x 
|- ( ph -> X e. CC )
lineq.y 
|- ( ph -> Y e. CC )
lineq.n0 
|- ( ph -> A =/= 0 )
Assertion lineq 
|- ( ph -> ( ( ( A x. X ) + B ) = Y <-> X = ( ( Y - B ) / A ) ) )

Proof

Step Hyp Ref Expression
1 lineq.a 
 |-  ( ph -> A e. CC )
2 lineq.b 
 |-  ( ph -> B e. CC )
3 lineq.x 
 |-  ( ph -> X e. CC )
4 lineq.y 
 |-  ( ph -> Y e. CC )
5 lineq.n0 
 |-  ( ph -> A =/= 0 )
6 1 3 mulcld 
 |-  ( ph -> ( A x. X ) e. CC )
7 6 2 4 addlsub 
 |-  ( ph -> ( ( ( A x. X ) + B ) = Y <-> ( A x. X ) = ( Y - B ) ) )
8 4 2 subcld 
 |-  ( ph -> ( Y - B ) e. CC )
9 1 3 8 5 rdiv 
 |-  ( ph -> ( ( A x. X ) = ( Y - B ) <-> X = ( ( Y - B ) / A ) ) )
10 7 9 bitrd 
 |-  ( ph -> ( ( ( A x. X ) + B ) = Y <-> X = ( ( Y - B ) / A ) ) )