Metamath Proof Explorer

Theorem eleesub

Description: Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013)

Ref Expression
Hypothesis eleesub.1 ⊢C=i∈1…N⟼A⁡i−B⁡i
Assertion eleesub ⊢A∈𝔼⁡N∧B∈𝔼⁡N→C∈𝔼⁡N

Proof

Step Hyp Ref Expression
1 eleesub.1 ⊢C=i∈1…N⟼A⁡i−B⁡i
2 fveere ⊢A∈𝔼⁡N∧i∈1…N→A⁡i∈ℝ
3 fveere ⊢B∈𝔼⁡N∧i∈1…N→B⁡i∈ℝ
4 resubcl ⊢A⁡i∈ℝ∧B⁡i∈ℝ→A⁡i−B⁡i∈ℝ
5 2 3 4 syl2an ⊢A∈𝔼⁡N∧i∈1…N∧B∈𝔼⁡N∧i∈1…N→A⁡i−B⁡i∈ℝ
6 5 anandirs ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧i∈1…N→A⁡i−B⁡i∈ℝ
7 6 ralrimiva ⊢A∈𝔼⁡N∧B∈𝔼⁡N→∀i∈1…NA⁡i−B⁡i∈ℝ
8 eleenn ⊢A∈𝔼⁡N→N∈ℕ
9 mptelee ⊢N∈ℕ→i∈1…N⟼A⁡i−B⁡i∈𝔼⁡N↔∀i∈1…NA⁡i−B⁡i∈ℝ
10 8 9 syl ⊢A∈𝔼⁡N→i∈1…N⟼A⁡i−B⁡i∈𝔼⁡N↔∀i∈1…NA⁡i−B⁡i∈ℝ
11 10 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N→i∈1…N⟼A⁡i−B⁡i∈𝔼⁡N↔∀i∈1…NA⁡i−B⁡i∈ℝ
12 7 11 mpbird ⊢A∈𝔼⁡N∧B∈𝔼⁡N→i∈1…N⟼A⁡i−B⁡i∈𝔼⁡N
13 1 12 eqeltrid ⊢A∈𝔼⁡N∧B∈𝔼⁡N→C∈𝔼⁡N