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 ) ) )