Metamath Proof Explorer

Theorem axsegconlem8

Description: Lemma for axsegcon . Show that a particular mapping generates a point. (Contributed by Scott Fenton, 18-Sep-2013)

Ref Expression
Hypotheses axsegconlem2.1 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
axsegconlem7.2 ⊢ T = ∑ p = 1 N C ⁡ p − D ⁡ p 2
axsegconlem8.3 ⊢ F = k ∈ 1 … N ⟼ S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S
Assertion axsegconlem8 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → F ∈ 𝔼 ⁡ N

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
2 axsegconlem7.2 ⊢ T = ∑ p = 1 N C ⁡ p − D ⁡ p 2
3 axsegconlem8.3 ⊢ F = k ∈ 1 … N ⟼ S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S
4 1 axsegconlem4 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → S ∈ ℝ
5 4 3adant3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → S ∈ ℝ
6 5 ad2antrr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → S ∈ ℝ
7 2 axsegconlem4 ⊢ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → T ∈ ℝ
8 7 ad2antlr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → T ∈ ℝ
9 6 8 readdcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → S + T ∈ ℝ
10 simpl2 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
11 fveere ⊢ B ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → B ⁡ k ∈ ℝ
12 10 11 sylan ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → B ⁡ k ∈ ℝ
13 9 12 remulcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → S + T ⁢ B ⁡ k ∈ ℝ
14 simpl1 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
15 fveere ⊢ A ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → A ⁡ k ∈ ℝ
16 14 15 sylan ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → A ⁡ k ∈ ℝ
17 8 16 remulcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → T ⁢ A ⁡ k ∈ ℝ
18 13 17 resubcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → S + T ⁢ B ⁡ k − T ⁢ A ⁡ k ∈ ℝ
19 1 axsegconlem6 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → 0 < S
20 19 gt0ne0d ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → S ≠ 0
21 20 ad2antrr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → S ≠ 0
22 18 6 21 redivcld ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ k ∈ 1 … N → S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S ∈ ℝ
23 22 ralrimiva ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∀ k ∈ 1 … N S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S ∈ ℝ
24 eleenn ⊢ D ∈ 𝔼 ⁡ N → N ∈ ℕ
25 24 ad2antll ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → N ∈ ℕ
26 mptelee ⊢ N ∈ ℕ → k ∈ 1 … N ⟼ S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S ∈ 𝔼 ⁡ N ↔ ∀ k ∈ 1 … N S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S ∈ ℝ
27 25 26 syl ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → k ∈ 1 … N ⟼ S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S ∈ 𝔼 ⁡ N ↔ ∀ k ∈ 1 … N S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S ∈ ℝ
28 23 27 mpbird ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → k ∈ 1 … N ⟼ S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S ∈ 𝔼 ⁡ N
29 3 28 eqeltrid ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → F ∈ 𝔼 ⁡ N