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

Metamath Proof Explorer

Theorem addpqf

Description: Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion addpqf 
|- +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )

Proof

Step Hyp Ref Expression
1 xp1st 
 |-  ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
2 xp2nd 
 |-  ( y e. ( N. X. N. ) -> ( 2nd ` y ) e. N. )
3 mulclpi 
 |-  ( ( ( 1st ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. )
4 1 2 3 syl2an 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. )
5 xp1st 
 |-  ( y e. ( N. X. N. ) -> ( 1st ` y ) e. N. )
6 xp2nd 
 |-  ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. )
7 mulclpi 
 |-  ( ( ( 1st ` y ) e. N. /\ ( 2nd ` x ) e. N. ) -> ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. )
8 5 6 7 syl2anr 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. )
9 addclpi 
 |-  ( ( ( ( 1st ` x ) .N ( 2nd ` y ) ) e. N. /\ ( ( 1st ` y ) .N ( 2nd ` x ) ) e. N. ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) e. N. )
10 4 8 9 syl2anc 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) e. N. )
11 mulclpi 
 |-  ( ( ( 2nd ` x ) e. N. /\ ( 2nd ` y ) e. N. ) -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) e. N. )
12 6 2 11 syl2an 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> ( ( 2nd ` x ) .N ( 2nd ` y ) ) e. N. )
13 10 12 opelxpd 
 |-  ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) -> <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. ) )
14 13 rgen2 
 |-  A. x e. ( N. X. N. ) A. y e. ( N. X. N. ) <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. )
15 df-plpq 
 |-  +pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
16 15 fmpo 
 |-  ( A. x e. ( N. X. N. ) A. y e. ( N. X. N. ) <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. e. ( N. X. N. ) <-> +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. ) )
17 14 16 mpbi 
 |-  +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )