Metamath Proof Explorer

Theorem ax5seglem1

Description: Lemma for ax5seg . Rexpress a one congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem1 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NA⁡j−B⁡j2=T2⁢∑j=1NA⁡j−C⁡j2

Proof

Step Hyp Ref Expression
1 simpl2l ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→A∈𝔼⁡N
2 fveecn ⊢A∈𝔼⁡N∧j∈1…N→A⁡j∈ℂ
3 1 2 sylancom ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→A⁡j∈ℂ
4 simpl2r ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→C∈𝔼⁡N
5 fveecn ⊢C∈𝔼⁡N∧j∈1…N→C⁡j∈ℂ
6 4 5 sylancom ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→C⁡j∈ℂ
7 elicc01 ⊢T∈01↔T∈ℝ∧0≤T∧T≤1
8 7 simp1bi ⊢T∈01→T∈ℝ
9 8 adantr ⊢T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→T∈ℝ
10 9 3ad2ant3 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→T∈ℝ
11 10 recnd ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→T∈ℂ
12 11 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→T∈ℂ
13 fveq2 ⊢i=j→B⁡i=B⁡j
14 fveq2 ⊢i=j→A⁡i=A⁡j
15 14 oveq2d ⊢i=j→1−T⁢A⁡i=1−T⁢A⁡j
16 fveq2 ⊢i=j→C⁡i=C⁡j
17 16 oveq2d ⊢i=j→T⁢C⁡i=T⁢C⁡j
18 15 17 oveq12d ⊢i=j→1−T⁢A⁡i+T⁢C⁡i=1−T⁢A⁡j+T⁢C⁡j
19 13 18 eqeq12d ⊢i=j→B⁡i=1−T⁢A⁡i+T⁢C⁡i↔B⁡j=1−T⁢A⁡j+T⁢C⁡j
20 19 rspccva ⊢∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→B⁡j=1−T⁢A⁡j+T⁢C⁡j
21 20 adantll ⊢T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→B⁡j=1−T⁢A⁡j+T⁢C⁡j
22 21 3ad2antl3 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→B⁡j=1−T⁢A⁡j+T⁢C⁡j
23 oveq2 ⊢B⁡j=1−T⁢A⁡j+T⁢C⁡j→A⁡j−B⁡j=A⁡j−1−T⁢A⁡j+T⁢C⁡j
24 23 oveq1d ⊢B⁡j=1−T⁢A⁡j+T⁢C⁡j→A⁡j−B⁡j2=A⁡j−1−T⁢A⁡j+T⁢C⁡j2
25 subdi ⊢T∈ℂ∧A⁡j∈ℂ∧C⁡j∈ℂ→T⁢A⁡j−C⁡j=T⁢A⁡j−T⁢C⁡j
26 25 3coml ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→T⁢A⁡j−C⁡j=T⁢A⁡j−T⁢C⁡j
27 ax-1cn ⊢1∈ℂ
28 subcl ⊢1∈ℂ∧T∈ℂ→1−T∈ℂ
29 27 28 mpan ⊢T∈ℂ→1−T∈ℂ
30 29 adantl ⊢A⁡j∈ℂ∧T∈ℂ→1−T∈ℂ
31 simpl ⊢A⁡j∈ℂ∧T∈ℂ→A⁡j∈ℂ
32 subdir ⊢1∈ℂ∧1−T∈ℂ∧A⁡j∈ℂ→1−1−T⁢A⁡j=1⁢A⁡j−1−T⁢A⁡j
33 27 30 31 32 mp3an2i ⊢A⁡j∈ℂ∧T∈ℂ→1−1−T⁢A⁡j=1⁢A⁡j−1−T⁢A⁡j
34 nncan ⊢1∈ℂ∧T∈ℂ→1−1−T=T
35 27 34 mpan ⊢T∈ℂ→1−1−T=T
36 35 oveq1d ⊢T∈ℂ→1−1−T⁢A⁡j=T⁢A⁡j
37 36 adantl ⊢A⁡j∈ℂ∧T∈ℂ→1−1−T⁢A⁡j=T⁢A⁡j
38 mullid ⊢A⁡j∈ℂ→1⁢A⁡j=A⁡j
39 38 oveq1d ⊢A⁡j∈ℂ→1⁢A⁡j−1−T⁢A⁡j=A⁡j−1−T⁢A⁡j
40 39 adantr ⊢A⁡j∈ℂ∧T∈ℂ→1⁢A⁡j−1−T⁢A⁡j=A⁡j−1−T⁢A⁡j
41 33 37 40 3eqtr3rd ⊢A⁡j∈ℂ∧T∈ℂ→A⁡j−1−T⁢A⁡j=T⁢A⁡j
42 41 oveq1d ⊢A⁡j∈ℂ∧T∈ℂ→A⁡j-1−T⁢A⁡j-T⁢C⁡j=T⁢A⁡j−T⁢C⁡j
43 42 3adant2 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j-1−T⁢A⁡j-T⁢C⁡j=T⁢A⁡j−T⁢C⁡j
44 simp1 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j∈ℂ
45 mulcl ⊢1−T∈ℂ∧A⁡j∈ℂ→1−T⁢A⁡j∈ℂ
46 29 45 sylan ⊢T∈ℂ∧A⁡j∈ℂ→1−T⁢A⁡j∈ℂ
47 46 ancoms ⊢A⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j∈ℂ
48 47 3adant2 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j∈ℂ
49 mulcl ⊢T∈ℂ∧C⁡j∈ℂ→T⁢C⁡j∈ℂ
50 49 ancoms ⊢C⁡j∈ℂ∧T∈ℂ→T⁢C⁡j∈ℂ
51 50 3adant1 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→T⁢C⁡j∈ℂ
52 44 48 51 subsub4d ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j-1−T⁢A⁡j-T⁢C⁡j=A⁡j−1−T⁢A⁡j+T⁢C⁡j
53 26 43 52 3eqtr2rd ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j−1−T⁢A⁡j+T⁢C⁡j=T⁢A⁡j−C⁡j
54 53 oveq1d ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j−1−T⁢A⁡j+T⁢C⁡j2=T⁢A⁡j−C⁡j2
55 simp3 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→T∈ℂ
56 subcl ⊢A⁡j∈ℂ∧C⁡j∈ℂ→A⁡j−C⁡j∈ℂ
57 56 3adant3 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j−C⁡j∈ℂ
58 55 57 sqmuld ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→T⁢A⁡j−C⁡j2=T2⁢A⁡j−C⁡j2
59 54 58 eqtrd ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j−1−T⁢A⁡j+T⁢C⁡j2=T2⁢A⁡j−C⁡j2
60 24 59 sylan9eqr ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ∧B⁡j=1−T⁢A⁡j+T⁢C⁡j→A⁡j−B⁡j2=T2⁢A⁡j−C⁡j2
61 3 6 12 22 60 syl31anc ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→A⁡j−B⁡j2=T2⁢A⁡j−C⁡j2
62 61 sumeq2dv ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NA⁡j−B⁡j2=∑j=1NT2⁢A⁡j−C⁡j2
63 fzfid ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→1…N∈Fin
64 8 resqcld ⊢T∈01→T2∈ℝ
65 64 recnd ⊢T∈01→T2∈ℂ
66 65 adantr ⊢T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→T2∈ℂ
67 66 3ad2ant3 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→T2∈ℂ
68 2 3adant1 ⊢N∈ℕ∧A∈𝔼⁡N∧j∈1…N→A⁡j∈ℂ
69 68 3adant2r ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→A⁡j∈ℂ
70 5 3adant1 ⊢N∈ℕ∧C∈𝔼⁡N∧j∈1…N→C⁡j∈ℂ
71 70 3adant2l ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→C⁡j∈ℂ
72 69 71 subcld ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j∈ℂ
73 72 sqcld ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j2∈ℂ
74 73 3expa ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j2∈ℂ
75 74 3adantl3 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→A⁡j−C⁡j2∈ℂ
76 63 67 75 fsummulc2 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→T2⁢∑j=1NA⁡j−C⁡j2=∑j=1NT2⁢A⁡j−C⁡j2
77 62 76 eqtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NA⁡j−B⁡j2=T2⁢∑j=1NA⁡j−C⁡j2