Theorem 6p5lem

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

	Ref	Expression
Hypotheses	6p5lem.1	$$⊢A\in {\mathbb{N}}_0$$
	6p5lem.2	$$⊢D\in {\mathbb{N}}_0$$
	6p5lem.3	$$⊢E\in {\mathbb{N}}_0$$
	6p5lem.4	$$⊢B=D+1$$
	6p5lem.5	$$⊢C=E+1$$
	6p5lem.6	No typesetting found for |- ( A + D ) = ; 1 E with typecode |-
Assertion	6p5lem	Could not format assertion : No typesetting found for |- ( A + B ) = ; 1 C with typecode |-

Proof

Step	Hyp	Ref	Expression
1		6p5lem.1	$$⊢A\in {\mathbb{N}}_0$$
2		6p5lem.2	$$⊢D\in {\mathbb{N}}_0$$
3		6p5lem.3	$$⊢E\in {\mathbb{N}}_0$$
4		6p5lem.4	$$⊢B=D+1$$
5		6p5lem.5	$$⊢C=E+1$$
6		6p5lem.6	Could not format ( A + D ) = ; 1 E : No typesetting found for |- ( A + D ) = ; 1 E with typecode |-
7	4	oveq2i	$$⊢A+B=A+D+1$$
8	1	nn0cni	$$⊢A\in ℂ$$
9	2	nn0cni	$$⊢D\in ℂ$$
10		ax-1cn	$$⊢1\in ℂ$$
11	8 9 10	addassi	$$⊢A+D+1=A+D+1$$
12		1nn0	$$⊢1\in {\mathbb{N}}_0$$
13	5	eqcomi	$$⊢E+1=C$$
14	12 3 13 6	decsuc	Could not format ( ( A + D ) + 1 ) = ; 1 C : No typesetting found for |- ( ( A + D ) + 1 ) = ; 1 C with typecode |-
15	7 11 14	3eqtr2i	Could not format ( A + B ) = ; 1 C : No typesetting found for |- ( A + B ) = ; 1 C with typecode |-