This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℕ 0
nn0opth.2 ⊢ B ∈ ℕ 0
nn0opth.3 ⊢ C ∈ ℕ 0
nn0opth.4 ⊢ D ∈ ℕ 0
Assertion nn0opth2i ⊢ A + B 2 + B = C + D 2 + D ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 nn0opth.1 ⊢ A ∈ ℕ 0
2 nn0opth.2 ⊢ B ∈ ℕ 0
3 nn0opth.3 ⊢ C ∈ ℕ 0
4 nn0opth.4 ⊢ D ∈ ℕ 0
5 1 nn0cni ⊢ A ∈ ℂ
6 2 nn0cni ⊢ B ∈ ℂ
7 5 6 addcli ⊢ A + B ∈ ℂ
8 7 sqvali ⊢ A + B 2 = A + B ⁢ A + B
9 8 oveq1i ⊢ A + B 2 + B = A + B ⁢ A + B + B
10 3 nn0cni ⊢ C ∈ ℂ
11 4 nn0cni ⊢ D ∈ ℂ
12 10 11 addcli ⊢ C + D ∈ ℂ
13 12 sqvali ⊢ C + D 2 = C + D ⁢ C + D
14 13 oveq1i ⊢ C + D 2 + D = C + D ⁢ C + D + D
15 9 14 eqeq12i ⊢ A + B 2 + B = C + D 2 + D ↔ A + B ⁢ A + B + B = C + D ⁢ C + D + D
16 1 2 3 4 nn0opthi ⊢ A + B ⁢ A + B + B = C + D ⁢ C + D + D ↔ A = C ∧ B = D
17 15 16 bitri ⊢ A + B 2 + B = C + D 2 + D ↔ A = C ∧ B = D