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 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐵 ⟩ → 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
2 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
3 brbtwn ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐵 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
4 1 2 2 3 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐵 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
5 elicc01 ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1 ) )
6 5 simp1bi ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ∈ ℝ )
7 6 recnd ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ∈ ℂ )
8 eqeefv ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )
9 8 3adant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )
10 9 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) )
11 ax-1cn ⊢ 1 ∈ ℂ
12 npcan ⊢ ( ( 1 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( ( 1 − 𝑡 ) + 𝑡 ) = 1 )
13 11 12 mpan ⊢ ( 𝑡 ∈ ℂ → ( ( 1 − 𝑡 ) + 𝑡 ) = 1 )
14 13 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑡 ) + 𝑡 ) = 1 )
15 14 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑡 ) + 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) = ( 1 · ( 𝐵 ‘ 𝑖 ) ) )
16 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( 1 − 𝑡 ) ∈ ℂ )
17 11 16 mpan ⊢ ( 𝑡 ∈ ℂ → ( 1 − 𝑡 ) ∈ ℂ )
18 17 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑡 ) ∈ ℂ )
19 simplr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℂ )
20 simpll3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
21 fveecn ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
22 20 21 sylancom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
23 18 19 22 adddird ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑡 ) + 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) )
24 22 mulid2d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 · ( 𝐵 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) )
25 15 23 24 3eqtr3rd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) )
26 25 eqeq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ↔ ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
27 26 ralbidva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
28 10 27 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
29 28 biimprd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ℂ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) → 𝐴 = 𝐵 ) )
30 7 29 sylan2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) → 𝐴 = 𝐵 ) )
31 30 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐴 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐵 ‘ 𝑖 ) ) ) → 𝐴 = 𝐵 ) )
32 4 31 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐴 Btwn ⟨ 𝐵 , 𝐵 ⟩ → 𝐴 = 𝐵 ) )