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	|- A e. CC
	problem3.2	|- ( A + 3 ) = 4
Assertion	problem3	|- A = 1

Proof

Step	Hyp	Ref	Expression
1		problem3.1	|- A e. CC
2		problem3.2	|- ( A + 3 ) = 4
3		4re	|- 4 e. RR
4	3	recni	|- 4 e. CC
5		3re	|- 3 e. RR
6	5	recni	|- 3 e. CC
7		1re	|- 1 e. RR
8	7	recni	|- 1 e. CC
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 + A ) = ( A + 3 )
14	13 2	eqtri	|- ( 3 + A ) = 4
15	4 6 1 14	subaddrii	|- ( 4 - 3 ) = A
16	12 15	eqtri	|- 1 = A
17	16	eqcomi	|- A = 1