Metamath Proof Explorer

Theorem eleesubd

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

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

Proof

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