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 ⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
axsegconlem7.2 ⊢ 𝑇 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 )
Assertion axsegconlem7 ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ∈ ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
2 axsegconlem7.2 ⊢ 𝑇 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 )
3 2 axsegconlem5 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → 0 ≤ ( √ ‘ 𝑇 ) )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 ≤ ( √ ‘ 𝑇 ) )
5 1 axsegconlem4 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
6 5 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( √ ‘ 𝑆 ) ∈ ℝ )
7 2 axsegconlem4 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℝ )
8 addge01 ⊢ ( ( ( √ ‘ 𝑆 ) ∈ ℝ ∧ ( √ ‘ 𝑇 ) ∈ ℝ ) → ( 0 ≤ ( √ ‘ 𝑇 ) ↔ ( √ ‘ 𝑆 ) ≤ ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) )
9 6 7 8 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 0 ≤ ( √ ‘ 𝑇 ) ↔ ( √ ‘ 𝑆 ) ≤ ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) )
10 4 9 mpbid ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( √ ‘ 𝑆 ) ≤ ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) )
11 6 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
12 1 axsegconlem5 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 0 ≤ ( √ ‘ 𝑆 ) )
13 12 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 0 ≤ ( √ ‘ 𝑆 ) )
14 13 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 ≤ ( √ ‘ 𝑆 ) )
15 readdcl ⊢ ( ( ( √ ‘ 𝑆 ) ∈ ℝ ∧ ( √ ‘ 𝑇 ) ∈ ℝ ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
16 6 7 15 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
17 0red ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 ∈ ℝ )
18 1 axsegconlem6 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 0 < ( √ ‘ 𝑆 ) )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 < ( √ ‘ 𝑆 ) )
20 17 11 16 19 10 ltletrd ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 < ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) )
21 divelunit ⊢ ( ( ( ( √ ‘ 𝑆 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑆 ) ) ∧ ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ ∧ 0 < ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) → ( ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ∈ ( 0 [,] 1 ) ↔ ( √ ‘ 𝑆 ) ≤ ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) )
22 11 14 16 20 21 syl22anc ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ∈ ( 0 [,] 1 ) ↔ ( √ ‘ 𝑆 ) ≤ ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) )
23 10 22 mpbird ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ∈ ( 0 [,] 1 ) )