Theorem axsegconlem8

Description: Lemma for axsegcon . Show that a particular mapping generates a point. (Contributed by Scott Fenton, 18-Sep-2013)

	Ref	Expression
Hypotheses	axsegconlem2.1	⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
	axsegconlem7.2	⊢ 𝑇 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 )
	axsegconlem8.3	⊢ 𝐹 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) )
Assertion	axsegconlem8	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		axsegconlem2.1	⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
2		axsegconlem7.2	⊢ 𝑇 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 )
3		axsegconlem8.3	⊢ 𝐹 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) )
4	1	axsegconlem4	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
5	4	3adant3	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( √ ‘ 𝑆 ) ∈ ℝ )
6	5	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
7	2	axsegconlem4	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℝ )
8	7	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℝ )
9	6 8	readdcld	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
10		simpl2	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
11		fveere	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
12	10 11	sylan	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
13	9 12	remulcld	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) ∈ ℝ )
14		simpl1	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
15		fveere	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
16	14 15	sylan	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
17	8 16	remulcld	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
18	13 17	resubcld	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) ∈ ℝ )
19	1	axsegconlem6	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 0 < ( √ ‘ 𝑆 ) )
20	19	gt0ne0d	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( √ ‘ 𝑆 ) ≠ 0 )
21	20	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑆 ) ≠ 0 )
22	18 6 21	redivcld	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) ∈ ℝ )
23	22	ralrimiva	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) ∈ ℝ )
24		eleenn	⊢ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
25	24	ad2antll	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
26		mptelee	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) ∈ ℝ ) )
27	25 26	syl	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) ∈ ℝ ) )
28	23 27	mpbird	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
29	3 28	eqeltrid	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )