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 e. NN0
nn0opth.2 
|- B e. NN0
nn0opth.3 
|- C e. NN0
nn0opth.4 
|- D e. NN0
Assertion nn0opthi 
|- ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) <-> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 nn0opth.1 
 |-  A e. NN0
2 nn0opth.2 
 |-  B e. NN0
3 nn0opth.3 
 |-  C e. NN0
4 nn0opth.4 
 |-  D e. NN0
5 1 2 nn0addcli 
 |-  ( A + B ) e. NN0
6 5 nn0rei 
 |-  ( A + B ) e. RR
7 3 4 nn0addcli 
 |-  ( C + D ) e. NN0
8 7 nn0rei 
 |-  ( C + D ) e. RR
9 6 8 lttri2i 
 |-  ( ( A + B ) =/= ( C + D ) <-> ( ( A + B ) < ( C + D ) \/ ( C + D ) < ( A + B ) ) )
10 1 2 7 4 nn0opthlem2 
 |-  ( ( A + B ) < ( C + D ) -> ( ( ( C + D ) x. ( C + D ) ) + D ) =/= ( ( ( A + B ) x. ( A + B ) ) + B ) )
11 10 necomd 
 |-  ( ( A + B ) < ( C + D ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) =/= ( ( ( C + D ) x. ( C + D ) ) + D ) )
12 3 4 5 2 nn0opthlem2 
 |-  ( ( C + D ) < ( A + B ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) =/= ( ( ( C + D ) x. ( C + D ) ) + D ) )
13 11 12 jaoi 
 |-  ( ( ( A + B ) < ( C + D ) \/ ( C + D ) < ( A + B ) ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) =/= ( ( ( C + D ) x. ( C + D ) ) + D ) )
14 9 13 sylbi 
 |-  ( ( A + B ) =/= ( C + D ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) =/= ( ( ( C + D ) x. ( C + D ) ) + D ) )
15 14 necon4i 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> ( A + B ) = ( C + D ) )
16 id 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) )
17 15 15 oveq12d 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> ( ( A + B ) x. ( A + B ) ) = ( ( C + D ) x. ( C + D ) ) )
18 17 oveq1d 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> ( ( ( A + B ) x. ( A + B ) ) + D ) = ( ( ( C + D ) x. ( C + D ) ) + D ) )
19 16 18 eqtr4d 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( A + B ) x. ( A + B ) ) + D ) )
20 5 nn0cni 
 |-  ( A + B ) e. CC
21 20 20 mulcli 
 |-  ( ( A + B ) x. ( A + B ) ) e. CC
22 2 nn0cni 
 |-  B e. CC
23 4 nn0cni 
 |-  D e. CC
24 21 22 23 addcani 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( A + B ) x. ( A + B ) ) + D ) <-> B = D )
25 19 24 sylib 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> B = D )
26 25 oveq2d 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> ( C + B ) = ( C + D ) )
27 15 26 eqtr4d 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> ( A + B ) = ( C + B ) )
28 1 nn0cni 
 |-  A e. CC
29 3 nn0cni 
 |-  C e. CC
30 28 29 22 addcan2i 
 |-  ( ( A + B ) = ( C + B ) <-> A = C )
31 27 30 sylib 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> A = C )
32 31 25 jca 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) -> ( A = C /\ B = D ) )
33 oveq12 
 |-  ( ( A = C /\ B = D ) -> ( A + B ) = ( C + D ) )
34 33 33 oveq12d 
 |-  ( ( A = C /\ B = D ) -> ( ( A + B ) x. ( A + B ) ) = ( ( C + D ) x. ( C + D ) ) )
35 simpr 
 |-  ( ( A = C /\ B = D ) -> B = D )
36 34 35 oveq12d 
 |-  ( ( A = C /\ B = D ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) )
37 32 36 impbii 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) <-> ( A = C /\ B = D ) )