Proof of Theorem ax5seglem5
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq1 6904 | . . . . . . . . . . . . . . 15
⊢ (𝐴 = 𝐶 → (𝐴‘𝑖) = (𝐶‘𝑖)) | 
| 2 | 1 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝐴 = 𝐶 → (𝑇 · (𝐴‘𝑖)) = (𝑇 · (𝐶‘𝑖))) | 
| 3 | 2 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝐴 = 𝐶 → (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖)))) | 
| 4 | 3 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝐴 = 𝐶 → ((𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) | 
| 5 | 4 | ralbidv 3177 | . . . . . . . . . . 11
⊢ (𝐴 = 𝐶 → (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) | 
| 6 | 5 | biimparc 479 | . . . . . . . . . 10
⊢
((∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) ∧ 𝐴 = 𝐶) → ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖)))) | 
| 7 |  | simplr1 1215 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) → 𝐴 ∈ (𝔼‘𝑁)) | 
| 8 |  | simplr2 1216 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) → 𝐵 ∈ (𝔼‘𝑁)) | 
| 9 |  | eqeefv 28919 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐵 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐵‘𝑖))) | 
| 10 | 7, 8, 9 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) → (𝐴 = 𝐵 ↔ ∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐵‘𝑖))) | 
| 11 |  | fveecn 28918 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ) | 
| 12 | 7, 11 | sylan 580 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ) | 
| 13 |  | elicc01 13507 | . . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤
𝑇 ∧ 𝑇 ≤ 1)) | 
| 14 | 13 | simp1bi 1145 | . . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈
ℝ) | 
| 15 | 14 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈
ℂ) | 
| 16 | 15 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → 𝑇 ∈ ℂ) | 
| 17 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ | 
| 18 |  | npcan 11518 | . . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ 𝑇
∈ ℂ) → ((1 − 𝑇) + 𝑇) = 1) | 
| 19 | 17, 18 | mpan 690 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℂ → ((1
− 𝑇) + 𝑇) = 1) | 
| 20 | 19 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ ℂ → (((1
− 𝑇) + 𝑇) · (𝐴‘𝑖)) = (1 · (𝐴‘𝑖))) | 
| 21 |  | mullid 11261 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴‘𝑖) ∈ ℂ → (1 · (𝐴‘𝑖)) = (𝐴‘𝑖)) | 
| 22 | 20, 21 | sylan9eqr 2798 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝑖) ∈ ℂ ∧ 𝑇 ∈ ℂ) → (((1 − 𝑇) + 𝑇) · (𝐴‘𝑖)) = (𝐴‘𝑖)) | 
| 23 |  | subcl 11508 | . . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ 𝑇
∈ ℂ) → (1 − 𝑇) ∈ ℂ) | 
| 24 | 17, 23 | mpan 690 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℂ → (1
− 𝑇) ∈
ℂ) | 
| 25 | 24 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴‘𝑖) ∈ ℂ ∧ 𝑇 ∈ ℂ) → (1 − 𝑇) ∈
ℂ) | 
| 26 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴‘𝑖) ∈ ℂ ∧ 𝑇 ∈ ℂ) → 𝑇 ∈ ℂ) | 
| 27 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴‘𝑖) ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝐴‘𝑖) ∈ ℂ) | 
| 28 | 25, 26, 27 | adddird 11287 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝑖) ∈ ℂ ∧ 𝑇 ∈ ℂ) → (((1 − 𝑇) + 𝑇) · (𝐴‘𝑖)) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖)))) | 
| 29 | 22, 28 | eqtr3d 2778 | . . . . . . . . . . . . . . 15
⊢ (((𝐴‘𝑖) ∈ ℂ ∧ 𝑇 ∈ ℂ) → (𝐴‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖)))) | 
| 30 | 29 | eqeq1d 2738 | . . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑖) ∈ ℂ ∧ 𝑇 ∈ ℂ) → ((𝐴‘𝑖) = (𝐵‘𝑖) ↔ (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))) = (𝐵‘𝑖))) | 
| 31 | 12, 16, 30 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) = (𝐵‘𝑖) ↔ (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))) = (𝐵‘𝑖))) | 
| 32 |  | eqcom 2743 | . . . . . . . . . . . . 13
⊢ ((((1
− 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))) = (𝐵‘𝑖) ↔ (𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖)))) | 
| 33 | 31, 32 | bitrdi 287 | . . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) = (𝐵‘𝑖) ↔ (𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))))) | 
| 34 | 33 | ralbidva 3175 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝐴‘𝑖) = (𝐵‘𝑖) ↔ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))))) | 
| 35 | 10, 34 | bitrd 279 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) → (𝐴 = 𝐵 ↔ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐴‘𝑖))))) | 
| 36 | 6, 35 | imbitrrid 246 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) → ((∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) ∧ 𝐴 = 𝐶) → 𝐴 = 𝐵)) | 
| 37 | 36 | expd 415 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ 𝑇 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) → (𝐴 = 𝐶 → 𝐴 = 𝐵))) | 
| 38 | 37 | impr 454 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (𝐴 = 𝐶 → 𝐴 = 𝐵)) | 
| 39 | 38 | necon3d 2960 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐶)) | 
| 40 | 39 | ex 412 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖)))) → (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐶))) | 
| 41 | 40 | com23 86 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 ≠ 𝐵 → ((𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖)))) → 𝐴 ≠ 𝐶))) | 
| 42 | 41 | exp4a 431 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (𝐴 ≠ 𝐵 → (𝑇 ∈ (0[,]1) → (∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) → 𝐴 ≠ 𝐶)))) | 
| 43 | 42 | 3imp2 1349 | . 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝐵 ∧ 𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → 𝐴 ≠ 𝐶) | 
| 44 |  | simplr1 1215 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝐵 ∧ 𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → 𝐴 ∈ (𝔼‘𝑁)) | 
| 45 |  | simplr3 1217 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝐵 ∧ 𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → 𝐶 ∈ (𝔼‘𝑁)) | 
| 46 |  | eqeelen 28920 | . . . 4
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐴 = 𝐶 ↔ Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2) = 0)) | 
| 47 | 44, 45, 46 | syl2anc 584 | . . 3
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝐵 ∧ 𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (𝐴 = 𝐶 ↔ Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2) = 0)) | 
| 48 | 47 | necon3bid 2984 | . 2
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝐵 ∧ 𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (𝐴 ≠ 𝐶 ↔ Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2) ≠ 0)) | 
| 49 | 43, 48 | mpbid 232 | 1
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) ∧ (𝐴 ≠ 𝐵 ∧ 𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2) ≠ 0) |