Metamath Proof Explorer

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 
|- A e. NN0
nn0opth.2 
|- B e. NN0
nn0opth.3 
|- C e. NN0
nn0opth.4 
|- D e. NN0
Assertion nn0opth2i 
|- ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + 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 nn0cni 
 |-  A e. CC
6 2 nn0cni 
 |-  B e. CC
7 5 6 addcli 
 |-  ( A + B ) e. CC
8 7 sqvali 
 |-  ( ( A + B ) ^ 2 ) = ( ( A + B ) x. ( A + B ) )
9 8 oveq1i 
 |-  ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( A + B ) x. ( A + B ) ) + B )
10 3 nn0cni 
 |-  C e. CC
11 4 nn0cni 
 |-  D e. CC
12 10 11 addcli 
 |-  ( C + D ) e. CC
13 12 sqvali 
 |-  ( ( C + D ) ^ 2 ) = ( ( C + D ) x. ( C + D ) )
14 13 oveq1i 
 |-  ( ( ( C + D ) ^ 2 ) + D ) = ( ( ( C + D ) x. ( C + D ) ) + D )
15 9 14 eqeq12i 
 |-  ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) )
16 1 2 3 4 nn0opthi 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) = ( ( ( C + D ) x. ( C + D ) ) + D ) <-> ( A = C /\ B = D ) )
17 15 16 bitri 
 |-  ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( A = C /\ B = D ) )