Proof of Theorem pthdlem2
| Step | Hyp | Ref
| Expression |
| 1 | | pthd.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ Word V) |
| 2 | | lencl 14571 |
. . . 4
⊢ (𝑃 ∈ Word V →
(♯‘𝑃) ∈
ℕ0) |
| 3 | | df-ne 2941 |
. . . . 5
⊢
((♯‘𝑃)
≠ 0 ↔ ¬ (♯‘𝑃) = 0) |
| 4 | | elnnne0 12540 |
. . . . . 6
⊢
((♯‘𝑃)
∈ ℕ ↔ ((♯‘𝑃) ∈ ℕ0 ∧
(♯‘𝑃) ≠
0)) |
| 5 | 4 | simplbi2 500 |
. . . . 5
⊢
((♯‘𝑃)
∈ ℕ0 → ((♯‘𝑃) ≠ 0 → (♯‘𝑃) ∈
ℕ)) |
| 6 | 3, 5 | biimtrrid 243 |
. . . 4
⊢
((♯‘𝑃)
∈ ℕ0 → (¬ (♯‘𝑃) = 0 → (♯‘𝑃) ∈
ℕ)) |
| 7 | 1, 2, 6 | 3syl 18 |
. . 3
⊢ (𝜑 → (¬
(♯‘𝑃) = 0
→ (♯‘𝑃)
∈ ℕ)) |
| 8 | | eqid 2737 |
. . . . . . 7
⊢ 0 =
0 |
| 9 | 8 | orci 866 |
. . . . . 6
⊢ (0 = 0
∨ 0 = 𝑅) |
| 10 | | pthd.r |
. . . . . . 7
⊢ 𝑅 = ((♯‘𝑃) − 1) |
| 11 | | pthd.s |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) |
| 12 | 1, 10, 11 | pthdlem2lem 29787 |
. . . . . 6
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (0 = 0
∨ 0 = 𝑅)) → (𝑃‘0) ∉ (𝑃 “ (1..^𝑅))) |
| 13 | 9, 12 | mp3an3 1452 |
. . . . 5
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ) → (𝑃‘0) ∉ (𝑃 “ (1..^𝑅))) |
| 14 | | eqid 2737 |
. . . . . . 7
⊢ 𝑅 = 𝑅 |
| 15 | 14 | olci 867 |
. . . . . 6
⊢ (𝑅 = 0 ∨ 𝑅 = 𝑅) |
| 16 | 1, 10, 11 | pthdlem2lem 29787 |
. . . . . 6
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝑅 = 0 ∨ 𝑅 = 𝑅)) → (𝑃‘𝑅) ∉ (𝑃 “ (1..^𝑅))) |
| 17 | 15, 16 | mp3an3 1452 |
. . . . 5
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ) → (𝑃‘𝑅) ∉ (𝑃 “ (1..^𝑅))) |
| 18 | | wrdffz 14573 |
. . . . . . . . 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 7442 |
. . . . . . . 8
⊢
(0...𝑅) =
(0...((♯‘𝑃)
− 1)) |
| 22 | 21 | feq2i 6728 |
. . . . . . 7
⊢ (𝑃:(0...𝑅)⟶V ↔ 𝑃:(0...((♯‘𝑃) − 1))⟶V) |
| 23 | 20, 22 | sylibr 234 |
. . . . . 6
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ) → 𝑃:(0...𝑅)⟶V) |
| 24 | | nnm1nn0 12567 |
. . . . . . . 8
⊢
((♯‘𝑃)
∈ ℕ → ((♯‘𝑃) − 1) ∈
ℕ0) |
| 25 | 10, 24 | eqeltrid 2845 |
. . . . . . 7
⊢
((♯‘𝑃)
∈ ℕ → 𝑅
∈ ℕ0) |
| 26 | 25 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ) → 𝑅 ∈
ℕ0) |
| 27 | | fvinim0ffz 13825 |
. . . . . 6
⊢ ((𝑃:(0...𝑅)⟶V ∧ 𝑅 ∈ ℕ0) → (((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^𝑅)) ∧ (𝑃‘𝑅) ∉ (𝑃 “ (1..^𝑅))))) |
| 28 | 23, 26, 27 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ) →
(((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^𝑅)) ∧ (𝑃‘𝑅) ∉ (𝑃 “ (1..^𝑅))))) |
| 29 | 13, 17, 28 | mpbir2and 713 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ) → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) |
| 30 | 29 | ex 412 |
. . 3
⊢ (𝜑 → ((♯‘𝑃) ∈ ℕ → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅)) |
| 31 | 7, 30 | syld 47 |
. 2
⊢ (𝜑 → (¬
(♯‘𝑃) = 0
→ ((𝑃 “ {0,
𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅)) |
| 32 | | oveq1 7438 |
. . . . . . . . 9
⊢
((♯‘𝑃) =
0 → ((♯‘𝑃)
− 1) = (0 − 1)) |
| 33 | 10, 32 | eqtrid 2789 |
. . . . . . . 8
⊢
((♯‘𝑃) =
0 → 𝑅 = (0 −
1)) |
| 34 | 33 | oveq2d 7447 |
. . . . . . 7
⊢
((♯‘𝑃) =
0 → (1..^𝑅) = (1..^(0
− 1))) |
| 35 | | 0le2 12368 |
. . . . . . . . . 10
⊢ 0 ≤
2 |
| 36 | | 1p1e2 12391 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
| 37 | 35, 36 | breqtrri 5170 |
. . . . . . . . 9
⊢ 0 ≤ (1
+ 1) |
| 38 | | 0re 11263 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
| 39 | | 1re 11261 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
| 40 | 38, 39, 39 | lesubadd2i 11823 |
. . . . . . . . 9
⊢ ((0
− 1) ≤ 1 ↔ 0 ≤ (1 + 1)) |
| 41 | 37, 40 | mpbir 231 |
. . . . . . . 8
⊢ (0
− 1) ≤ 1 |
| 42 | | 1z 12647 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
| 43 | | 0z 12624 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
| 44 | | peano2zm 12660 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → (0 − 1) ∈ ℤ) |
| 45 | 43, 44 | ax-mp 5 |
. . . . . . . . 9
⊢ (0
− 1) ∈ ℤ |
| 46 | | fzon 13720 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ (0 − 1) ∈ ℤ) → ((0 − 1) ≤ 1
↔ (1..^(0 − 1)) = ∅)) |
| 47 | 42, 45, 46 | mp2an 692 |
. . . . . . . 8
⊢ ((0
− 1) ≤ 1 ↔ (1..^(0 − 1)) = ∅) |
| 48 | 41, 47 | mpbi 230 |
. . . . . . 7
⊢ (1..^(0
− 1)) = ∅ |
| 49 | 34, 48 | eqtrdi 2793 |
. . . . . 6
⊢
((♯‘𝑃) =
0 → (1..^𝑅) =
∅) |
| 50 | 49 | imaeq2d 6078 |
. . . . 5
⊢
((♯‘𝑃) =
0 → (𝑃 “
(1..^𝑅)) = (𝑃 “
∅)) |
| 51 | | ima0 6095 |
. . . . 5
⊢ (𝑃 “ ∅) =
∅ |
| 52 | 50, 51 | eqtrdi 2793 |
. . . 4
⊢
((♯‘𝑃) =
0 → (𝑃 “
(1..^𝑅)) =
∅) |
| 53 | 52 | ineq2d 4220 |
. . 3
⊢
((♯‘𝑃) =
0 → ((𝑃 “ {0,
𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ((𝑃 “ {0, 𝑅}) ∩ ∅)) |
| 54 | | in0 4395 |
. . 3
⊢ ((𝑃 “ {0, 𝑅}) ∩ ∅) = ∅ |
| 55 | 53, 54 | eqtrdi 2793 |
. 2
⊢
((♯‘𝑃) =
0 → ((𝑃 “ {0,
𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) |
| 56 | 31, 55 | pm2.61d2 181 |
1
⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) |