Metamath Proof Explorer

Theorem ax5seglem2

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

Ref Expression
Assertion ax5seglem2 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NB⁡j−C⁡j2=1−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 recnd ⊢T∈01→T∈ℂ
10 9 adantr ⊢T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→T∈ℂ
11 10 3ad2ant3 ⊢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 oveq1 ⊢B⁡j=1−T⁢A⁡j+T⁢C⁡j→B⁡j−C⁡j=1−T⁢A⁡j+T⁢C⁡j-C⁡j
24 23 oveq1d ⊢B⁡j=1−T⁢A⁡j+T⁢C⁡j→B⁡j−C⁡j2=1−T⁢A⁡j+T⁢C⁡j-C⁡j2
25 ax-1cn ⊢1∈ℂ
26 subcl ⊢1∈ℂ∧T∈ℂ→1−T∈ℂ
27 25 26 mpan ⊢T∈ℂ→1−T∈ℂ
28 27 3ad2ant3 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T∈ℂ
29 simp1 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j∈ℂ
30 28 29 mulcld ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j∈ℂ
31 simp3 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→T∈ℂ
32 simp2 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→C⁡j∈ℂ
33 31 32 mulcld ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→T⁢C⁡j∈ℂ
34 30 33 32 addsubassd ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j+T⁢C⁡j-C⁡j=1−T⁢A⁡j+T⁢C⁡j-C⁡j
35 subdi ⊢1−T∈ℂ∧A⁡j∈ℂ∧C⁡j∈ℂ→1−T⁢A⁡j−C⁡j=1−T⁢A⁡j−1−T⁢C⁡j
36 27 35 syl3an1 ⊢T∈ℂ∧A⁡j∈ℂ∧C⁡j∈ℂ→1−T⁢A⁡j−C⁡j=1−T⁢A⁡j−1−T⁢C⁡j
37 36 3coml ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j−C⁡j=1−T⁢A⁡j−1−T⁢C⁡j
38 subdir ⊢1∈ℂ∧T∈ℂ∧C⁡j∈ℂ→1−T⁢C⁡j=1⁢C⁡j−T⁢C⁡j
39 25 38 mp3an1 ⊢T∈ℂ∧C⁡j∈ℂ→1−T⁢C⁡j=1⁢C⁡j−T⁢C⁡j
40 39 ancoms ⊢C⁡j∈ℂ∧T∈ℂ→1−T⁢C⁡j=1⁢C⁡j−T⁢C⁡j
41 40 3adant1 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢C⁡j=1⁢C⁡j−T⁢C⁡j
42 mullid ⊢C⁡j∈ℂ→1⁢C⁡j=C⁡j
43 42 oveq1d ⊢C⁡j∈ℂ→1⁢C⁡j−T⁢C⁡j=C⁡j−T⁢C⁡j
44 43 3ad2ant2 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1⁢C⁡j−T⁢C⁡j=C⁡j−T⁢C⁡j
45 41 44 eqtrd ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢C⁡j=C⁡j−T⁢C⁡j
46 45 oveq2d ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j−1−T⁢C⁡j=1−T⁢A⁡j−C⁡j−T⁢C⁡j
47 30 32 33 subsub2d ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j−C⁡j−T⁢C⁡j=1−T⁢A⁡j+T⁢C⁡j-C⁡j
48 37 46 47 3eqtrd ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j−C⁡j=1−T⁢A⁡j+T⁢C⁡j-C⁡j
49 34 48 eqtr4d ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j+T⁢C⁡j-C⁡j=1−T⁢A⁡j−C⁡j
50 49 oveq1d ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j+T⁢C⁡j-C⁡j2=1−T⁢A⁡j−C⁡j2
51 subcl ⊢A⁡j∈ℂ∧C⁡j∈ℂ→A⁡j−C⁡j∈ℂ
52 51 3adant3 ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→A⁡j−C⁡j∈ℂ
53 28 52 sqmuld ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j−C⁡j2=1−T2⁢A⁡j−C⁡j2
54 50 53 eqtrd ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ→1−T⁢A⁡j+T⁢C⁡j-C⁡j2=1−T2⁢A⁡j−C⁡j2
55 24 54 sylan9eqr ⊢A⁡j∈ℂ∧C⁡j∈ℂ∧T∈ℂ∧B⁡j=1−T⁢A⁡j+T⁢C⁡j→B⁡j−C⁡j2=1−T2⁢A⁡j−C⁡j2
56 3 6 12 22 55 syl31anc ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧j∈1…N→B⁡j−C⁡j2=1−T2⁢A⁡j−C⁡j2
57 56 sumeq2dv ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NB⁡j−C⁡j2=∑j=1N1−T2⁢A⁡j−C⁡j2
58 fzfid ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→1…N∈Fin
59 1re ⊢1∈ℝ
60 resubcl ⊢1∈ℝ∧T∈ℝ→1−T∈ℝ
61 59 8 60 sylancr ⊢T∈01→1−T∈ℝ
62 61 resqcld ⊢T∈01→1−T2∈ℝ
63 62 recnd ⊢T∈01→1−T2∈ℂ
64 63 adantr ⊢T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→1−T2∈ℂ
65 64 3ad2ant3 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→1−T2∈ℂ
66 2 3adant1 ⊢N∈ℕ∧A∈𝔼⁡N∧j∈1…N→A⁡j∈ℂ
67 66 3adant2r ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→A⁡j∈ℂ
68 5 3adant1 ⊢N∈ℕ∧C∈𝔼⁡N∧j∈1…N→C⁡j∈ℂ
69 68 3adant2l ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→C⁡j∈ℂ
70 67 69 subcld ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j∈ℂ
71 70 sqcld ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j2∈ℂ
72 71 3expa ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→A⁡j−C⁡j2∈ℂ
73 72 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∈ℂ
74 58 65 73 fsummulc2 ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→1−T2⁢∑j=1NA⁡j−C⁡j2=∑j=1N1−T2⁢A⁡j−C⁡j2
75 57 74 eqtr4d ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NB⁡j−C⁡j2=1−T2⁢∑j=1NA⁡j−C⁡j2