Step |
Hyp |
Ref |
Expression |
1 |
|
eluz2b2 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) ) |
2 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
3 |
2
|
a1i |
⊢ ( ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) → 1 ∈ ℕ0 ) |
4 |
|
simpl |
⊢ ( ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) → 𝑁 ∈ ℕ ) |
5 |
|
simpr |
⊢ ( ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) → 1 < 𝑁 ) |
6 |
|
elfzo0 |
⊢ ( 1 ∈ ( 0 ..^ 𝑁 ) ↔ ( 1 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) ) |
7 |
3 4 5 6
|
syl3anbrc |
⊢ ( ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) → 1 ∈ ( 0 ..^ 𝑁 ) ) |
8 |
1 7
|
sylbi |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ( 0 ..^ 𝑁 ) ) |
9 |
8
|
3ad2ant2 |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → 1 ∈ ( 0 ..^ 𝑁 ) ) |
10 |
|
fveq2 |
⊢ ( 𝑖 = 1 → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 1 ) ) |
11 |
10
|
adantl |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ 𝑖 = 1 ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 1 ) ) |
12 |
11
|
neeq1d |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) ∧ 𝑖 = 1 ) → ( ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ↔ ( 𝑊 ‘ 1 ) ≠ ( 𝑊 ‘ 0 ) ) ) |
13 |
|
umgr2cwwk2dif |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ( 𝑊 ‘ 1 ) ≠ ( 𝑊 ‘ 0 ) ) |
14 |
9 12 13
|
rspcedvd |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) |