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 ( ( 𝐴Q𝐵Q ) → ( 𝐴 +Q 𝐵 ) ∈ Q )

Proof

Step Hyp Ref Expression
1 addpqnq ( ( 𝐴Q𝐵Q ) → ( 𝐴 +Q 𝐵 ) = ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) )
2 elpqn ( 𝐴Q𝐴 ∈ ( N × N ) )
3 elpqn ( 𝐵Q𝐵 ∈ ( N × N ) )
4 addpqf +pQ : ( ( N × N ) × ( N × N ) ) ⟶ ( N × N )
5 4 fovcl ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 +pQ 𝐵 ) ∈ ( N × N ) )
6 2 3 5 syl2an ( ( 𝐴Q𝐵Q ) → ( 𝐴 +pQ 𝐵 ) ∈ ( N × N ) )
7 nqercl ( ( 𝐴 +pQ 𝐵 ) ∈ ( N × N ) → ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) ∈ Q )
8 6 7 syl ( ( 𝐴Q𝐵Q ) → ( [Q] ‘ ( 𝐴 +pQ 𝐵 ) ) ∈ Q )
9 1 8 eqeltrd ( ( 𝐴Q𝐵Q ) → ( 𝐴 +Q 𝐵 ) ∈ Q )