# Metamath Proof Explorer

## 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 𝐴 ∈ ℕ0
nn0opth.2 𝐵 ∈ ℕ0
nn0opth.3 𝐶 ∈ ℕ0
nn0opth.4 𝐷 ∈ ℕ0
Assertion nn0opth2i ( ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) ↑ 2 ) + 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )

### Proof

Step Hyp Ref Expression
1 nn0opth.1 𝐴 ∈ ℕ0
2 nn0opth.2 𝐵 ∈ ℕ0
3 nn0opth.3 𝐶 ∈ ℕ0
4 nn0opth.4 𝐷 ∈ ℕ0
5 1 nn0cni 𝐴 ∈ ℂ
6 2 nn0cni 𝐵 ∈ ℂ
7 5 6 addcli ( 𝐴 + 𝐵 ) ∈ ℂ
8 7 sqvali ( ( 𝐴 + 𝐵 ) ↑ 2 ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) )
9 8 oveq1i ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) + 𝐵 ) = ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 )
10 3 nn0cni 𝐶 ∈ ℂ
11 4 nn0cni 𝐷 ∈ ℂ
12 10 11 addcli ( 𝐶 + 𝐷 ) ∈ ℂ
13 12 sqvali ( ( 𝐶 + 𝐷 ) ↑ 2 ) = ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) )
14 13 oveq1i ( ( ( 𝐶 + 𝐷 ) ↑ 2 ) + 𝐷 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 )
15 9 14 eqeq12i ( ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) ↑ 2 ) + 𝐷 ) ↔ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) )
16 1 2 3 4 nn0opthi ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )
17 15 16 bitri ( ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) ↑ 2 ) + 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )