Metamath Proof Explorer

Theorem axsegconlem7

Description: Lemma for axsegcon . Show that a particular ratio of distances is in the closed unit interval. (Contributed by Scott Fenton, 18-Sep-2013)

Ref Expression
Hypotheses axsegconlem2.1 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
axsegconlem7.2 ⊢ T = ∑ p = 1 N C ⁡ p − D ⁡ p 2
Assertion axsegconlem7 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → S S + T ∈ 0 1

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
2 axsegconlem7.2 ⊢ T = ∑ p = 1 N C ⁡ p − D ⁡ p 2
3 2 axsegconlem5 ⊢ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → 0 ≤ T
4 3 adantl ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → 0 ≤ T
5 1 axsegconlem4 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → S ∈ ℝ
6 5 3adant3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → S ∈ ℝ
7 2 axsegconlem4 ⊢ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → T ∈ ℝ
8 addge01 ⊢ S ∈ ℝ ∧ T ∈ ℝ → 0 ≤ T ↔ S ≤ S + T
9 6 7 8 syl2an ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → 0 ≤ T ↔ S ≤ S + T
10 4 9 mpbid ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → S ≤ S + T
11 6 adantr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → S ∈ ℝ
12 1 axsegconlem5 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → 0 ≤ S
13 12 3adant3 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → 0 ≤ S
14 13 adantr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → 0 ≤ S
15 readdcl ⊢ S ∈ ℝ ∧ T ∈ ℝ → S + T ∈ ℝ
16 6 7 15 syl2an ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → S + T ∈ ℝ
17 0red ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → 0 ∈ ℝ
18 1 axsegconlem6 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B → 0 < S
19 18 adantr ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → 0 < S
20 17 11 16 19 10 ltletrd ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → 0 < S + T
21 divelunit ⊢ S ∈ ℝ ∧ 0 ≤ S ∧ S + T ∈ ℝ ∧ 0 < S + T → S S + T ∈ 0 1 ↔ S ≤ S + T
22 11 14 16 20 21 syl22anc ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → S S + T ∈ 0 1 ↔ S ≤ S + T
23 10 22 mpbird ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → S S + T ∈ 0 1