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