Theorem nn0opth2i

Description: An ordered pair theorem for nonnegative integers. Theorem 17.3 of Quine p. 124. See comments for nn0opthi . (Contributed by NM, 22-Jul-2004)

	Ref	Expression
Hypotheses	nn0opth.1	$$⊢A\in {\mathbb{N}}_0$$
	nn0opth.2	$$⊢B\in {\mathbb{N}}_0$$
	nn0opth.3	$$⊢C\in {\mathbb{N}}_0$$
	nn0opth.4	$$⊢D\in {\mathbb{N}}_0$$
Assertion	nn0opth2i	$$⊢{\left(A+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0opth.1	$$⊢A\in {\mathbb{N}}_0$$
2		nn0opth.2	$$⊢B\in {\mathbb{N}}_0$$
3		nn0opth.3	$$⊢C\in {\mathbb{N}}_0$$
4		nn0opth.4	$$⊢D\in {\mathbb{N}}_0$$
5	1	nn0cni	$$⊢A\in ℂ$$
6	2	nn0cni	$$⊢B\in ℂ$$
7	5 6	addcli	$$⊢A+B\in ℂ$$
8	7	sqvali	$$⊢{\left(A+B\right)}^2=\left(A+B\right)\left(A+B\right)$$
9	8	oveq1i	$$⊢{\left(A+B\right)}^2+B=\left(A+B\right)\left(A+B\right)+B$$
10	3	nn0cni	$$⊢C\in ℂ$$
11	4	nn0cni	$$⊢D\in ℂ$$
12	10 11	addcli	$$⊢C+D\in ℂ$$
13	12	sqvali	$$⊢{\left(C+D\right)}^2=\left(C+D\right)\left(C+D\right)$$
14	13	oveq1i	$$⊢{\left(C+D\right)}^2+D=\left(C+D\right)\left(C+D\right)+D$$
15	9 14	eqeq12i	$$⊢{\left(A+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow \left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D$$
16	1 2 3 4	nn0opthi	$$⊢\left(A+B\right)\left(A+B\right)+B=\left(C+D\right)\left(C+D\right)+D\leftrightarrow \left(A=C\wedge B=D\right)$$
17	15 16	bitri	$$⊢{\left(A+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow \left(A=C\wedge B=D\right)$$