# Metamath Proof Explorer

## 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 {ℕ}_{0}\wedge {B}\in {ℕ}_{0}\right)\wedge \left({C}\in {ℕ}_{0}\wedge {D}\in {ℕ}_{0}\right)\right)\to \left({\left({A}+{B}\right)}^{2}+{B}={\left({C}+{D}\right)}^{2}+{D}↔\left({A}={C}\wedge {B}={D}\right)\right)$

### Proof

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