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 ) )