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=1NA⁡p−B⁡p2
axsegconlem7.2 ⊢T=∑p=1NC⁡p−D⁡p2
axsegconlem8.3 ⊢F=k∈1…N⟼S+T⁢B⁡k−T⁢A⁡kS
Assertion axsegconlem8 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→F∈𝔼⁡N

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢S=∑p=1NA⁡p−B⁡p2
2 axsegconlem7.2 ⊢T=∑p=1NC⁡p−D⁡p2
3 axsegconlem8.3 ⊢F=k∈1…N⟼S+T⁢B⁡k−T⁢A⁡kS
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⁡kS∈ℝ
23 22 ralrimiva ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→∀k∈1…NS+T⁢B⁡k−T⁢A⁡kS∈ℝ
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⁡kS∈𝔼⁡N↔∀k∈1…NS+T⁢B⁡k−T⁢A⁡kS∈ℝ
27 25 26 syl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→k∈1…N⟼S+T⁢B⁡k−T⁢A⁡kS∈𝔼⁡N↔∀k∈1…NS+T⁢B⁡k−T⁢A⁡kS∈ℝ
28 23 27 mpbird ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→k∈1…N⟼S+T⁢B⁡k−T⁢A⁡kS∈𝔼⁡N
29 3 28 eqeltrid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧A≠B∧C∈𝔼⁡N∧D∈𝔼⁡N→F∈𝔼⁡N