Metamath Proof Explorer

Theorem pthdlem2

Description: Lemma 2 for pthd . (Contributed by Alexander van der Vekens, 11-Nov-2017) (Revised by AV, 10-Feb-2021)

Ref Expression
Hypotheses pthd.p ⊢ ( 𝜑 → 𝑃 ∈ Word V )
pthd.r ⊢ 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 )
pthd.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
Assertion pthdlem2 ( 𝜑 → ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 pthd.p ⊢ ( 𝜑 → 𝑃 ∈ Word V )
2 pthd.r ⊢ 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 )
3 pthd.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
4 lencl ⊢ ( 𝑃 ∈ Word V → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
5 df-ne ⊢ ( ( ♯ ‘ 𝑃 ) ≠ 0 ↔ ¬ ( ♯ ‘ 𝑃 ) = 0 )
6 elnnne0 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) ≠ 0 ) )
7 6 simplbi2 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) ≠ 0 → ( ♯ ‘ 𝑃 ) ∈ ℕ ) )
8 5 7 syl5bir ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ¬ ( ♯ ‘ 𝑃 ) = 0 → ( ♯ ‘ 𝑃 ) ∈ ℕ ) )
9 1 4 8 3syl ⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝑃 ) = 0 → ( ♯ ‘ 𝑃 ) ∈ ℕ ) )
10 eqid ⊢ 0 = 0
11 10 orci ⊢ ( 0 = 0 ∨ 0 = 𝑅 )
12 1 2 3 pthdlem2lem ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 0 = 0 ∨ 0 = 𝑅 ) ) → ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) )
13 11 12 mp3an3 ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ) → ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) )
14 eqid ⊢ 𝑅 = 𝑅
15 14 olci ⊢ ( 𝑅 = 0 ∨ 𝑅 = 𝑅 )
16 1 2 3 pthdlem2lem ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ∧ ( 𝑅 = 0 ∨ 𝑅 = 𝑅 ) ) → ( 𝑃 ‘ 𝑅 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) )
17 15 16 mp3an3 ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ) → ( 𝑃 ‘ 𝑅 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) )
18 wrdffz ⊢ ( 𝑃 ∈ Word V → 𝑃 : ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ V )
19 1 18 syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ V )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ) → 𝑃 : ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ V )
21 2 oveq2i ⊢ ( 0 ... 𝑅 ) = ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) )
22 21 feq2i ⊢ ( 𝑃 : ( 0 ... 𝑅 ) ⟶ V ↔ 𝑃 : ( 0 ... ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ V )
23 20 22 sylibr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ) → 𝑃 : ( 0 ... 𝑅 ) ⟶ V )
24 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 )
25 2 24 eqeltrid ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → 𝑅 ∈ ℕ0 )
26 25 adantl ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ) → 𝑅 ∈ ℕ0 )
27 fvinim0ffz ⊢ ( ( 𝑃 : ( 0 ... 𝑅 ) ⟶ V ∧ 𝑅 ∈ ℕ0 ) → ( ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ∅ ↔ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ∧ ( 𝑃 ‘ 𝑅 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) ) )
28 23 26 27 syl2anc ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ) → ( ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ∅ ↔ ( ( 𝑃 ‘ 0 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ∧ ( 𝑃 ‘ 𝑅 ) ∉ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) ) )
29 13 17 28 mpbir2and ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) ∈ ℕ ) → ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ∅ )
30 29 ex ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ∅ ) )
31 9 30 syld ⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝑃 ) = 0 → ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ∅ ) )
32 oveq1 ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( 0 − 1 ) )
33 2 32 syl5eq ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → 𝑅 = ( 0 − 1 ) )
34 33 oveq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → ( 1 ..^ 𝑅 ) = ( 1 ..^ ( 0 − 1 ) ) )
35 0le2 ⊢ 0 ≤ 2
36 1p1e2 ⊢ ( 1 + 1 ) = 2
37 35 36 breqtrri ⊢ 0 ≤ ( 1 + 1 )
38 0re ⊢ 0 ∈ ℝ
39 1re ⊢ 1 ∈ ℝ
40 38 39 39 lesubadd2i ⊢ ( ( 0 − 1 ) ≤ 1 ↔ 0 ≤ ( 1 + 1 ) )
41 37 40 mpbir ⊢ ( 0 − 1 ) ≤ 1
42 1z ⊢ 1 ∈ ℤ
43 0z ⊢ 0 ∈ ℤ
44 peano2zm ⊢ ( 0 ∈ ℤ → ( 0 − 1 ) ∈ ℤ )
45 43 44 ax-mp ⊢ ( 0 − 1 ) ∈ ℤ
46 fzon ⊢ ( ( 1 ∈ ℤ ∧ ( 0 − 1 ) ∈ ℤ ) → ( ( 0 − 1 ) ≤ 1 ↔ ( 1 ..^ ( 0 − 1 ) ) = ∅ ) )
47 42 45 46 mp2an ⊢ ( ( 0 − 1 ) ≤ 1 ↔ ( 1 ..^ ( 0 − 1 ) ) = ∅ )
48 41 47 mpbi ⊢ ( 1 ..^ ( 0 − 1 ) ) = ∅
49 34 48 eqtrdi ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → ( 1 ..^ 𝑅 ) = ∅ )
50 49 imaeq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → ( 𝑃 “ ( 1 ..^ 𝑅 ) ) = ( 𝑃 “ ∅ ) )
51 ima0 ⊢ ( 𝑃 “ ∅ ) = ∅
52 50 51 eqtrdi ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → ( 𝑃 “ ( 1 ..^ 𝑅 ) ) = ∅ )
53 52 ineq2d ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ∅ ) )
54 in0 ⊢ ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ∅ ) = ∅
55 53 54 eqtrdi ⊢ ( ( ♯ ‘ 𝑃 ) = 0 → ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ∅ )
56 31 55 pm2.61d2 ⊢ ( 𝜑 → ( ( 𝑃 “ { 0 , 𝑅 } ) ∩ ( 𝑃 “ ( 1 ..^ 𝑅 ) ) ) = ∅ )