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. )