Metamath Proof Explorer

Theorem seglelin

Description: Linearity law for segment comparison. Theorem 5.10 of Schwabhauser p. 42. (Contributed by Scott Fenton, 14-Oct-2013)

Ref Expression
Assertion seglelin ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) )

Proof

Step Hyp Ref Expression
1 segcon2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
2 andir ⊢ ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
3 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
4 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
6 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) )
7 cgrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) )
8 3 4 5 6 7 syl121anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) )
9 8 anbi2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ↔ ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) )
10 9 orbi2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
11 2 10 syl5bb ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ↔ ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
12 11 rexbidva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
13 brsegle2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) )
14 brsegle ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) )
15 14 3com23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) )
16 13 15 orbi12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
17 r19.43 ⊢ ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) ↔ ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) )
18 16 17 bitr4di ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∨ ( 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝑥 ⟩ ) ) ) )
19 12 18 bitr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
20 1 19 mpbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg≤ ⟨ 𝐶 , 𝐷 ⟩ ∨ ⟨ 𝐶 , 𝐷 ⟩ Seg≤ ⟨ 𝐴 , 𝐵 ⟩ ) )