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