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 ⊢ φ → P ∈ Word V
pthd.r ⊢ R = P − 1
pthd.s ⊢ φ → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
Assertion pthdlem2 ⊢ φ → P 0 R ∩ P 1 ..^ R = ∅

Proof

Step Hyp Ref Expression
1 pthd.p ⊢ φ → P ∈ Word V
2 pthd.r ⊢ R = P − 1
3 pthd.s ⊢ φ → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
4 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
5 df-ne ⊢ P ≠ 0 ↔ ¬ P = 0
6 elnnne0 ⊢ P ∈ ℕ ↔ P ∈ ℕ 0 ∧ P ≠ 0
7 6 simplbi2 ⊢ P ∈ ℕ 0 → P ≠ 0 → P ∈ ℕ
8 5 7 syl5bir ⊢ P ∈ ℕ 0 → ¬ P = 0 → P ∈ ℕ
9 1 4 8 3syl ⊢ φ → ¬ P = 0 → P ∈ ℕ
10 eqid ⊢ 0 = 0
11 10 orci ⊢ 0 = 0 ∨ 0 = R
12 1 2 3 pthdlem2lem ⊢ φ ∧ P ∈ ℕ ∧ 0 = 0 ∨ 0 = R → P ⁡ 0 ∉ P 1 ..^ R
13 11 12 mp3an3 ⊢ φ ∧ P ∈ ℕ → P ⁡ 0 ∉ P 1 ..^ R
14 eqid ⊢ R = R
15 14 olci ⊢ R = 0 ∨ R = R
16 1 2 3 pthdlem2lem ⊢ φ ∧ P ∈ ℕ ∧ R = 0 ∨ R = R → P ⁡ R ∉ P 1 ..^ R
17 15 16 mp3an3 ⊢ φ ∧ P ∈ ℕ → P ⁡ R ∉ P 1 ..^ R
18 wrdffz ⊢ P ∈ Word V → P : 0 … P − 1 ⟶ V
19 1 18 syl ⊢ φ → P : 0 … P − 1 ⟶ V
20 19 adantr ⊢ φ ∧ P ∈ ℕ → P : 0 … P − 1 ⟶ V
21 2 oveq2i ⊢ 0 … R = 0 … P − 1
22 21 feq2i ⊢ P : 0 … R ⟶ V ↔ P : 0 … P − 1 ⟶ V
23 20 22 sylibr ⊢ φ ∧ P ∈ ℕ → P : 0 … R ⟶ V
24 nnm1nn0 ⊢ P ∈ ℕ → P − 1 ∈ ℕ 0
25 2 24 eqeltrid ⊢ P ∈ ℕ → R ∈ ℕ 0
26 25 adantl ⊢ φ ∧ P ∈ ℕ → R ∈ ℕ 0
27 fvinim0ffz ⊢ P : 0 … R ⟶ V ∧ R ∈ ℕ 0 → P 0 R ∩ P 1 ..^ R = ∅ ↔ P ⁡ 0 ∉ P 1 ..^ R ∧ P ⁡ R ∉ P 1 ..^ R
28 23 26 27 syl2anc ⊢ φ ∧ P ∈ ℕ → P 0 R ∩ P 1 ..^ R = ∅ ↔ P ⁡ 0 ∉ P 1 ..^ R ∧ P ⁡ R ∉ P 1 ..^ R
29 13 17 28 mpbir2and ⊢ φ ∧ P ∈ ℕ → P 0 R ∩ P 1 ..^ R = ∅
30 29 ex ⊢ φ → P ∈ ℕ → P 0 R ∩ P 1 ..^ R = ∅
31 9 30 syld ⊢ φ → ¬ P = 0 → P 0 R ∩ P 1 ..^ R = ∅
32 oveq1 ⊢ P = 0 → P − 1 = 0 − 1
33 2 32 eqtrid ⊢ P = 0 → R = 0 − 1
34 33 oveq2d ⊢ P = 0 → 1 ..^ R = 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 ⊢ P = 0 → 1 ..^ R = ∅
50 49 imaeq2d ⊢ P = 0 → P 1 ..^ R = P ∅
51 ima0 ⊢ P ∅ = ∅
52 50 51 eqtrdi ⊢ P = 0 → P 1 ..^ R = ∅
53 52 ineq2d ⊢ P = 0 → P 0 R ∩ P 1 ..^ R = P 0 R ∩ ∅
54 in0 ⊢ P 0 R ∩ ∅ = ∅
55 53 54 eqtrdi ⊢ P = 0 → P 0 R ∩ P 1 ..^ R = ∅
56 31 55 pm2.61d2 ⊢ φ → P 0 R ∩ P 1 ..^ R = ∅