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 ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → ∑ j = 1 N A ⁡ j − C ⁡ j 2 ≠ 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 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ A ⁡ i ↔ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i
6 5 biimparc ⊢ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i ∧ A = C → ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ A ⁡ i
7 simplr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 → A ∈ 𝔼 ⁡ N
8 simplr2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 → B ∈ 𝔼 ⁡ N
9 eqeefv ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
10 7 8 9 syl2anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
11 fveecn ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
12 7 11 sylan ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
13 elicc01 ⊢ T ∈ 0 1 ↔ T ∈ ℝ ∧ 0 ≤ T ∧ T ≤ 1
14 13 simp1bi ⊢ T ∈ 0 1 → T ∈ ℝ
15 14 recnd ⊢ T ∈ 0 1 → T ∈ ℂ
16 15 ad2antlr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 ∧ 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 mulid2 ⊢ 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 ∈ 0 1 ∧ 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 ∈ 0 1 ∧ 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 ∈ 0 1 → ∀ i ∈ 1 … N A ⁡ i = B ⁡ i ↔ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ A ⁡ i
35 10 34 bitrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 → A = B ↔ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ A ⁡ i
36 6 35 syl5ibr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 → ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i ∧ A = C → A = B
37 36 expd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 → ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A = C → A = B
38 37 impr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A = C → A = B
39 38 necon3d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A ≠ B → A ≠ C
40 39 ex ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ 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 ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A ≠ C
42 41 exp4a ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A ≠ B → T ∈ 0 1 → ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A ≠ C
43 42 3imp2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A ≠ C
44 simplr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A ∈ 𝔼 ⁡ N
45 simplr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → C ∈ 𝔼 ⁡ N
46 eqeelen ⊢ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A = C ↔ ∑ j = 1 N A ⁡ j − C ⁡ j 2 = 0
47 44 45 46 syl2anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A = C ↔ ∑ j = 1 N A ⁡ j − C ⁡ j 2 = 0
48 47 necon3bid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A ≠ C ↔ ∑ j = 1 N A ⁡ j − C ⁡ j 2 ≠ 0
49 43 48 mpbid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ T ∈ 0 1 ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → ∑ j = 1 N A ⁡ j − C ⁡ j 2 ≠ 0