This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0opth2

Description: An ordered pair theorem for nonnegative integers. Theorem 17.3 of Quine p. 124. See nn0opthi . (Contributed by NM, 22-Jul-2004)

Ref Expression
Assertion nn0opth2 
|- ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( C e. NN0 /\ D e. NN0 ) ) -> ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( A = C /\ B = D ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = if ( A e. NN0 , A , 0 ) -> ( A + B ) = ( if ( A e. NN0 , A , 0 ) + B ) )
2 1 oveq1d 
 |-  ( A = if ( A e. NN0 , A , 0 ) -> ( ( A + B ) ^ 2 ) = ( ( if ( A e. NN0 , A , 0 ) + B ) ^ 2 ) )
3 2 oveq1d 
 |-  ( A = if ( A e. NN0 , A , 0 ) -> ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( if ( A e. NN0 , A , 0 ) + B ) ^ 2 ) + B ) )
4 3 eqeq1d 
 |-  ( A = if ( A e. NN0 , A , 0 ) -> ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( ( ( if ( A e. NN0 , A , 0 ) + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) ) )
5 eqeq1 
 |-  ( A = if ( A e. NN0 , A , 0 ) -> ( A = C <-> if ( A e. NN0 , A , 0 ) = C ) )
6 5 anbi1d 
 |-  ( A = if ( A e. NN0 , A , 0 ) -> ( ( A = C /\ B = D ) <-> ( if ( A e. NN0 , A , 0 ) = C /\ B = D ) ) )
7 4 6 bibi12d 
 |-  ( A = if ( A e. NN0 , A , 0 ) -> ( ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( A = C /\ B = D ) ) <-> ( ( ( ( if ( A e. NN0 , A , 0 ) + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( if ( A e. NN0 , A , 0 ) = C /\ B = D ) ) ) )
8 oveq2 
 |-  ( B = if ( B e. NN0 , B , 0 ) -> ( if ( A e. NN0 , A , 0 ) + B ) = ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) )
9 8 oveq1d 
 |-  ( B = if ( B e. NN0 , B , 0 ) -> ( ( if ( A e. NN0 , A , 0 ) + B ) ^ 2 ) = ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) )
10 id 
 |-  ( B = if ( B e. NN0 , B , 0 ) -> B = if ( B e. NN0 , B , 0 ) )
11 9 10 oveq12d 
 |-  ( B = if ( B e. NN0 , B , 0 ) -> ( ( ( if ( A e. NN0 , A , 0 ) + B ) ^ 2 ) + B ) = ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) )
12 11 eqeq1d 
 |-  ( B = if ( B e. NN0 , B , 0 ) -> ( ( ( ( if ( A e. NN0 , A , 0 ) + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( C + D ) ^ 2 ) + D ) ) )
13 eqeq1 
 |-  ( B = if ( B e. NN0 , B , 0 ) -> ( B = D <-> if ( B e. NN0 , B , 0 ) = D ) )
14 13 anbi2d 
 |-  ( B = if ( B e. NN0 , B , 0 ) -> ( ( if ( A e. NN0 , A , 0 ) = C /\ B = D ) <-> ( if ( A e. NN0 , A , 0 ) = C /\ if ( B e. NN0 , B , 0 ) = D ) ) )
15 12 14 bibi12d 
 |-  ( B = if ( B e. NN0 , B , 0 ) -> ( ( ( ( ( if ( A e. NN0 , A , 0 ) + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( if ( A e. NN0 , A , 0 ) = C /\ B = D ) ) <-> ( ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( if ( A e. NN0 , A , 0 ) = C /\ if ( B e. NN0 , B , 0 ) = D ) ) ) )
16 oveq1 
 |-  ( C = if ( C e. NN0 , C , 0 ) -> ( C + D ) = ( if ( C e. NN0 , C , 0 ) + D ) )
17 16 oveq1d 
 |-  ( C = if ( C e. NN0 , C , 0 ) -> ( ( C + D ) ^ 2 ) = ( ( if ( C e. NN0 , C , 0 ) + D ) ^ 2 ) )
18 17 oveq1d 
 |-  ( C = if ( C e. NN0 , C , 0 ) -> ( ( ( C + D ) ^ 2 ) + D ) = ( ( ( if ( C e. NN0 , C , 0 ) + D ) ^ 2 ) + D ) )
19 18 eqeq2d 
 |-  ( C = if ( C e. NN0 , C , 0 ) -> ( ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( if ( C e. NN0 , C , 0 ) + D ) ^ 2 ) + D ) ) )
20 eqeq2 
 |-  ( C = if ( C e. NN0 , C , 0 ) -> ( if ( A e. NN0 , A , 0 ) = C <-> if ( A e. NN0 , A , 0 ) = if ( C e. NN0 , C , 0 ) ) )
21 20 anbi1d 
 |-  ( C = if ( C e. NN0 , C , 0 ) -> ( ( if ( A e. NN0 , A , 0 ) = C /\ if ( B e. NN0 , B , 0 ) = D ) <-> ( if ( A e. NN0 , A , 0 ) = if ( C e. NN0 , C , 0 ) /\ if ( B e. NN0 , B , 0 ) = D ) ) )
22 19 21 bibi12d 
 |-  ( C = if ( C e. NN0 , C , 0 ) -> ( ( ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( if ( A e. NN0 , A , 0 ) = C /\ if ( B e. NN0 , B , 0 ) = D ) ) <-> ( ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( if ( C e. NN0 , C , 0 ) + D ) ^ 2 ) + D ) <-> ( if ( A e. NN0 , A , 0 ) = if ( C e. NN0 , C , 0 ) /\ if ( B e. NN0 , B , 0 ) = D ) ) ) )
