Theorem bj-lineqi

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-lineqi.a	|- ( ph -> A e. CC )
2		bj-lineqi.b	|- ( ph -> B e. CC )
3		bj-lineqi.x	|- ( ph -> X e. CC )
4		bj-lineqi.y	|- ( ph -> Y e. CC )
5		bj-lineqi.n0	|- ( ph -> A =/= 0 )
6		bj-lineqi.1	|- ( ph -> ( ( A x. X ) + B ) = Y )
7	1 2 3 4 5	lineq	|- ( ph -> ( ( ( A x. X ) + B ) = Y <-> X = ( ( Y - B ) / A ) ) )
8	6 7	mpbid	|- ( ph -> X = ( ( Y - B ) / A ) )