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