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

Metamath Proof Explorer

Theorem addclnq

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 addclnq 
|- ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) e. Q. )

Proof

Step Hyp Ref Expression
1 addpqnq 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( /Q ` ( A +pQ B ) ) )
2 elpqn 
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
3 elpqn 
 |-  ( B e. Q. -> B e. ( N. X. N. ) )
4 addpqf 
 |-  +pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )
5 4 fovcl 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A +pQ B ) e. ( N. X. N. ) )
6 2 3 5 syl2an 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A +pQ B ) e. ( N. X. N. ) )
7 nqercl 
 |-  ( ( A +pQ B ) e. ( N. X. N. ) -> ( /Q ` ( A +pQ B ) ) e. Q. )
8 6 7 syl 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( /Q ` ( A +pQ B ) ) e. Q. )
9 1 8 eqeltrd 
 |-  ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) e. Q. )