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∈ℝ