Theorem 6p5lem

Description: Lemma for 6p5e11 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Hypotheses	6p5lem.1	|- A e. NN0
	6p5lem.2	|- D e. NN0
	6p5lem.3	|- E e. NN0
	6p5lem.4	|- B = ( D + 1 )
	6p5lem.5	|- C = ( E + 1 )
	6p5lem.6	|- ( A + D ) = ; 1 E
Assertion	6p5lem	|- ( A + B ) = ; 1 C

Proof

Step	Hyp	Ref	Expression
1		6p5lem.1	|- A e. NN0
2		6p5lem.2	|- D e. NN0
3		6p5lem.3	|- E e. NN0
4		6p5lem.4	|- B = ( D + 1 )
5		6p5lem.5	|- C = ( E + 1 )
6		6p5lem.6	|- ( A + D ) = ; 1 E
7	4	oveq2i	|- ( A + B ) = ( A + ( D + 1 ) )
8	1	nn0cni	|- A e. CC
9	2	nn0cni	|- D e. CC
10		ax-1cn	|- 1 e. CC
11	8 9 10	addassi	|- ( ( A + D ) + 1 ) = ( A + ( D + 1 ) )
12		1nn0	|- 1 e. NN0
13	5	eqcomi	|- ( E + 1 ) = C
14	12 3 13 6	decsuc	|- ( ( A + D ) + 1 ) = ; 1 C
15	7 11 14	3eqtr2i	|- ( A + B ) = ; 1 C