Proof of Theorem pthdlem2
Step | Hyp | Ref
| Expression |
1 | | pthd.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ Word V) |
2 | | lencl 13179 |
. . . 4
⊢ (𝑃 ∈ Word V →
(#‘𝑃) ∈
ℕ0) |
3 | | df-ne 2782 |
. . . . 5
⊢
((#‘𝑃) ≠ 0
↔ ¬ (#‘𝑃) =
0) |
4 | | elnnne0 11183 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℕ ↔ ((#‘𝑃)
∈ ℕ0 ∧ (#‘𝑃) ≠ 0)) |
5 | 4 | simplbi2 653 |
. . . . 5
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) ≠ 0 → (#‘𝑃) ∈ ℕ)) |
6 | 3, 5 | syl5bir 232 |
. . . 4
⊢
((#‘𝑃) ∈
ℕ0 → (¬ (#‘𝑃) = 0 → (#‘𝑃) ∈ ℕ)) |
7 | 1, 2, 6 | 3syl 18 |
. . 3
⊢ (𝜑 → (¬ (#‘𝑃) = 0 → (#‘𝑃) ∈
ℕ)) |
8 | | eqid 2610 |
. . . . . . 7
⊢ 0 =
0 |
9 | 8 | orci 404 |
. . . . . 6
⊢ (0 = 0
∨ 0 = 𝑅) |
10 | | pthd.r |
. . . . . . 7
⊢ 𝑅 = ((#‘𝑃) − 1) |
11 | | pthd.s |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ (0..^(#‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) |
12 | 1, 10, 11 | pthdlem2lem 40973 |
. . . . . 6
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ ∧ (0 = 0 ∨ 0 = 𝑅)) → (𝑃‘0) ∉ (𝑃 “ (1..^𝑅))) |
13 | 9, 12 | mp3an3 1405 |
. . . . 5
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ) → (𝑃‘0) ∉ (𝑃 “ (1..^𝑅))) |
14 | | eqid 2610 |
. . . . . . 7
⊢ 𝑅 = 𝑅 |
15 | 14 | olci 405 |
. . . . . 6
⊢ (𝑅 = 0 ∨ 𝑅 = 𝑅) |
16 | 1, 10, 11 | pthdlem2lem 40973 |
. . . . . 6
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ ∧ (𝑅 = 0 ∨ 𝑅 = 𝑅)) → (𝑃‘𝑅) ∉ (𝑃 “ (1..^𝑅))) |
17 | 15, 16 | mp3an3 1405 |
. . . . 5
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ) → (𝑃‘𝑅) ∉ (𝑃 “ (1..^𝑅))) |
18 | | wrdffz 13181 |
. . . . . . . . 9
⊢ (𝑃 ∈ Word V → 𝑃:(0...((#‘𝑃) −
1))⟶V) |
19 | 1, 18 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃:(0...((#‘𝑃) − 1))⟶V) |
20 | 19 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ) → 𝑃:(0...((#‘𝑃) − 1))⟶V) |
21 | 10 | oveq2i 6560 |
. . . . . . . 8
⊢
(0...𝑅) =
(0...((#‘𝑃) −
1)) |
22 | 21 | feq2i 5950 |
. . . . . . 7
⊢ (𝑃:(0...𝑅)⟶V ↔ 𝑃:(0...((#‘𝑃) − 1))⟶V) |
23 | 20, 22 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ) → 𝑃:(0...𝑅)⟶V) |
24 | | nnm1nn0 11211 |
. . . . . . . 8
⊢
((#‘𝑃) ∈
ℕ → ((#‘𝑃)
− 1) ∈ ℕ0) |
25 | 10, 24 | syl5eqel 2692 |
. . . . . . 7
⊢
((#‘𝑃) ∈
ℕ → 𝑅 ∈
ℕ0) |
26 | 25 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ) → 𝑅 ∈
ℕ0) |
27 | | fvinim0ffz 12449 |
. . . . . 6
⊢ ((𝑃:(0...𝑅)⟶V ∧ 𝑅 ∈ ℕ0) → (((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^𝑅)) ∧ (𝑃‘𝑅) ∉ (𝑃 “ (1..^𝑅))))) |
28 | 23, 26, 27 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ) → (((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^𝑅)) ∧ (𝑃‘𝑅) ∉ (𝑃 “ (1..^𝑅))))) |
29 | 13, 17, 28 | mpbir2and 959 |
. . . 4
⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ) → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) |
30 | 29 | ex 449 |
. . 3
⊢ (𝜑 → ((#‘𝑃) ∈ ℕ → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅)) |
31 | 7, 30 | syld 46 |
. 2
⊢ (𝜑 → (¬ (#‘𝑃) = 0 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅)) |
32 | | oveq1 6556 |
. . . . . . . . 9
⊢
((#‘𝑃) = 0
→ ((#‘𝑃) −
1) = (0 − 1)) |
33 | 10, 32 | syl5eq 2656 |
. . . . . . . 8
⊢
((#‘𝑃) = 0
→ 𝑅 = (0 −
1)) |
34 | 33 | oveq2d 6565 |
. . . . . . 7
⊢
((#‘𝑃) = 0
→ (1..^𝑅) = (1..^(0
− 1))) |
35 | | 0le2 10988 |
. . . . . . . . . 10
⊢ 0 ≤
2 |
36 | | 1p1e2 11011 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
37 | 35, 36 | breqtrri 4610 |
. . . . . . . . 9
⊢ 0 ≤ (1
+ 1) |
38 | | 0re 9919 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
39 | | 1re 9918 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
40 | 38, 39, 39 | lesubadd2i 10467 |
. . . . . . . . 9
⊢ ((0
− 1) ≤ 1 ↔ 0 ≤ (1 + 1)) |
41 | 37, 40 | mpbir 220 |
. . . . . . . 8
⊢ (0
− 1) ≤ 1 |
42 | | 1z 11284 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
43 | | 0z 11265 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
44 | | peano2zm 11297 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → (0 − 1) ∈ ℤ) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . 9
⊢ (0
− 1) ∈ ℤ |
46 | | fzon 12358 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ (0 − 1) ∈ ℤ) → ((0 − 1) ≤ 1
↔ (1..^(0 − 1)) = ∅)) |
47 | 42, 45, 46 | mp2an 704 |
. . . . . . . 8
⊢ ((0
− 1) ≤ 1 ↔ (1..^(0 − 1)) = ∅) |
48 | 41, 47 | mpbi 219 |
. . . . . . 7
⊢ (1..^(0
− 1)) = ∅ |
49 | 34, 48 | syl6eq 2660 |
. . . . . 6
⊢
((#‘𝑃) = 0
→ (1..^𝑅) =
∅) |
50 | 49 | imaeq2d 5385 |
. . . . 5
⊢
((#‘𝑃) = 0
→ (𝑃 “
(1..^𝑅)) = (𝑃 “
∅)) |
51 | | ima0 5400 |
. . . . 5
⊢ (𝑃 “ ∅) =
∅ |
52 | 50, 51 | syl6eq 2660 |
. . . 4
⊢
((#‘𝑃) = 0
→ (𝑃 “
(1..^𝑅)) =
∅) |
53 | 52 | ineq2d 3776 |
. . 3
⊢
((#‘𝑃) = 0
→ ((𝑃 “ {0,
𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ((𝑃 “ {0, 𝑅}) ∩ ∅)) |
54 | | in0 3920 |
. . 3
⊢ ((𝑃 “ {0, 𝑅}) ∩ ∅) = ∅ |
55 | 53, 54 | syl6eq 2660 |
. 2
⊢
((#‘𝑃) = 0
→ ((𝑃 “ {0,
𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) |
56 | 31, 55 | pm2.61d2 171 |
1
⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) |