Metamath Proof Explorer

Theorem ax5seglem4

Description: Lemma for ax5seg . Given two distinct points, the scaling constant in a betweenness statement is nonzero. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem4 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧A≠B→T≠0

Proof

Step Hyp Ref Expression
1 oveq2 ⊢T=0→1−T=1−0
2 1m0e1 ⊢1−0=1
3 1 2 eqtrdi ⊢T=0→1−T=1
4 3 oveq1d ⊢T=0→1−T⁢A⁡i=1⁢A⁡i
5 oveq1 ⊢T=0→T⁢C⁡i=0⋅C⁡i
6 4 5 oveq12d ⊢T=0→1−T⁢A⁡i+T⁢C⁡i=1⁢A⁡i+0⋅C⁡i
7 6 eqeq2d ⊢T=0→B⁡i=1−T⁢A⁡i+T⁢C⁡i↔B⁡i=1⁢A⁡i+0⋅C⁡i
8 7 ralbidv ⊢T=0→∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i↔∀i∈1…NB⁡i=1⁢A⁡i+0⋅C⁡i
9 8 biimpac ⊢∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧T=0→∀i∈1…NB⁡i=1⁢A⁡i+0⋅C⁡i
10 eqeefv ⊢A∈𝔼⁡N∧B∈𝔼⁡N→A=B↔∀i∈1…NA⁡i=B⁡i
11 10 3adant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→A=B↔∀i∈1…NA⁡i=B⁡i
12 11 3adant3r3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A=B↔∀i∈1…NA⁡i=B⁡i
13 simplr1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→A∈𝔼⁡N
14 fveecn ⊢A∈𝔼⁡N∧i∈1…N→A⁡i∈ℂ
15 13 14 sylancom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→A⁡i∈ℂ
16 simplr3 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→C∈𝔼⁡N
17 fveecn ⊢C∈𝔼⁡N∧i∈1…N→C⁡i∈ℂ
18 16 17 sylancom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→C⁡i∈ℂ
19 mullid ⊢A⁡i∈ℂ→1⁢A⁡i=A⁡i
20 mul02 ⊢C⁡i∈ℂ→0⋅C⁡i=0
21 19 20 oveqan12d ⊢A⁡i∈ℂ∧C⁡i∈ℂ→1⁢A⁡i+0⋅C⁡i=A⁡i+0
22 addrid ⊢A⁡i∈ℂ→A⁡i+0=A⁡i
23 22 adantr ⊢A⁡i∈ℂ∧C⁡i∈ℂ→A⁡i+0=A⁡i
24 21 23 eqtrd ⊢A⁡i∈ℂ∧C⁡i∈ℂ→1⁢A⁡i+0⋅C⁡i=A⁡i
25 15 18 24 syl2anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→1⁢A⁡i+0⋅C⁡i=A⁡i
26 25 eqeq1d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→1⁢A⁡i+0⋅C⁡i=B⁡i↔A⁡i=B⁡i
27 eqcom ⊢1⁢A⁡i+0⋅C⁡i=B⁡i↔B⁡i=1⁢A⁡i+0⋅C⁡i
28 26 27 bitr3di ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→A⁡i=B⁡i↔B⁡i=1⁢A⁡i+0⋅C⁡i
29 28 ralbidva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…NA⁡i=B⁡i↔∀i∈1…NB⁡i=1⁢A⁡i+0⋅C⁡i
30 12 29 bitrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A=B↔∀i∈1…NB⁡i=1⁢A⁡i+0⋅C⁡i
31 9 30 imbitrrid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧T=0→A=B
32 31 expdimp ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→T=0→A=B
33 32 necon3d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i→A≠B→T≠0
34 33 3impia ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧∀i∈1…NB⁡i=1−T⁢A⁡i+T⁢C⁡i∧A≠B→T≠0