elntg2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elntg2		Structured version Visualization version GIF version

Theorem elntg2 29443

Description: The line definition in the Tarski structure for the Euclidean geometry. In contrast to elntg 29442, the betweenness can be strengthened by excluding 1 resp. 0 from the related intervals (because of 𝑥 ≠ 𝑦). (Contributed by AV, 14-Feb-2023.)

**Hypotheses**
Ref	Expression
elntg2.1	⊢ 𝑃 = (Base‘(EEG‘𝑁))
elntg2.2	⊢ 𝐼 = (1...𝑁)

**Assertion**
Ref	Expression
elntg2	⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑝 ∈ 𝑃 ∣ (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))}))

Distinct variable groups: 𝑖,𝐼 𝑖,𝑁,𝑘,𝑙,𝑚,𝑝,𝑥,𝑦 𝑃,𝑖,𝑝 Allowed substitution hints: 𝑃(𝑥, 𝑦, 𝑘, 𝑚, 𝑙) 𝐼(𝑥, 𝑦, 𝑘, 𝑚, 𝑝, 𝑙)

**Proof of Theorem elntg2**
Step	Hyp	Ref	Expression
1		elntg2.1	. . 3 ⊢ 𝑃 = (Base‘(EEG‘𝑁))
2		eqid 2762	. . 3 ⊢ (Itv‘(EEG‘𝑁)) = (Itv‘(EEG‘𝑁))
3	1, 2	elntg 29442	. 2 ⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑝 ∈ 𝑃 ∣ (𝑝 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑥 ∈ (𝑝(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑝))}))
4		simpl1 1210	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑁 ∈ ℕ)
5		simpl2 1211	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑥 ∈ 𝑃)
6		eldifi 4081	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑃 ∖ {𝑥}) → 𝑦 ∈ 𝑃)
7	6	3ad2ant3 1153	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → 𝑦 ∈ 𝑃)
8	7	adantr 486	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑦 ∈ 𝑃)
9		simpr 490	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ 𝑃)
10	4, 1, 2, 5, 8, 9	ebtwntg 29440	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑝 Btwn ⟨𝑥, 𝑦⟩ ↔ 𝑝 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦)))
11		eengbas 29439	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝔼‘𝑁) = (Base‘(EEG‘𝑁)))
12	1, 11	eqtr4id 2816	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑃 = (𝔼‘𝑁))
13	12	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → 𝑃 = (𝔼‘𝑁))
14	13	eleq2d 2848	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → (𝑝 ∈ 𝑃 ↔ 𝑝 ∈ (𝔼‘𝑁)))
15	14	biimpa 482	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑝 ∈ (𝔼‘𝑁))
16	12	eleq2d 2848	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃 ↔ 𝑥 ∈ (𝔼‘𝑁)))
17	16	biimpa 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃) → 𝑥 ∈ (𝔼‘𝑁))
18	17	3adant3 1150	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → 𝑥 ∈ (𝔼‘𝑁))
19	18	adantr 486	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑥 ∈ (𝔼‘𝑁))
20	12	eleq2d 2848	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑦 ∈ 𝑃 ↔ 𝑦 ∈ (𝔼‘𝑁)))
21	20	biimpcd 252	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑃 → (𝑁 ∈ ℕ → 𝑦 ∈ (𝔼‘𝑁)))
22	21, 6	syl11 34	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑦 ∈ (𝑃 ∖ {𝑥}) → 𝑦 ∈ (𝔼‘𝑁)))
23	22	a1d 26	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃 → (𝑦 ∈ (𝑃 ∖ {𝑥}) → 𝑦 ∈ (𝔼‘𝑁))))
24	23	3imp 1128	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → 𝑦 ∈ (𝔼‘𝑁))
25	24	adantr 486	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑦 ∈ (𝔼‘𝑁))
26		brbtwn 29357	. . . . . . . 8 ⊢ ((𝑝 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑝 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖)))))
27	15, 19, 25, 26	syl3anc 1398	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑝 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖)))))
28		elntg2.2	. . . . . . . . 9 ⊢ 𝐼 = (1...𝑁)
29	28	raleqi 3319	. . . . . . . 8 ⊢ (∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))))
30	29	rexbii 3111	. . . . . . 7 ⊢ (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ↔ ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))))
31	27, 30	bitr4di 292	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑝 Btwn ⟨𝑥, 𝑦⟩ ↔ ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖)))))
32	10, 31	bitr3d 284	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑝 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ↔ ∃𝑘 ∈ (0[,]1)∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖)))))
33	4, 1, 2, 9, 8, 5	ebtwntg 29440	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑥 Btwn ⟨𝑝, 𝑦⟩ ↔ 𝑥 ∈ (𝑝(Itv‘(EEG‘𝑁))𝑦)))
34		brbtwn 29357	. . . . . . . 8 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝑝, 𝑦⟩ ↔ ∃𝑙 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
35	19, 15, 25, 34	syl3anc 1398	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑥 Btwn ⟨𝑝, 𝑦⟩ ↔ ∃𝑙 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
36	33, 35	bitr3d 284	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑥 ∈ (𝑝(Itv‘(EEG‘𝑁))𝑦) ↔ ∃𝑙 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
37		0xr 11283	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
38		1xr 11295	. . . . . . . . . 10 ⊢ 1 ∈ ℝ^*
39		0le1 11764	. . . . . . . . . 10 ⊢ 0 ≤ 1
40		snunico 13534	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 0 ≤ 1) → ((0[,)1) ∪ {1}) = (0[,]1))
41	37, 38, 39, 40	mp3an 1490	. . . . . . . . 9 ⊢ ((0[,)1) ∪ {1}) = (0[,]1)
42	41	eqcomi 2771	. . . . . . . 8 ⊢ (0[,]1) = ((0[,)1) ∪ {1})
43	42	a1i 11	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (0[,]1) = ((0[,)1) ∪ {1}))
44	43	rexeqdv 3322	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (∃𝑙 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∃𝑙 ∈ ((0[,)1) ∪ {1})∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
45		rexun 4145	. . . . . . 7 ⊢ (∃𝑙 ∈ ((0[,)1) ∪ {1})∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
46		eldifsn 4751	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑃 ∖ {𝑥}) ↔ (𝑦 ∈ 𝑃 ∧ 𝑦 ≠ 𝑥))
47		elee 29351	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (𝔼‘𝑁) ↔ 𝑥:(1...𝑁)⟶ℝ))
48		ffn 6706	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥:(1...𝑁)⟶ℝ → 𝑥 Fn (1...𝑁))
49	47, 48	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ (𝔼‘𝑁) → 𝑥 Fn (1...𝑁)))
50	16, 49	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃 → 𝑥 Fn (1...𝑁)))
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝑃 → (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃 → 𝑥 Fn (1...𝑁))))
52	51	3imp 1128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃) → 𝑥 Fn (1...𝑁))
53		elee 29351	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → (𝑦 ∈ (𝔼‘𝑁) ↔ 𝑦:(1...𝑁)⟶ℝ))
54		ffn 6706	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦:(1...𝑁)⟶ℝ → 𝑦 Fn (1...𝑁))
55	53, 54	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → (𝑦 ∈ (𝔼‘𝑁) → 𝑦 Fn (1...𝑁)))
56	20, 55	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ → (𝑦 ∈ 𝑃 → 𝑦 Fn (1...𝑁)))
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝑃 → (𝑁 ∈ ℕ → (𝑦 ∈ 𝑃 → 𝑦 Fn (1...𝑁))))
58	57	3imp31 1129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃) → 𝑦 Fn (1...𝑁))
59		eqfnfv 7026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 Fn (1...𝑁) ∧ 𝑦 Fn (1...𝑁)) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
60	52, 58, 59	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃) → (𝑥 = 𝑦 ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
61	60	biimprd 251	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖) → 𝑥 = 𝑦))
62		eqcom 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
63	61, 62	imbitrrdi 255	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖) → 𝑦 = 𝑥))
64	63	necon3ad 2970	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃) → (𝑦 ≠ 𝑥 → ¬ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
65	64	3exp 1137	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑃 → (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃 → (𝑦 ≠ 𝑥 → ¬ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))))
66	65	com24 96	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑃 → (𝑦 ≠ 𝑥 → (𝑥 ∈ 𝑃 → (𝑁 ∈ ℕ → ¬ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))))
67	66	imp 412	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝑃 ∧ 𝑦 ≠ 𝑥) → (𝑥 ∈ 𝑃 → (𝑁 ∈ ℕ → ¬ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))))
68	46, 67	sylbi 220	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑃 ∖ {𝑥}) → (𝑥 ∈ 𝑃 → (𝑁 ∈ ℕ → ¬ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))))
69	68	3imp31 1129	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
70	69	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖))
71	12	eleq2d 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ → (𝑝 ∈ 𝑃 ↔ 𝑝 ∈ (𝔼‘𝑁)))
72		elee 29351	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ → (𝑝 ∈ (𝔼‘𝑁) ↔ 𝑝:(1...𝑁)⟶ℝ))
73	72	biimpd 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ → (𝑝 ∈ (𝔼‘𝑁) → 𝑝:(1...𝑁)⟶ℝ))
74	71, 73	sylbid 243	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ → (𝑝 ∈ 𝑃 → 𝑝:(1...𝑁)⟶ℝ))
75	74	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → (𝑝 ∈ 𝑃 → 𝑝:(1...𝑁)⟶ℝ))
76	75	imp 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑝:(1...𝑁)⟶ℝ)
77	76	ffvelcdmda 7080	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℝ)
78	77	recnd 11264	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (𝑝‘𝑖) ∈ ℂ)
79	78	mul02d 11435	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (0 · (𝑝‘𝑖)) = 0)
80	21, 53	mpbidi 244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝑃 → (𝑁 ∈ ℕ → 𝑦:(1...𝑁)⟶ℝ))
81	80, 6	syl11 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ → (𝑦 ∈ (𝑃 ∖ {𝑥}) → 𝑦:(1...𝑁)⟶ℝ))
82	81	a1d 26	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃 → (𝑦 ∈ (𝑃 ∖ {𝑥}) → 𝑦:(1...𝑁)⟶ℝ)))
83	82	3imp 1128	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → 𝑦:(1...𝑁)⟶ℝ)
84	83	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑦:(1...𝑁)⟶ℝ)
85	84	ffvelcdmda 7080	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℝ)
86	85	recnd 11264	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) ∈ ℂ)
87	86	mullidd 11254	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (1 · (𝑦‘𝑖)) = (𝑦‘𝑖))
88	79, 87	oveq12d 7434	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖))) = (0 + (𝑦‘𝑖)))
89	86	addlidd 11438	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (0 + (𝑦‘𝑖)) = (𝑦‘𝑖))
90	88, 89	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖))) = (𝑦‘𝑖))
91	90	eqeq2d 2773	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖))) ↔ (𝑥‘𝑖) = (𝑦‘𝑖)))
92	91	ralbidva 3185	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖)))
93	70, 92	mtbird 328	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖))))
94		1re 11235	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
95		oveq2 7424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 1 → (1 − 𝑙) = (1 − 1))
96	95	oveq1d 7431	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 1 → ((1 − 𝑙) · (𝑝‘𝑖)) = ((1 − 1) · (𝑝‘𝑖)))
97		1m1e0 12340	. . . . . . . . . . . . . . . . 17 ⊢ (1 − 1) = 0
98	97	oveq1i 7426	. . . . . . . . . . . . . . . 16 ⊢ ((1 − 1) · (𝑝‘𝑖)) = (0 · (𝑝‘𝑖))
99	96, 98	eqtrdi 2813	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 1 → ((1 − 𝑙) · (𝑝‘𝑖)) = (0 · (𝑝‘𝑖)))
100		oveq1 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 1 → (𝑙 · (𝑦‘𝑖)) = (1 · (𝑦‘𝑖)))
101	99, 100	oveq12d 7434	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 1 → (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) = ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖))))
102	101	eqeq2d 2773	. . . . . . . . . . . . 13 ⊢ (𝑙 = 1 → ((𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (𝑥‘𝑖) = ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖)))))
103	102	ralbidv 3187	. . . . . . . . . . . 12 ⊢ (𝑙 = 1 → (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖)))))
104	103	rexsng 4640	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ → (∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖)))))
105	94, 104	ax-mp 5	. . . . . . . . . 10 ⊢ (∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = ((0 · (𝑝‘𝑖)) + (1 · (𝑦‘𝑖))))
106	93, 105	sylnibr 332	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → ¬ ∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))
107	28	raleqi 3319	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))
108	107	rexbii 3111	. . . . . . . . . 10 ⊢ (∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))
109		biorf 950	. . . . . . . . . 10 ⊢ (¬ ∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) → (∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))))
110	108, 109	bitrid 286	. . . . . . . . 9 ⊢ (¬ ∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) → (∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))))
111	106, 110	syl 18	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ (∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))))))
112		orcom 884	. . . . . . . 8 ⊢ ((∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))) ↔ (∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
113	111, 112	bitr2di 291	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → ((∃𝑙 ∈ (0[,)1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ {1}∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))) ↔ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
114	45, 113	bitrid 286	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (∃𝑙 ∈ ((0[,)1) ∪ {1})∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ↔ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
115	36, 44, 114	3bitrd 308	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑥 ∈ (𝑝(Itv‘(EEG‘𝑁))𝑦) ↔ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖)))))
116	4, 1, 2, 5, 9, 8	ebtwntg 29440	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑦 Btwn ⟨𝑥, 𝑝⟩ ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑝)))
117		brbtwn 29357	. . . . . . . 8 ⊢ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑝 ∈ (𝔼‘𝑁)) → (𝑦 Btwn ⟨𝑥, 𝑝⟩ ↔ ∃𝑚 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
118	25, 19, 15, 117	syl3anc 1398	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑦 Btwn ⟨𝑥, 𝑝⟩ ↔ ∃𝑚 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
119	116, 118	bitr3d 284	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑝) ↔ ∃𝑚 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
120		snunioc 13535	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 0 ≤ 1) → ({0} ∪ (0(,]1)) = (0[,]1))
121	37, 38, 39, 120	mp3an 1490	. . . . . . . . 9 ⊢ ({0} ∪ (0(,]1)) = (0[,]1)
122	121	eqcomi 2771	. . . . . . . 8 ⊢ (0[,]1) = ({0} ∪ (0(,]1))
123	122	a1i 11	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (0[,]1) = ({0} ∪ (0(,]1)))
124	123	rexeqdv 3322	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (∃𝑚 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∃𝑚 ∈ ({0} ∪ (0(,]1))∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
125		rexun 4145	. . . . . . 7 ⊢ (∃𝑚 ∈ ({0} ∪ (0(,]1))∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
126		eqcom 2769	. . . . . . . . . . . 12 ⊢ ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑦‘𝑖) = (𝑥‘𝑖))
127	126	ralbii 3110	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (𝑦‘𝑖) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (𝑥‘𝑖))
128	70, 127	sylnib 331	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (𝑥‘𝑖))
129	16	biimpd 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃 → 𝑥 ∈ (𝔼‘𝑁)))
130	129, 47	sylibd 242	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃 → 𝑥:(1...𝑁)⟶ℝ))
131	130	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃) → 𝑥:(1...𝑁)⟶ℝ)
132	131	3adant3 1150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → 𝑥:(1...𝑁)⟶ℝ)
133	132	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → 𝑥:(1...𝑁)⟶ℝ)
134	133	ffvelcdmda 7080	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℝ)
135	134	recnd 11264	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) ∈ ℂ)
136	135	mullidd 11254	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → (1 · (𝑥‘𝑖)) = (𝑥‘𝑖))
137	136, 79	oveq12d 7434	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖))) = ((𝑥‘𝑖) + 0))
138	135	addridd 11437	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) + 0) = (𝑥‘𝑖))
139	137, 138	eqtrd 2797	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖))) = (𝑥‘𝑖))
140	139	eqeq2d 2773	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑦‘𝑖) = ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖))) ↔ (𝑦‘𝑖) = (𝑥‘𝑖)))
141	140	ralbidva 3185	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (𝑥‘𝑖)))
142	128, 141	mtbird 328	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → ¬ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖))))
143		0re 11237	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
144		oveq2 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 0 → (1 − 𝑚) = (1 − 0))
145	144	oveq1d 7431	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 0 → ((1 − 𝑚) · (𝑥‘𝑖)) = ((1 − 0) · (𝑥‘𝑖)))
146		1m0e1 12387	. . . . . . . . . . . . . . . 16 ⊢ (1 − 0) = 1
147	146	oveq1i 7426	. . . . . . . . . . . . . . 15 ⊢ ((1 − 0) · (𝑥‘𝑖)) = (1 · (𝑥‘𝑖))
148	145, 147	eqtrdi 2813	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 0 → ((1 − 𝑚) · (𝑥‘𝑖)) = (1 · (𝑥‘𝑖)))
149		oveq1 7423	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 0 → (𝑚 · (𝑝‘𝑖)) = (0 · (𝑝‘𝑖)))
150	148, 149	oveq12d 7434	. . . . . . . . . . . . 13 ⊢ (𝑚 = 0 → (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) = ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖))))
151	150	eqeq2d 2773	. . . . . . . . . . . 12 ⊢ (𝑚 = 0 → ((𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (𝑦‘𝑖) = ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖)))))
152	151	ralbidv 3187	. . . . . . . . . . 11 ⊢ (𝑚 = 0 → (∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖)))))
153	152	rexsng 4640	. . . . . . . . . 10 ⊢ (0 ∈ ℝ → (∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖)))))
154	143, 153	ax-mp 5	. . . . . . . . 9 ⊢ (∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = ((1 · (𝑥‘𝑖)) + (0 · (𝑝‘𝑖))))
155	142, 154	sylnibr 332	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → ¬ ∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))
156	28	raleqi 3319	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))
157	156	rexbii 3111	. . . . . . . . 9 ⊢ (∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))
158		biorf 950	. . . . . . . . 9 ⊢ (¬ ∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) → (∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
159	157, 158	bitrid 286	. . . . . . . 8 ⊢ (¬ ∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) → (∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
160	155, 159	syl 18	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ (∃𝑚 ∈ {0}∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
161	125, 160	bitr4id 293	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (∃𝑚 ∈ ({0} ∪ (0(,]1))∀𝑖 ∈ (1...𝑁)(𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))) ↔ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
162	119, 124, 161	3bitrd 308	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑝) ↔ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖)))))
163	32, 115, 162	3orbi123d 1463	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) ∧ 𝑝 ∈ 𝑃) → ((𝑝 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑥 ∈ (𝑝(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑝)) ↔ (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))))
164	163	rabbidva 3420	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ (𝑃 ∖ {𝑥})) → {𝑝 ∈ 𝑃 ∣ (𝑝 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑥 ∈ (𝑝(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑝))} = {𝑝 ∈ 𝑃 ∣ (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))})
165	164	mpoeq3dva 7493	. 2 ⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑝 ∈ 𝑃 ∣ (𝑝 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑥 ∈ (𝑝(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑝))}) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑝 ∈ 𝑃 ∣ (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))}))
166	3, 165	eqtrd 2797	1 ⊢ (𝑁 ∈ ℕ → (LineG‘(EEG‘𝑁)) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑝 ∈ 𝑃 ∣ (∃𝑘 ∈ (0[,]1)∀𝑖 ∈ 𝐼 (𝑝‘𝑖) = (((1 − 𝑘) · (𝑥‘𝑖)) + (𝑘 · (𝑦‘𝑖))) ∨ ∃𝑙 ∈ (0[,)1)∀𝑖 ∈ 𝐼 (𝑥‘𝑖) = (((1 − 𝑙) · (𝑝‘𝑖)) + (𝑙 · (𝑦‘𝑖))) ∨ ∃𝑚 ∈ (0(,]1)∀𝑖 ∈ 𝐼 (𝑦‘𝑖) = (((1 − 𝑚) · (𝑥‘𝑖)) + (𝑚 · (𝑝‘𝑖))))}))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 {crab 3414 ∖ cdif 3899 ∪ cun 3900 {csn 4587 ⟨cop 4593 class class class wbr 5107 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 ∈ cmpo 7418 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 ℝ^*cxr 11269 ≤ cle 11271 − cmin 11468 ℕcn 12260 (,]cioc 13401 [,)cico 13402 [,]cicc 13403 ...cfz 13563 Basecbs 17305 Itvcitv 28775 LineGclng 28776 𝔼cee 29345 Btwn cbtwn 29346 EEGceeng 29435

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-er 8699 df-map 8831 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-ioc 13405 df-ico 13406 df-icc 13407 df-fz 13564 df-seq 14068 df-sum 15776 df-struct 17243 df-slot 17278 df-ndx 17290 df-base 17306 df-ds 17368 df-itv 28777 df-lng 28778 df-ee 29348 df-btwn 29349 df-eeng 29436

This theorem is used by: eenglngeehlnm 49671

W3C validator