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 … N A ⁡ i − B ⁡ i ∈ ℝ
8 eleenn ⊢ A ∈ 𝔼 ⁡ N → N ∈ ℕ
9 mptelee ⊢ N ∈ ℕ → i ∈ 1 … N ⟼ A ⁡ i − B ⁡ i ∈ 𝔼 ⁡ N ↔ ∀ i ∈ 1 … N A ⁡ i − B ⁡ i ∈ ℝ
10 8 9 syl ⊢ A ∈ 𝔼 ⁡ N → i ∈ 1 … N ⟼ A ⁡ i − B ⁡ i ∈ 𝔼 ⁡ N ↔ ∀ i ∈ 1 … N A ⁡ i − B ⁡ i ∈ ℝ
11 10 adantr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → i ∈ 1 … N ⟼ A ⁡ i − B ⁡ i ∈ 𝔼 ⁡ N ↔ ∀ i ∈ 1 … N A ⁡ 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