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

Proof

Step Hyp Ref Expression
1 nn0opth.1 𝐴 ∈ ℕ0
2 nn0opth.2 𝐵 ∈ ℕ0
3 nn0opth.3 𝐶 ∈ ℕ0
4 nn0opth.4 𝐷 ∈ ℕ0
5 1 2 nn0addcli ( 𝐴 + 𝐵 ) ∈ ℕ0
6 5 nn0rei ( 𝐴 + 𝐵 ) ∈ ℝ
7 3 4 nn0addcli ( 𝐶 + 𝐷 ) ∈ ℕ0
8 7 nn0rei ( 𝐶 + 𝐷 ) ∈ ℝ
9 6 8 lttri2i ( ( 𝐴 + 𝐵 ) ≠ ( 𝐶 + 𝐷 ) ↔ ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ∨ ( 𝐶 + 𝐷 ) < ( 𝐴 + 𝐵 ) ) )
10 1 2 7 4 nn0opthlem2 ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) → ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) ≠ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) )
11 10 necomd ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ≠ ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) )
12 3 4 5 2 nn0opthlem2 ( ( 𝐶 + 𝐷 ) < ( 𝐴 + 𝐵 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ≠ ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) )
13 11 12 jaoi ( ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ∨ ( 𝐶 + 𝐷 ) < ( 𝐴 + 𝐵 ) ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ≠ ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) )
14 9 13 sylbi ( ( 𝐴 + 𝐵 ) ≠ ( 𝐶 + 𝐷 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) ≠ ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) )
15 14 necon4i ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
16 id ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) )
17 15 15 oveq12d ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) = ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) )
18 17 oveq1d ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐷 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) )
19 16 18 eqtr4d ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐷 ) )
20 5 nn0cni ( 𝐴 + 𝐵 ) ∈ ℂ
21 20 20 mulcli ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) ∈ ℂ
22 2 nn0cni 𝐵 ∈ ℂ
23 4 nn0cni 𝐷 ∈ ℂ
24 21 22 23 addcani ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐷 ) ↔ 𝐵 = 𝐷 )
25 19 24 sylib ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → 𝐵 = 𝐷 )
26 25 oveq2d ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → ( 𝐶 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
27 15 26 eqtr4d ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐵 ) )
28 1 nn0cni 𝐴 ∈ ℂ
29 3 nn0cni 𝐶 ∈ ℂ
30 28 29 22 addcan2i ( ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐵 ) ↔ 𝐴 = 𝐶 )
31 27 30 sylib ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → 𝐴 = 𝐶 )
32 31 25 jca ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) )
33 oveq12 ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
34 33 33 oveq12d ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) = ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) )
35 simpr ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → 𝐵 = 𝐷 )
36 34 35 oveq12d ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) )
37 32 36 impbii ( ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) + 𝐵 ) = ( ( ( 𝐶 + 𝐷 ) · ( 𝐶 + 𝐷 ) ) + 𝐷 ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) )