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 ) + 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )