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→ABtwnBB→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→ABtwnBB↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢B⁡i
4 1 2 2 3 syl3anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnBB↔∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢B⁡i
5 elicc01 ⊢t∈01↔t∈ℝ∧0≤t∧t≤1
6 5 simp1bi ⊢t∈01→t∈ℝ
7 6 recnd ⊢t∈01→t∈ℂ
8 eqeefv ⊢A∈𝔼⁡N∧B∈𝔼⁡N→A=B↔∀i∈1…NA⁡i=B⁡i
9 8 3adant1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→A=B↔∀i∈1…NA⁡i=B⁡i
10 9 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧t∈ℂ→A=B↔∀i∈1…NA⁡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 mullidd ⊢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…NA⁡i=B⁡i↔∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢B⁡i
28 10 27 bitrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧t∈ℂ→A=B↔∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢B⁡i
29 28 biimprd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧t∈ℂ→∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢B⁡i→A=B
30 7 29 sylan2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧t∈01→∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢B⁡i→A=B
31 30 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→∃t∈01∀i∈1…NA⁡i=1−t⁢B⁡i+t⁢B⁡i→A=B
32 4 31 sylbid ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→ABtwnBB→A=B