Metamath Proof Explorer

Theorem axbtwnid

Description: Points are indivisible. That is, if A lies between B and B , then A = B . Axiom A6 of Schwabhauser p. 11. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axbtwnid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn B B → A = B

Proof

Step Hyp Ref Expression
1 simp2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
2 simp3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
3 brbtwn ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn B B ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i
4 1 2 2 3 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn B B ↔ ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i
5 elicc01 ⊢ t ∈ 0 1 ↔ t ∈ ℝ ∧ 0 ≤ t ∧ t ≤ 1
6 5 simp1bi ⊢ t ∈ 0 1 → t ∈ ℝ
7 6 recnd ⊢ t ∈ 0 1 → t ∈ ℂ
8 eqeefv ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
9 8 3adant1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
10 9 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
11 ax-1cn ⊢ 1 ∈ ℂ
12 npcan ⊢ 1 ∈ ℂ ∧ t ∈ ℂ → 1 - t + t = 1
13 11 12 mpan ⊢ t ∈ ℂ → 1 - t + t = 1
14 13 ad2antlr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → 1 - t + t = 1
15 14 oveq1d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → 1 - t + t ⁢ B ⁡ i = 1 ⁢ B ⁡ i
16 subcl ⊢ 1 ∈ ℂ ∧ t ∈ ℂ → 1 − t ∈ ℂ
17 11 16 mpan ⊢ t ∈ ℂ → 1 − t ∈ ℂ
18 17 ad2antlr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → 1 − t ∈ ℂ
19 simplr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → t ∈ ℂ
20 simpll3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → B ∈ 𝔼 ⁡ N
21 fveecn ⊢ B ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → B ⁡ i ∈ ℂ
22 20 21 sylancom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → B ⁡ i ∈ ℂ
23 18 19 22 adddird ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → 1 - t + t ⁢ B ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i
24 22 mulid2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → 1 ⁢ B ⁡ i = B ⁡ i
25 15 23 24 3eqtr3rd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → B ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i
26 25 eqeq2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ ∧ i ∈ 1 … N → A ⁡ i = B ⁡ i ↔ A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i
27 26 ralbidva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ → ∀ i ∈ 1 … N A ⁡ i = B ⁡ i ↔ ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i
28 10 27 bitrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i
29 28 biimprd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ ℂ → ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i → A = B
30 7 29 sylan2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ t ∈ 0 1 → ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i → A = B
31 30 rexlimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ t ∈ 0 1 ∀ i ∈ 1 … N A ⁡ i = 1 − t ⁢ B ⁡ i + t ⁢ B ⁡ i → A = B
32 4 31 sylbid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn B B → A = B