Proof of Theorem pfxnd0
Step | Hyp | Ref
| Expression |
1 | | df-nel 3123 |
. . . . 5
⊢ (𝐿 ∉
(0...(♯‘𝑊))
↔ ¬ 𝐿 ∈
(0...(♯‘𝑊))) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝐿 ∉ (0...(♯‘𝑊)) ↔ ¬ 𝐿 ∈
(0...(♯‘𝑊)))) |
3 | | elfz2nn0 12995 |
. . . . . 6
⊢ (𝐿 ∈
(0...(♯‘𝑊))
↔ (𝐿 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑊))) |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (𝐿 ∈ (0...(♯‘𝑊)) ↔ (𝐿 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ0 ∧ 𝐿
≤ (♯‘𝑊)))) |
5 | 4 | notbid 320 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (¬ 𝐿 ∈ (0...(♯‘𝑊)) ↔ ¬ (𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑊)))) |
6 | | 3ianor 1102 |
. . . . 5
⊢ (¬
(𝐿 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑊)) ↔ (¬ 𝐿 ∈ ℕ0 ∨
¬ (♯‘𝑊)
∈ ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑊))) |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (¬ (𝐿 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ0 ∧ 𝐿
≤ (♯‘𝑊))
↔ (¬ 𝐿 ∈
ℕ0 ∨ ¬ (♯‘𝑊) ∈ ℕ0 ∨ ¬
𝐿 ≤ (♯‘𝑊)))) |
8 | 2, 5, 7 | 3bitrd 307 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → (𝐿 ∉ (0...(♯‘𝑊)) ↔ (¬ 𝐿 ∈ ℕ0 ∨
¬ (♯‘𝑊)
∈ ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑊)))) |
9 | | 3orrot 1087 |
. . . . 5
⊢ ((¬
𝐿 ∈
ℕ0 ∨ ¬ (♯‘𝑊) ∈ ℕ0 ∨ ¬
𝐿 ≤ (♯‘𝑊)) ↔ (¬
(♯‘𝑊) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑊) ∨ ¬ 𝐿 ∈
ℕ0)) |
10 | | 3orass 1085 |
. . . . . 6
⊢ ((¬
(♯‘𝑊) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑊) ∨ ¬ 𝐿 ∈ ℕ0) ↔ (¬
(♯‘𝑊) ∈
ℕ0 ∨ (¬ 𝐿 ≤ (♯‘𝑊) ∨ ¬ 𝐿 ∈
ℕ0))) |
11 | | lencl 13878 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
12 | 11 | pm2.24d 154 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (¬ (♯‘𝑊) ∈ ℕ0
→ (𝑊 prefix 𝐿) = ∅)) |
13 | 12 | com12 32 |
. . . . . . 7
⊢ (¬
(♯‘𝑊) ∈
ℕ0 → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅)) |
14 | | simpr 487 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ V ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℕ0) |
15 | 14 | con3i 157 |
. . . . . . . . . . 11
⊢ (¬
𝐿 ∈
ℕ0 → ¬ (𝑊 ∈ V ∧ 𝐿 ∈
ℕ0)) |
16 | | pfxnndmnd 14029 |
. . . . . . . . . . 11
⊢ (¬
(𝑊 ∈ V ∧ 𝐿 ∈ ℕ0)
→ (𝑊 prefix 𝐿) = ∅) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ (¬
𝐿 ∈
ℕ0 → (𝑊 prefix 𝐿) = ∅) |
18 | 17 | a1d 25 |
. . . . . . . . 9
⊢ (¬
𝐿 ∈
ℕ0 → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅)) |
19 | | notnotb 317 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ ℕ0
↔ ¬ ¬ 𝐿 ∈
ℕ0) |
20 | 11 | nn0red 11950 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℝ) |
21 | | nn0re 11900 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
22 | | ltnle 10713 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑊)
∈ ℝ ∧ 𝐿
∈ ℝ) → ((♯‘𝑊) < 𝐿 ↔ ¬ 𝐿 ≤ (♯‘𝑊))) |
23 | 20, 21, 22 | syl2an 597 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0) →
((♯‘𝑊) <
𝐿 ↔ ¬ 𝐿 ≤ (♯‘𝑊))) |
24 | | pfxnd 14044 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧
(♯‘𝑊) <
𝐿) → (𝑊 prefix 𝐿) = ∅) |
25 | 24 | 3expia 1116 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0) →
((♯‘𝑊) <
𝐿 → (𝑊 prefix 𝐿) = ∅)) |
26 | 23, 25 | sylbird 262 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0) → (¬
𝐿 ≤ (♯‘𝑊) → (𝑊 prefix 𝐿) = ∅)) |
27 | 26 | expcom 416 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ ℕ0
→ (𝑊 ∈ Word 𝑉 → (¬ 𝐿 ≤ (♯‘𝑊) → (𝑊 prefix 𝐿) = ∅))) |
28 | 27 | com23 86 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ ℕ0
→ (¬ 𝐿 ≤
(♯‘𝑊) →
(𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅))) |
29 | 19, 28 | sylbir 237 |
. . . . . . . . . 10
⊢ (¬
¬ 𝐿 ∈
ℕ0 → (¬ 𝐿 ≤ (♯‘𝑊) → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅))) |
30 | 29 | imp 409 |
. . . . . . . . 9
⊢ ((¬
¬ 𝐿 ∈
ℕ0 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅)) |
31 | 18, 30 | jaoi3 1055 |
. . . . . . . 8
⊢ ((¬
𝐿 ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑊)) → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅)) |
32 | 31 | orcoms 868 |
. . . . . . 7
⊢ ((¬
𝐿 ≤ (♯‘𝑊) ∨ ¬ 𝐿 ∈ ℕ0) → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅)) |
33 | 13, 32 | jaoi 853 |
. . . . . 6
⊢ ((¬
(♯‘𝑊) ∈
ℕ0 ∨ (¬ 𝐿 ≤ (♯‘𝑊) ∨ ¬ 𝐿 ∈ ℕ0)) → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅)) |
34 | 10, 33 | sylbi 219 |
. . . . 5
⊢ ((¬
(♯‘𝑊) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑊) ∨ ¬ 𝐿 ∈ ℕ0) → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅)) |
35 | 9, 34 | sylbi 219 |
. . . 4
⊢ ((¬
𝐿 ∈
ℕ0 ∨ ¬ (♯‘𝑊) ∈ ℕ0 ∨ ¬
𝐿 ≤ (♯‘𝑊)) → (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) = ∅)) |
36 | 35 | com12 32 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → ((¬ 𝐿 ∈ ℕ0 ∨ ¬
(♯‘𝑊) ∈
ℕ0 ∨ ¬ 𝐿 ≤ (♯‘𝑊)) → (𝑊 prefix 𝐿) = ∅)) |
37 | 8, 36 | sylbid 242 |
. 2
⊢ (𝑊 ∈ Word 𝑉 → (𝐿 ∉ (0...(♯‘𝑊)) → (𝑊 prefix 𝐿) = ∅)) |
38 | 37 | imp 409 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∉ (0...(♯‘𝑊))) → (𝑊 prefix 𝐿) = ∅) |