Theorem nn0opth2

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

	Ref	Expression
Assertion	nn0opth2	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \left(C\in {\mathbb{N}}_0\wedge D\in {\mathbb{N}}_0\right)\right)\to \left({\left(A+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow \left(A=C\wedge B=D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢A=if\left(A\in {\mathbb{N}}_0,A,0\right)\to A+B=if\left(A\in {\mathbb{N}}_0,A,0\right)+B$$
2	1	oveq1d	$$⊢A=if\left(A\in {\mathbb{N}}_0,A,0\right)\to {\left(A+B\right)}^2={\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+B\right)}^2$$
3	2	oveq1d	$$⊢A=if\left(A\in {\mathbb{N}}_0,A,0\right)\to {\left(A+B\right)}^2+B={\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+B\right)}^2+B$$
4	3	eqeq1d	$$⊢A=if\left(A\in {\mathbb{N}}_0,A,0\right)\to \left({\left(A+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow {\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+B\right)}^2+B={\left(C+D\right)}^2+D\right)$$
5		eqeq1	$$⊢A=if\left(A\in {\mathbb{N}}_0,A,0\right)\to \left(A=C\leftrightarrow if\left(A\in {\mathbb{N}}_0,A,0\right)=C\right)$$
6	5	anbi1d	$$⊢A=if\left(A\in {\mathbb{N}}_0,A,0\right)\to \left(\left(A=C\wedge B=D\right)\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\wedge B=D\right)\right)$$
7	4 6	bibi12d	$$⊢A=if\left(A\in {\mathbb{N}}_0,A,0\right)\to \left(\left({\left(A+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow \left(A=C\wedge B=D\right)\right)\leftrightarrow \left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\wedge B=D\right)\right)\right)$$
8		oveq2	$$⊢B=if\left(B\in {\mathbb{N}}_0,B,0\right)\to if\left(A\in {\mathbb{N}}_0,A,0\right)+B=if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)$$
9	8	oveq1d	$$⊢B=if\left(B\in {\mathbb{N}}_0,B,0\right)\to {\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+B\right)}^2={\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2$$
10		id	$$⊢B=if\left(B\in {\mathbb{N}}_0,B,0\right)\to B=if\left(B\in {\mathbb{N}}_0,B,0\right)$$
11	9 10	oveq12d	$$⊢B=if\left(B\in {\mathbb{N}}_0,B,0\right)\to {\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+B\right)}^2+B={\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)$$
12	11	eqeq1d	$$⊢B=if\left(B\in {\mathbb{N}}_0,B,0\right)\to \left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow {\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(C+D\right)}^2+D\right)$$
13		eqeq1	$$⊢B=if\left(B\in {\mathbb{N}}_0,B,0\right)\to \left(B=D\leftrightarrow if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)$$
14	13	anbi2d	$$⊢B=if\left(B\in {\mathbb{N}}_0,B,0\right)\to \left(\left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\wedge B=D\right)\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)\right)$$
15	12 14	bibi12d	$$⊢B=if\left(B\in {\mathbb{N}}_0,B,0\right)\to \left(\left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\wedge B=D\right)\right)\leftrightarrow \left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(C+D\right)}^2+D\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)\right)\right)$$
16		oveq1	$$⊢C=if\left(C\in {\mathbb{N}}_0,C,0\right)\to C+D=if\left(C\in {\mathbb{N}}_0,C,0\right)+D$$
17	16	oveq1d	$$⊢C=if\left(C\in {\mathbb{N}}_0,C,0\right)\to {\left(C+D\right)}^2={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+D\right)}^2$$
18	17	oveq1d	$$⊢C=if\left(C\in {\mathbb{N}}_0,C,0\right)\to {\left(C+D\right)}^2+D={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+D\right)}^2+D$$
19	18	eqeq2d	$$⊢C=if\left(C\in {\mathbb{N}}_0,C,0\right)\to \left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(C+D\right)}^2+D\leftrightarrow {\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+D\right)}^2+D\right)$$
20		eqeq2	$$⊢C=if\left(C\in {\mathbb{N}}_0,C,0\right)\to \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\leftrightarrow if\left(A\in {\mathbb{N}}_0,A,0\right)=if\left(C\in {\mathbb{N}}_0,C,0\right)\right)$$
21	20	anbi1d	$$⊢C=if\left(C\in {\mathbb{N}}_0,C,0\right)\to \left(\left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=if\left(C\in {\mathbb{N}}_0,C,0\right)\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)\right)$$
22	19 21	bibi12d	$$⊢C=if\left(C\in {\mathbb{N}}_0,C,0\right)\to \left(\left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(C+D\right)}^2+D\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=C\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)\right)\leftrightarrow \left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+D\right)}^2+D\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=if\left(C\in {\mathbb{N}}_0,C,0\right)\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)\right)\right)$$
23		oveq2	$$⊢D=if\left(D\in {\mathbb{N}}_0,D,0\right)\to if\left(C\in {\mathbb{N}}_0,C,0\right)+D=if\left(C\in {\mathbb{N}}_0,C,0\right)+if\left(D\in {\mathbb{N}}_0,D,0\right)$$
24	23	oveq1d	$$⊢D=if\left(D\in {\mathbb{N}}_0,D,0\right)\to {\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+D\right)}^2={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+if\left(D\in {\mathbb{N}}_0,D,0\right)\right)}^2$$
25		id	$$⊢D=if\left(D\in {\mathbb{N}}_0,D,0\right)\to D=if\left(D\in {\mathbb{N}}_0,D,0\right)$$
26	24 25	oveq12d	$$⊢D=if\left(D\in {\mathbb{N}}_0,D,0\right)\to {\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+D\right)}^2+D={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+if\left(D\in {\mathbb{N}}_0,D,0\right)\right)}^2+if\left(D\in {\mathbb{N}}_0,D,0\right)$$
27	26	eqeq2d	$$⊢D=if\left(D\in {\mathbb{N}}_0,D,0\right)\to \left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+D\right)}^2+D\leftrightarrow {\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+if\left(D\in {\mathbb{N}}_0,D,0\right)\right)}^2+if\left(D\in {\mathbb{N}}_0,D,0\right)\right)$$
28		eqeq2	$$⊢D=if\left(D\in {\mathbb{N}}_0,D,0\right)\to \left(if\left(B\in {\mathbb{N}}_0,B,0\right)=D\leftrightarrow if\left(B\in {\mathbb{N}}_0,B,0\right)=if\left(D\in {\mathbb{N}}_0,D,0\right)\right)$$
29	28	anbi2d	$$⊢D=if\left(D\in {\mathbb{N}}_0,D,0\right)\to \left(\left(if\left(A\in {\mathbb{N}}_0,A,0\right)=if\left(C\in {\mathbb{N}}_0,C,0\right)\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=if\left(C\in {\mathbb{N}}_0,C,0\right)\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=if\left(D\in {\mathbb{N}}_0,D,0\right)\right)\right)$$
30	27 29	bibi12d	$$⊢D=if\left(D\in {\mathbb{N}}_0,D,0\right)\to \left(\left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+D\right)}^2+D\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=if\left(C\in {\mathbb{N}}_0,C,0\right)\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=D\right)\right)\leftrightarrow \left({\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+if\left(D\in {\mathbb{N}}_0,D,0\right)\right)}^2+if\left(D\in {\mathbb{N}}_0,D,0\right)\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=if\left(C\in {\mathbb{N}}_0,C,0\right)\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=if\left(D\in {\mathbb{N}}_0,D,0\right)\right)\right)\right)$$
31		0nn0	$$⊢0\in {\mathbb{N}}_0$$
32	31	elimel	$$⊢if\left(A\in {\mathbb{N}}_0,A,0\right)\in {\mathbb{N}}_0$$
33	31	elimel	$$⊢if\left(B\in {\mathbb{N}}_0,B,0\right)\in {\mathbb{N}}_0$$
34	31	elimel	$$⊢if\left(C\in {\mathbb{N}}_0,C,0\right)\in {\mathbb{N}}_0$$
35	31	elimel	$$⊢if\left(D\in {\mathbb{N}}_0,D,0\right)\in {\mathbb{N}}_0$$
36	32 33 34 35	nn0opth2i	$$⊢{\left(if\left(A\in {\mathbb{N}}_0,A,0\right)+if\left(B\in {\mathbb{N}}_0,B,0\right)\right)}^2+if\left(B\in {\mathbb{N}}_0,B,0\right)={\left(if\left(C\in {\mathbb{N}}_0,C,0\right)+if\left(D\in {\mathbb{N}}_0,D,0\right)\right)}^2+if\left(D\in {\mathbb{N}}_0,D,0\right)\leftrightarrow \left(if\left(A\in {\mathbb{N}}_0,A,0\right)=if\left(C\in {\mathbb{N}}_0,C,0\right)\wedge if\left(B\in {\mathbb{N}}_0,B,0\right)=if\left(D\in {\mathbb{N}}_0,D,0\right)\right)$$
37	7 15 22 30 36	dedth4h	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\wedge \left(C\in {\mathbb{N}}_0\wedge D\in {\mathbb{N}}_0\right)\right)\to \left({\left(A+B\right)}^2+B={\left(C+D\right)}^2+D\leftrightarrow \left(A=C\wedge B=D\right)\right)$$