23 oveq2 
 |-  ( D = if ( D e. NN0 , D , 0 ) -> ( if ( C e. NN0 , C , 0 ) + D ) = ( if ( C e. NN0 , C , 0 ) + if ( D e. NN0 , D , 0 ) ) )
24 23 oveq1d 
 |-  ( D = if ( D e. NN0 , D , 0 ) -> ( ( if ( C e. NN0 , C , 0 ) + D ) ^ 2 ) = ( ( if ( C e. NN0 , C , 0 ) + if ( D e. NN0 , D , 0 ) ) ^ 2 ) )
25 id 
 |-  ( D = if ( D e. NN0 , D , 0 ) -> D = if ( D e. NN0 , D , 0 ) )
26 24 25 oveq12d 
 |-  ( D = if ( D e. NN0 , D , 0 ) -> ( ( ( if ( C e. NN0 , C , 0 ) + D ) ^ 2 ) + D ) = ( ( ( if ( C e. NN0 , C , 0 ) + if ( D e. NN0 , D , 0 ) ) ^ 2 ) + if ( D e. NN0 , D , 0 ) ) )
27 26 eqeq2d 
 |-  ( D = if ( D e. NN0 , D , 0 ) -> ( ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( if ( C e. NN0 , C , 0 ) + D ) ^ 2 ) + D ) <-> ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( if ( C e. NN0 , C , 0 ) + if ( D e. NN0 , D , 0 ) ) ^ 2 ) + if ( D e. NN0 , D , 0 ) ) ) )
28 eqeq2 
 |-  ( D = if ( D e. NN0 , D , 0 ) -> ( if ( B e. NN0 , B , 0 ) = D <-> if ( B e. NN0 , B , 0 ) = if ( D e. NN0 , D , 0 ) ) )
29 28 anbi2d 
 |-  ( D = if ( D e. NN0 , D , 0 ) -> ( ( if ( A e. NN0 , A , 0 ) = if ( C e. NN0 , C , 0 ) /\ if ( B e. NN0 , B , 0 ) = D ) <-> ( if ( A e. NN0 , A , 0 ) = if ( C e. NN0 , C , 0 ) /\ if ( B e. NN0 , B , 0 ) = if ( D e. NN0 , D , 0 ) ) ) )
30 27 29 bibi12d 
 |-  ( D = if ( D e. NN0 , D , 0 ) -> ( ( ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( if ( C e. NN0 , C , 0 ) + D ) ^ 2 ) + D ) <-> ( if ( A e. NN0 , A , 0 ) = if ( C e. NN0 , C , 0 ) /\ if ( B e. NN0 , B , 0 ) = D ) ) <-> ( ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( if ( C e. NN0 , C , 0 ) + if ( D e. NN0 , D , 0 ) ) ^ 2 ) + if ( D e. NN0 , D , 0 ) ) <-> ( if ( A e. NN0 , A , 0 ) = if ( C e. NN0 , C , 0 ) /\ if ( B e. NN0 , B , 0 ) = if ( D e. NN0 , D , 0 ) ) ) ) )
31 0nn0 
 |-  0 e. NN0
32 31 elimel 
 |-  if ( A e. NN0 , A , 0 ) e. NN0
33 31 elimel 
 |-  if ( B e. NN0 , B , 0 ) e. NN0
34 31 elimel 
 |-  if ( C e. NN0 , C , 0 ) e. NN0
35 31 elimel 
 |-  if ( D e. NN0 , D , 0 ) e. NN0
36 32 33 34 35 nn0opth2i 
 |-  ( ( ( ( if ( A e. NN0 , A , 0 ) + if ( B e. NN0 , B , 0 ) ) ^ 2 ) + if ( B e. NN0 , B , 0 ) ) = ( ( ( if ( C e. NN0 , C , 0 ) + if ( D e. NN0 , D , 0 ) ) ^ 2 ) + if ( D e. NN0 , D , 0 ) ) <-> ( if ( A e. NN0 , A , 0 ) = if ( C e. NN0 , C , 0 ) /\ if ( B e. NN0 , B , 0 ) = if ( D e. NN0 , D , 0 ) ) )
37 7 15 22 30 36 dedth4h 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( C e. NN0 /\ D e. NN0 ) ) -> ( ( ( ( A + B ) ^ 2 ) + B ) = ( ( ( C + D ) ^ 2 ) + D ) <-> ( A = C /\ B = D ) ) )