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 ( ( 𝐴 ∈ 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 )