Theorem problem3

Description: Practice problem 3. Clues: eqcomi eqtri subaddrii recni 4re 3re 1re df-4 addcomi . (Contributed by Filip Cernatescu, 16-Mar-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	problem3.1	⊢ 𝐴 ∈ ℂ
	problem3.2	⊢ ( 𝐴 + 3 ) = 4
Assertion	problem3	⊢ 𝐴 = 1

Proof

Step	Hyp	Ref	Expression
1		problem3.1	⊢ 𝐴 ∈ ℂ
2		problem3.2	⊢ ( 𝐴 + 3 ) = 4
3		4re	⊢ 4 ∈ ℝ
4	3	recni	⊢ 4 ∈ ℂ
5		3re	⊢ 3 ∈ ℝ
6	5	recni	⊢ 3 ∈ ℂ
7		1re	⊢ 1 ∈ ℝ
8	7	recni	⊢ 1 ∈ ℂ
9		df-4	⊢ 4 = ( 3 + 1 )
10	9	eqcomi	⊢ ( 3 + 1 ) = 4
11	4 6 8 10	subaddrii	⊢ ( 4 − 3 ) = 1
12	11	eqcomi	⊢ 1 = ( 4 − 3 )
13	6 1	addcomi	⊢ ( 3 + 𝐴 ) = ( 𝐴 + 3 )
14	13 2	eqtri	⊢ ( 3 + 𝐴 ) = 4
15	4 6 1 14	subaddrii	⊢ ( 4 − 3 ) = 𝐴
16	12 15	eqtri	⊢ 1 = 𝐴
17	16	eqcomi	⊢ 𝐴 = 1