Metamath Proof Explorer

Theorem ax5seglem5

Description: Lemma for ax5seg . If B is between A and C , and A is distinct from B , then A is distinct from C . (Contributed by Scott Fenton, 11-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 fveq1 ⊢A=C→A⁡i=C⁡i
2 1 oveq2d ⊢A=C→T⁢A⁡i=T⁢C⁡i
3 2 oveq2d ⊢A=C→1−T⁢A⁡i+T⁢A⁡i=1−T⁢A⁡i+T⁢C⁡i
4 3 eqeq2d ⊢A=C→B⁡i=1−T⁢A⁡i+T⁢A⁡i↔B⁡i=1−T⁢A⁡i+T⁢C⁡i
5 4 ralbidv ⊢A=C→∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢A⁡i↔∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i
6 5 biimparc ⊢∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧A=C→∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢A⁡i
7 simplr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01→A∈𝔼⁡N
8 simplr2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01→B∈𝔼⁡N
9 eqeefv ⊢A∈𝔼⁡N∧B∈𝔼⁡N→A=B↔∀i∈1…NA⁡i=B⁡i
10 7 8 9 syl2anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01→A=B↔∀i∈1…NA⁡i=B⁡i
11 fveecn ⊢A∈𝔼⁡N∧i∈1…N→A⁡i∈ℂ
12 7 11 sylan ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧i∈1…N→A⁡i∈ℂ
13 elicc01 ⊢T∈01↔T∈ℝ∧0≤T∧T≤1
14 13 simp1bi ⊢T∈01→T∈ℝ
15 14 recnd ⊢T∈01→T∈ℂ
16 15 ad2antlr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧i∈1…N→T∈ℂ
17 ax-1cn ⊢1∈ℂ
18 npcan ⊢1∈ℂ∧T∈ℂ→1-T+T=1
19 17 18 mpan ⊢T∈ℂ→1-T+T=1
20 19 oveq1d ⊢T∈ℂ→1-T+T⁢A⁡i=1⁢A⁡i
21 mullid ⊢A⁡i∈ℂ→1⁢A⁡i=A⁡i
22 20 21 sylan9eqr ⊢A⁡i∈ℂ∧T∈ℂ→1-T+T⁢A⁡i=A⁡i
23 subcl ⊢1∈ℂ∧T∈ℂ→1−T∈ℂ
24 17 23 mpan ⊢T∈ℂ→1−T∈ℂ
25 24 adantl ⊢A⁡i∈ℂ∧T∈ℂ→1−T∈ℂ
26 simpr ⊢A⁡i∈ℂ∧T∈ℂ→T∈ℂ
27 simpl ⊢A⁡i∈ℂ∧T∈ℂ→A⁡i∈ℂ
28 25 26 27 adddird ⊢A⁡i∈ℂ∧T∈ℂ→1-T+T⁢A⁡i=1−T⁢A⁡i+T⁢A⁡i
29 22 28 eqtr3d ⊢A⁡i∈ℂ∧T∈ℂ→A⁡i=1−T⁢A⁡i+T⁢A⁡i
30 29 eqeq1d ⊢A⁡i∈ℂ∧T∈ℂ→A⁡i=B⁡i↔1−T⁢A⁡i+T⁢A⁡i=B⁡i
31 12 16 30 syl2anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧i∈1…N→A⁡i=B⁡i↔1−T⁢A⁡i+T⁢A⁡i=B⁡i
32 eqcom ⊢1−T⁢A⁡i+T⁢A⁡i=B⁡i↔B⁡i=1−T⁢A⁡i+T⁢A⁡i
33 31 32 bitrdi ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧i∈1…N→A⁡i=B⁡i↔B⁡i=1−T⁢A⁡i+T⁢A⁡i
34 33 ralbidva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01→∀i∈1…NA⁡i=B⁡i↔∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢A⁡i
35 10 34 bitrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01→A=B↔∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢A⁡i
36 6 35 imbitrrid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01→∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧A=C→A=B
37 36 expd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01→∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A=C→A=B
38 37 impr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A=C→A=B
39 38 necon3d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A≠B→A≠C
40 39 ex ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A≠B→A≠C
41 40 com23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A≠B→T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A≠C
42 41 exp4a ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A≠B→T∈01→∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A≠C
43 42 3imp2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A≠B∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A≠C
44 simplr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A≠B∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A∈𝔼⁡N
45 simplr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A≠B∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→C∈𝔼⁡N
46 eqeelen ⊢A∈𝔼⁡N∧C∈𝔼⁡N→A=C↔∑j=1NA⁡j−C⁡j2=0
47 44 45 46 syl2anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A≠B∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A=C↔∑j=1NA⁡j−C⁡j2=0
48 47 necon3bid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A≠B∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A≠C↔∑j=1NA⁡j−C⁡j2≠0
49 43 48 mpbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧A≠B∧T∈01∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→∑j=1NA⁡j−C⁡j2≠0