| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elntg2.1 |
⊢ 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) ) |
| 2 |
|
elntg2.2 |
⊢ 𝐼 = ( 1 ... 𝑁 ) |
| 3 |
|
eqid |
⊢ ( Itv ‘ ( EEG ‘ 𝑁 ) ) = ( Itv ‘ ( EEG ‘ 𝑁 ) ) |
| 4 |
1 3
|
elntg |
⊢ ( 𝑁 ∈ ℕ → ( LineG ‘ ( EEG ‘ 𝑁 ) ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑝 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑝 ) ) } ) ) |
| 5 |
|
simpl1 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑁 ∈ ℕ ) |
| 6 |
|
simpl2 |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑥 ∈ 𝑃 ) |
| 7 |
|
eldifi |
⊢ ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → 𝑦 ∈ 𝑃 ) |
| 8 |
7
|
3ad2ant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑦 ∈ 𝑃 ) |
| 9 |
8
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑦 ∈ 𝑃 ) |
| 10 |
|
simpr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 ) |
| 11 |
5 1 3 6 9 10
|
ebtwntg |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑝 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ) ) |
| 12 |
|
eengbas |
⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) ) |
| 13 |
1 12
|
eqtr4id |
⊢ ( 𝑁 ∈ ℕ → 𝑃 = ( 𝔼 ‘ 𝑁 ) ) |
| 14 |
13
|
3ad2ant1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑃 = ( 𝔼 ‘ 𝑁 ) ) |
| 15 |
14
|
eleq2d |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
| 16 |
15
|
biimpa |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) |
| 17 |
13
|
eleq2d |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 ↔ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
| 18 |
17
|
biimpa |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) |
| 19 |
18
|
3adant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) |
| 20 |
19
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) |
| 21 |
13
|
eleq2d |
⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ 𝑃 ↔ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
| 22 |
21
|
biimpcd |
⊢ ( 𝑦 ∈ 𝑃 → ( 𝑁 ∈ ℕ → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
| 23 |
22 7
|
syl11 |
⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
| 24 |
23
|
a1d |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 → ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) |
| 25 |
24
|
3imp |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) |
| 26 |
25
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) |
| 27 |
|
brbtwn |
⊢ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑝 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 28 |
16 20 26 27
|
syl3anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 29 |
2
|
raleqi |
⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 30 |
29
|
rexbii |
⊢ ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 31 |
28 30
|
bitr4di |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 32 |
11 31
|
bitr3d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑝 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ↔ ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 33 |
5 1 3 10 9 6
|
ebtwntg |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑥 Btwn ⟨ 𝑝 , 𝑦 ⟩ ↔ 𝑥 ∈ ( 𝑝 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ) ) |
| 34 |
|
brbtwn |
⊢ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝑝 , 𝑦 ⟩ ↔ ∃ 𝑙 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 35 |
20 16 26 34
|
syl3anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑥 Btwn ⟨ 𝑝 , 𝑦 ⟩ ↔ ∃ 𝑙 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 36 |
33 35
|
bitr3d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑥 ∈ ( 𝑝 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ↔ ∃ 𝑙 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 37 |
|
0xr |
⊢ 0 ∈ ℝ* |
| 38 |
|
1xr |
⊢ 1 ∈ ℝ* |
| 39 |
|
0le1 |
⊢ 0 ≤ 1 |
| 40 |
|
snunico |
⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1 ) → ( ( 0 [,) 1 ) ∪ { 1 } ) = ( 0 [,] 1 ) ) |
| 41 |
37 38 39 40
|
mp3an |
⊢ ( ( 0 [,) 1 ) ∪ { 1 } ) = ( 0 [,] 1 ) |
| 42 |
41
|
eqcomi |
⊢ ( 0 [,] 1 ) = ( ( 0 [,) 1 ) ∪ { 1 } ) |
| 43 |
42
|
a1i |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 [,] 1 ) = ( ( 0 [,) 1 ) ∪ { 1 } ) ) |
| 44 |
43
|
rexeqdv |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑙 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∃ 𝑙 ∈ ( ( 0 [,) 1 ) ∪ { 1 } ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 45 |
|
rexun |
⊢ ( ∃ 𝑙 ∈ ( ( 0 [,) 1 ) ∪ { 1 } ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 46 |
|
eldifsn |
⊢ ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↔ ( 𝑦 ∈ 𝑃 ∧ 𝑦 ≠ 𝑥 ) ) |
| 47 |
|
elee |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 48 |
|
ffn |
⊢ ( 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ → 𝑥 Fn ( 1 ... 𝑁 ) ) |
| 49 |
47 48
|
biimtrdi |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑥 Fn ( 1 ... 𝑁 ) ) ) |
| 50 |
17 49
|
sylbid |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 → 𝑥 Fn ( 1 ... 𝑁 ) ) ) |
| 51 |
50
|
a1i |
⊢ ( 𝑦 ∈ 𝑃 → ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 → 𝑥 Fn ( 1 ... 𝑁 ) ) ) ) |
| 52 |
51
|
3imp |
⊢ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ) → 𝑥 Fn ( 1 ... 𝑁 ) ) |
| 53 |
|
elee |
⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 54 |
|
ffn |
⊢ ( 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ → 𝑦 Fn ( 1 ... 𝑁 ) ) |
| 55 |
53 54
|
biimtrdi |
⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑦 Fn ( 1 ... 𝑁 ) ) ) |
| 56 |
21 55
|
sylbid |
⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ 𝑃 → 𝑦 Fn ( 1 ... 𝑁 ) ) ) |
| 57 |
56
|
a1i |
⊢ ( 𝑥 ∈ 𝑃 → ( 𝑁 ∈ ℕ → ( 𝑦 ∈ 𝑃 → 𝑦 Fn ( 1 ... 𝑁 ) ) ) ) |
| 58 |
57
|
3imp31 |
⊢ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ) → 𝑦 Fn ( 1 ... 𝑁 ) ) |
| 59 |
|
eqfnfv |
⊢ ( ( 𝑥 Fn ( 1 ... 𝑁 ) ∧ 𝑦 Fn ( 1 ... 𝑁 ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) |
| 60 |
52 58 59
|
syl2anc |
⊢ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) |
| 61 |
60
|
biimprd |
⊢ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) → 𝑥 = 𝑦 ) ) |
| 62 |
|
eqcom |
⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 ) |
| 63 |
61 62
|
imbitrrdi |
⊢ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) → 𝑦 = 𝑥 ) ) |
| 64 |
63
|
necon3ad |
⊢ ( ( 𝑦 ∈ 𝑃 ∧ 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ) → ( 𝑦 ≠ 𝑥 → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) |
| 65 |
64
|
3exp |
⊢ ( 𝑦 ∈ 𝑃 → ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 → ( 𝑦 ≠ 𝑥 → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 66 |
65
|
com24 |
⊢ ( 𝑦 ∈ 𝑃 → ( 𝑦 ≠ 𝑥 → ( 𝑥 ∈ 𝑃 → ( 𝑁 ∈ ℕ → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 67 |
66
|
imp |
⊢ ( ( 𝑦 ∈ 𝑃 ∧ 𝑦 ≠ 𝑥 ) → ( 𝑥 ∈ 𝑃 → ( 𝑁 ∈ ℕ → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 68 |
46 67
|
sylbi |
⊢ ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → ( 𝑥 ∈ 𝑃 → ( 𝑁 ∈ ℕ → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 69 |
68
|
3imp31 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) |
| 70 |
69
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) |
| 71 |
13
|
eleq2d |
⊢ ( 𝑁 ∈ ℕ → ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
| 72 |
|
elee |
⊢ ( 𝑁 ∈ ℕ → ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 73 |
72
|
biimpd |
⊢ ( 𝑁 ∈ ℕ → ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 74 |
71 73
|
sylbid |
⊢ ( 𝑁 ∈ ℕ → ( 𝑝 ∈ 𝑃 → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 75 |
74
|
3ad2ant1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → ( 𝑝 ∈ 𝑃 → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 76 |
75
|
imp |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ ) |
| 77 |
76
|
ffvelcdmda |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℝ ) |
| 78 |
77
|
recnd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℂ ) |
| 79 |
78
|
mul02d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 0 · ( 𝑝 ‘ 𝑖 ) ) = 0 ) |
| 80 |
22 53
|
mpbidi |
⊢ ( 𝑦 ∈ 𝑃 → ( 𝑁 ∈ ℕ → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 81 |
80 7
|
syl11 |
⊢ ( 𝑁 ∈ ℕ → ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 82 |
81
|
a1d |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 → ( 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) ) |
| 83 |
82
|
3imp |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ ) |
| 84 |
83
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ ) |
| 85 |
84
|
ffvelcdmda |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℝ ) |
| 86 |
85
|
recnd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℂ ) |
| 87 |
86
|
mullidd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 · ( 𝑦 ‘ 𝑖 ) ) = ( 𝑦 ‘ 𝑖 ) ) |
| 88 |
79 87
|
oveq12d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) = ( 0 + ( 𝑦 ‘ 𝑖 ) ) ) |
| 89 |
86
|
addlidd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 0 + ( 𝑦 ‘ 𝑖 ) ) = ( 𝑦 ‘ 𝑖 ) ) |
| 90 |
88 89
|
eqtrd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) = ( 𝑦 ‘ 𝑖 ) ) |
| 91 |
90
|
eqeq2d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) |
| 92 |
91
|
ralbidva |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) |
| 93 |
70 92
|
mtbird |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 94 |
|
1re |
⊢ 1 ∈ ℝ |
| 95 |
|
oveq2 |
⊢ ( 𝑙 = 1 → ( 1 − 𝑙 ) = ( 1 − 1 ) ) |
| 96 |
95
|
oveq1d |
⊢ ( 𝑙 = 1 → ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 1 − 1 ) · ( 𝑝 ‘ 𝑖 ) ) ) |
| 97 |
|
1m1e0 |
⊢ ( 1 − 1 ) = 0 |
| 98 |
97
|
oveq1i |
⊢ ( ( 1 − 1 ) · ( 𝑝 ‘ 𝑖 ) ) = ( 0 · ( 𝑝 ‘ 𝑖 ) ) |
| 99 |
96 98
|
eqtrdi |
⊢ ( 𝑙 = 1 → ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) = ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) |
| 100 |
|
oveq1 |
⊢ ( 𝑙 = 1 → ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) = ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) |
| 101 |
99 100
|
oveq12d |
⊢ ( 𝑙 = 1 → ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 102 |
101
|
eqeq2d |
⊢ ( 𝑙 = 1 → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 103 |
102
|
ralbidv |
⊢ ( 𝑙 = 1 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 104 |
103
|
rexsng |
⊢ ( 1 ∈ ℝ → ( ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 105 |
94 104
|
ax-mp |
⊢ ( ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( 0 · ( 𝑝 ‘ 𝑖 ) ) + ( 1 · ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 106 |
93 105
|
sylnibr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ¬ ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 107 |
2
|
raleqi |
⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 108 |
107
|
rexbii |
⊢ ( ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) |
| 109 |
|
biorf |
⊢ ( ¬ ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) → ( ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) ) |
| 110 |
108 109
|
bitrid |
⊢ ( ¬ ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) → ( ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) ) |
| 111 |
106 110
|
syl |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) ) |
| 112 |
|
orcom |
⊢ ( ( ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 113 |
111 112
|
bitr2di |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ { 1 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 114 |
45 113
|
bitrid |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑙 ∈ ( ( 0 [,) 1 ) ∪ { 1 } ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 115 |
36 44 114
|
3bitrd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑥 ∈ ( 𝑝 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ↔ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) |
| 116 |
5 1 3 6 10 9
|
ebtwntg |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑦 Btwn ⟨ 𝑥 , 𝑝 ⟩ ↔ 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑝 ) ) ) |
| 117 |
|
brbtwn |
⊢ ( ( 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑦 Btwn ⟨ 𝑥 , 𝑝 ⟩ ↔ ∃ 𝑚 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 118 |
26 20 16 117
|
syl3anc |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑦 Btwn ⟨ 𝑥 , 𝑝 ⟩ ↔ ∃ 𝑚 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 119 |
116 118
|
bitr3d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑝 ) ↔ ∃ 𝑚 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 120 |
|
snunioc |
⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 0 ≤ 1 ) → ( { 0 } ∪ ( 0 (,] 1 ) ) = ( 0 [,] 1 ) ) |
| 121 |
37 38 39 120
|
mp3an |
⊢ ( { 0 } ∪ ( 0 (,] 1 ) ) = ( 0 [,] 1 ) |
| 122 |
121
|
eqcomi |
⊢ ( 0 [,] 1 ) = ( { 0 } ∪ ( 0 (,] 1 ) ) |
| 123 |
122
|
a1i |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 0 [,] 1 ) = ( { 0 } ∪ ( 0 (,] 1 ) ) ) |
| 124 |
123
|
rexeqdv |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑚 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∃ 𝑚 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 125 |
|
rexun |
⊢ ( ∃ 𝑚 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 126 |
|
eqcom |
⊢ ( ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ( 𝑦 ‘ 𝑖 ) = ( 𝑥 ‘ 𝑖 ) ) |
| 127 |
126
|
ralbii |
⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( 𝑥 ‘ 𝑖 ) ) |
| 128 |
70 127
|
sylnib |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( 𝑥 ‘ 𝑖 ) ) |
| 129 |
17
|
biimpd |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) |
| 130 |
129 47
|
sylibd |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
| 131 |
130
|
imp |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ ) |
| 132 |
131
|
3adant3 |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ ) |
| 133 |
132
|
adantr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ ) |
| 134 |
133
|
ffvelcdmda |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℝ ) |
| 135 |
134
|
recnd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ ) |
| 136 |
135
|
mullidd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 · ( 𝑥 ‘ 𝑖 ) ) = ( 𝑥 ‘ 𝑖 ) ) |
| 137 |
136 79
|
oveq12d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) = ( ( 𝑥 ‘ 𝑖 ) + 0 ) ) |
| 138 |
135
|
addridd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) + 0 ) = ( 𝑥 ‘ 𝑖 ) ) |
| 139 |
137 138
|
eqtrd |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) = ( 𝑥 ‘ 𝑖 ) ) |
| 140 |
139
|
eqeq2d |
⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) = ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( 𝑦 ‘ 𝑖 ) = ( 𝑥 ‘ 𝑖 ) ) ) |
| 141 |
140
|
ralbidva |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( 𝑥 ‘ 𝑖 ) ) ) |
| 142 |
128 141
|
mtbird |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) ) |
| 143 |
|
0re |
⊢ 0 ∈ ℝ |
| 144 |
|
oveq2 |
⊢ ( 𝑚 = 0 → ( 1 − 𝑚 ) = ( 1 − 0 ) ) |
| 145 |
144
|
oveq1d |
⊢ ( 𝑚 = 0 → ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − 0 ) · ( 𝑥 ‘ 𝑖 ) ) ) |
| 146 |
|
1m0e1 |
⊢ ( 1 − 0 ) = 1 |
| 147 |
146
|
oveq1i |
⊢ ( ( 1 − 0 ) · ( 𝑥 ‘ 𝑖 ) ) = ( 1 · ( 𝑥 ‘ 𝑖 ) ) |
| 148 |
145 147
|
eqtrdi |
⊢ ( 𝑚 = 0 → ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) = ( 1 · ( 𝑥 ‘ 𝑖 ) ) ) |
| 149 |
|
oveq1 |
⊢ ( 𝑚 = 0 → ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) = ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) |
| 150 |
148 149
|
oveq12d |
⊢ ( 𝑚 = 0 → ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) = ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) ) |
| 151 |
150
|
eqeq2d |
⊢ ( 𝑚 = 0 → ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( 𝑦 ‘ 𝑖 ) = ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 152 |
151
|
ralbidv |
⊢ ( 𝑚 = 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 153 |
152
|
rexsng |
⊢ ( 0 ∈ ℝ → ( ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 154 |
143 153
|
ax-mp |
⊢ ( ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( 1 · ( 𝑥 ‘ 𝑖 ) ) + ( 0 · ( 𝑝 ‘ 𝑖 ) ) ) ) |
| 155 |
142 154
|
sylnibr |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ¬ ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) |
| 156 |
2
|
raleqi |
⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) |
| 157 |
156
|
rexbii |
⊢ ( ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) |
| 158 |
|
biorf |
⊢ ( ¬ ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) → ( ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) |
| 159 |
157 158
|
bitrid |
⊢ ( ¬ ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) → ( ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) |
| 160 |
155 159
|
syl |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑚 ∈ { 0 } ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) |
| 161 |
125 160
|
bitr4id |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ∃ 𝑚 ∈ ( { 0 } ∪ ( 0 (,] 1 ) ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 162 |
119 124 161
|
3bitrd |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑝 ) ↔ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) |
| 163 |
32 115 162
|
3orbi123d |
⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑝 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑝 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑝 ) ) ↔ ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) |
| 164 |
163
|
rabbidva |
⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝑃 ∧ 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ) → { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑝 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑝 ) ) } = { 𝑝 ∈ 𝑃 ∣ ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) } ) |
| 165 |
164
|
mpoeq3dva |
⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( 𝑝 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ∨ 𝑥 ∈ ( 𝑝 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑝 ) ) } ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) } ) ) |
| 166 |
4 165
|
eqtrd |
⊢ ( 𝑁 ∈ ℕ → ( LineG ‘ ( EEG ‘ 𝑁 ) ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑝 ∈ 𝑃 ∣ ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) } ) ) |