Theorem bj-lineqi

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

	Ref	Expression
Hypotheses	bj-lineqi.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	bj-lineqi.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	bj-lineqi.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	bj-lineqi.y	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
	bj-lineqi.n0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	bj-lineqi.1	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + 𝐵 ) = 𝑌 )
Assertion	bj-lineqi	⊢ ( 𝜑 → 𝑋 = ( ( 𝑌 − 𝐵 ) / 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-lineqi.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		bj-lineqi.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		bj-lineqi.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4		bj-lineqi.y	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
5		bj-lineqi.n0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
6		bj-lineqi.1	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + 𝐵 ) = 𝑌 )
7	1 2 3 4 5	lineq	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) = 𝑌 ↔ 𝑋 = ( ( 𝑌 − 𝐵 ) / 𝐴 ) ) )
8	6 7	mpbid	⊢ ( 𝜑 → 𝑋 = ( ( 𝑌 − 𝐵 ) / 𝐴 ) )