Metamath Proof Explorer

Theorem nn0opthi

Description: An ordered pair theorem for nonnegative integers. Theorem 17.3 of Quine p. 124. We can represent an ordered pair of nonnegative integers A and B by ( ( ( A + B ) x. ( A + B ) ) + B ) . If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op that works for any set. (Contributed by Raph Levien, 10-Dec-2002) (Proof shortened by Scott Fenton, 8-Sep-2010)

Ref Expression
Hypotheses nn0opth.1 ${⊢}{A}\in {ℕ}_{0}$
nn0opth.2 ${⊢}{B}\in {ℕ}_{0}$
nn0opth.3 ${⊢}{C}\in {ℕ}_{0}$
nn0opth.4 ${⊢}{D}\in {ℕ}_{0}$
Assertion nn0opthi ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}↔\left({A}={C}\wedge {B}={D}\right)$

Proof

Step Hyp Ref Expression
1 nn0opth.1 ${⊢}{A}\in {ℕ}_{0}$
2 nn0opth.2 ${⊢}{B}\in {ℕ}_{0}$
3 nn0opth.3 ${⊢}{C}\in {ℕ}_{0}$
4 nn0opth.4 ${⊢}{D}\in {ℕ}_{0}$
5 1 2 nn0addcli ${⊢}{A}+{B}\in {ℕ}_{0}$
6 5 nn0rei ${⊢}{A}+{B}\in ℝ$
7 3 4 nn0addcli ${⊢}{C}+{D}\in {ℕ}_{0}$
8 7 nn0rei ${⊢}{C}+{D}\in ℝ$
9 6 8 lttri2i ${⊢}{A}+{B}\ne {C}+{D}↔\left({A}+{B}<{C}+{D}\vee {C}+{D}<{A}+{B}\right)$
10 1 2 7 4 nn0opthlem2 ${⊢}{A}+{B}<{C}+{D}\to \left({C}+{D}\right)\left({C}+{D}\right)+{D}\ne \left({A}+{B}\right)\left({A}+{B}\right)+{B}$
11 10 necomd ${⊢}{A}+{B}<{C}+{D}\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}\ne \left({C}+{D}\right)\left({C}+{D}\right)+{D}$
12 3 4 5 2 nn0opthlem2 ${⊢}{C}+{D}<{A}+{B}\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}\ne \left({C}+{D}\right)\left({C}+{D}\right)+{D}$
13 11 12 jaoi ${⊢}\left({A}+{B}<{C}+{D}\vee {C}+{D}<{A}+{B}\right)\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}\ne \left({C}+{D}\right)\left({C}+{D}\right)+{D}$
14 9 13 sylbi ${⊢}{A}+{B}\ne {C}+{D}\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}\ne \left({C}+{D}\right)\left({C}+{D}\right)+{D}$
15 14 necon4i ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to {A}+{B}={C}+{D}$
16 id ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}$
17 15 15 oveq12d ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to \left({A}+{B}\right)\left({A}+{B}\right)=\left({C}+{D}\right)\left({C}+{D}\right)$
18 17 oveq1d ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to \left({A}+{B}\right)\left({A}+{B}\right)+{D}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}$
19 16 18 eqtr4d ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({A}+{B}\right)\left({A}+{B}\right)+{D}$
20 5 nn0cni ${⊢}{A}+{B}\in ℂ$
21 20 20 mulcli ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)\in ℂ$
22 2 nn0cni ${⊢}{B}\in ℂ$
23 4 nn0cni ${⊢}{D}\in ℂ$
24 21 22 23 addcani ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({A}+{B}\right)\left({A}+{B}\right)+{D}↔{B}={D}$
25 19 24 sylib ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to {B}={D}$
26 25 oveq2d ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to {C}+{B}={C}+{D}$
27 15 26 eqtr4d ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to {A}+{B}={C}+{B}$
28 1 nn0cni ${⊢}{A}\in ℂ$
29 3 nn0cni ${⊢}{C}\in ℂ$
30 28 29 22 addcan2i ${⊢}{A}+{B}={C}+{B}↔{A}={C}$
31 27 30 sylib ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to {A}={C}$
32 31 25 jca ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}\to \left({A}={C}\wedge {B}={D}\right)$
33 oveq12 ${⊢}\left({A}={C}\wedge {B}={D}\right)\to {A}+{B}={C}+{D}$
34 33 33 oveq12d ${⊢}\left({A}={C}\wedge {B}={D}\right)\to \left({A}+{B}\right)\left({A}+{B}\right)=\left({C}+{D}\right)\left({C}+{D}\right)$
35 simpr ${⊢}\left({A}={C}\wedge {B}={D}\right)\to {B}={D}$
36 34 35 oveq12d ${⊢}\left({A}={C}\wedge {B}={D}\right)\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}$
37 32 36 impbii ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}=\left({C}+{D}\right)\left({C}+{D}\right)+{D}↔\left({A}={C}\wedge {B}={D}\right)$