Metamath Proof Explorer

Theorem ax5seglem3a

Description: Lemma for ax5seg . (Contributed by Scott Fenton, 7-May-2015)

Ref Expression
Assertion ax5seglem3a ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → A ⁡ j − C ⁡ j ∈ ℝ ∧ D ⁡ j − F ⁡ j ∈ ℝ

Proof

Step Hyp Ref Expression
1 simpl21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → A ∈ 𝔼 ⁡ N
2 fveere ⊢ A ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → A ⁡ j ∈ ℝ
3 1 2 sylancom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → A ⁡ j ∈ ℝ
4 simpl23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → C ∈ 𝔼 ⁡ N
5 fveere ⊢ C ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → C ⁡ j ∈ ℝ
6 4 5 sylancom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → C ⁡ j ∈ ℝ
7 3 6 resubcld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → A ⁡ j − C ⁡ j ∈ ℝ
8 simpl31 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → D ∈ 𝔼 ⁡ N
9 fveere ⊢ D ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → D ⁡ j ∈ ℝ
10 8 9 sylancom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → D ⁡ j ∈ ℝ
11 simpl33 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → F ∈ 𝔼 ⁡ N
12 fveere ⊢ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → F ⁡ j ∈ ℝ
13 11 12 sylancom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → F ⁡ j ∈ ℝ
14 10 13 resubcld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → D ⁡ j − F ⁡ j ∈ ℝ
15 7 14 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ j ∈ 1 … N → A ⁡ j − C ⁡ j ∈ ℝ ∧ D ⁡ j − F ⁡ j ∈ ℝ