Metamath Proof Explorer

Theorem pthdlem2lem

Description: Lemma for pthdlem2 . (Contributed 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 pthdlem2lem ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → P ⁡ I ∉ 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 3 3ad2ant1 ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
5 ralcom ⊢ ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ j ∈ 1 ..^ R ∀ i ∈ 0 ..^ P i ≠ j → P ⁡ i ≠ P ⁡ j
6 elfzo1 ⊢ j ∈ 1 ..^ R ↔ j ∈ ℕ ∧ R ∈ ℕ ∧ j < R
7 nnne0 ⊢ j ∈ ℕ → j ≠ 0
8 7 necomd ⊢ j ∈ ℕ → 0 ≠ j
9 8 3ad2ant1 ⊢ j ∈ ℕ ∧ R ∈ ℕ ∧ j < R → 0 ≠ j
10 6 9 sylbi ⊢ j ∈ 1 ..^ R → 0 ≠ j
11 10 adantl ⊢ P ∈ ℕ ∧ j ∈ 1 ..^ R → 0 ≠ j
12 neeq1 ⊢ I = 0 → I ≠ j ↔ 0 ≠ j
13 11 12 imbitrrid ⊢ I = 0 → P ∈ ℕ ∧ j ∈ 1 ..^ R → I ≠ j
14 13 expd ⊢ I = 0 → P ∈ ℕ → j ∈ 1 ..^ R → I ≠ j
15 nnre ⊢ j ∈ ℕ → j ∈ ℝ
16 15 adantr ⊢ j ∈ ℕ ∧ R ∈ ℕ → j ∈ ℝ
17 nnre ⊢ R ∈ ℕ → R ∈ ℝ
18 17 adantl ⊢ j ∈ ℕ ∧ R ∈ ℕ → R ∈ ℝ
19 16 18 ltlend ⊢ j ∈ ℕ ∧ R ∈ ℕ → j < R ↔ j ≤ R ∧ R ≠ j
20 simpr ⊢ j ≤ R ∧ R ≠ j → R ≠ j
21 19 20 biimtrdi ⊢ j ∈ ℕ ∧ R ∈ ℕ → j < R → R ≠ j
22 21 3impia ⊢ j ∈ ℕ ∧ R ∈ ℕ ∧ j < R → R ≠ j
23 6 22 sylbi ⊢ j ∈ 1 ..^ R → R ≠ j
24 23 adantl ⊢ P ∈ ℕ ∧ j ∈ 1 ..^ R → R ≠ j
25 neeq1 ⊢ I = R → I ≠ j ↔ R ≠ j
26 24 25 imbitrrid ⊢ I = R → P ∈ ℕ ∧ j ∈ 1 ..^ R → I ≠ j
27 26 expd ⊢ I = R → P ∈ ℕ → j ∈ 1 ..^ R → I ≠ j
28 14 27 jaoi ⊢ I = 0 ∨ I = R → P ∈ ℕ → j ∈ 1 ..^ R → I ≠ j
29 28 impcom ⊢ P ∈ ℕ ∧ I = 0 ∨ I = R → j ∈ 1 ..^ R → I ≠ j
30 29 3adant1 ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → j ∈ 1 ..^ R → I ≠ j
31 30 imp ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R ∧ j ∈ 1 ..^ R → I ≠ j
32 lbfzo0 ⊢ 0 ∈ 0 ..^ P ↔ P ∈ ℕ
33 32 biimpri ⊢ P ∈ ℕ → 0 ∈ 0 ..^ P
34 eleq1 ⊢ I = 0 → I ∈ 0 ..^ P ↔ 0 ∈ 0 ..^ P
35 33 34 imbitrrid ⊢ I = 0 → P ∈ ℕ → I ∈ 0 ..^ P
36 fzo0end ⊢ P ∈ ℕ → P − 1 ∈ 0 ..^ P
37 2 36 eqeltrid ⊢ P ∈ ℕ → R ∈ 0 ..^ P
38 eleq1 ⊢ I = R → I ∈ 0 ..^ P ↔ R ∈ 0 ..^ P
39 37 38 imbitrrid ⊢ I = R → P ∈ ℕ → I ∈ 0 ..^ P
40 35 39 jaoi ⊢ I = 0 ∨ I = R → P ∈ ℕ → I ∈ 0 ..^ P
41 40 impcom ⊢ P ∈ ℕ ∧ I = 0 ∨ I = R → I ∈ 0 ..^ P
42 41 3adant1 ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → I ∈ 0 ..^ P
43 42 adantr ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R ∧ j ∈ 1 ..^ R → I ∈ 0 ..^ P
44 neeq1 ⊢ i = I → i ≠ j ↔ I ≠ j
45 fveq2 ⊢ i = I → P ⁡ i = P ⁡ I
46 45 neeq1d ⊢ i = I → P ⁡ i ≠ P ⁡ j ↔ P ⁡ I ≠ P ⁡ j
47 44 46 imbi12d ⊢ i = I → i ≠ j → P ⁡ i ≠ P ⁡ j ↔ I ≠ j → P ⁡ I ≠ P ⁡ j
48 47 rspcv ⊢ I ∈ 0 ..^ P → ∀ i ∈ 0 ..^ P i ≠ j → P ⁡ i ≠ P ⁡ j → I ≠ j → P ⁡ I ≠ P ⁡ j
49 43 48 syl ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R ∧ j ∈ 1 ..^ R → ∀ i ∈ 0 ..^ P i ≠ j → P ⁡ i ≠ P ⁡ j → I ≠ j → P ⁡ I ≠ P ⁡ j
50 31 49 mpid ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R ∧ j ∈ 1 ..^ R → ∀ i ∈ 0 ..^ P i ≠ j → P ⁡ i ≠ P ⁡ j → P ⁡ I ≠ P ⁡ j
51 nesym ⊢ P ⁡ I ≠ P ⁡ j ↔ ¬ P ⁡ j = P ⁡ I
52 50 51 imbitrdi ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R ∧ j ∈ 1 ..^ R → ∀ i ∈ 0 ..^ P i ≠ j → P ⁡ i ≠ P ⁡ j → ¬ P ⁡ j = P ⁡ I
53 52 ralimdva ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → ∀ j ∈ 1 ..^ R ∀ i ∈ 0 ..^ P i ≠ j → P ⁡ i ≠ P ⁡ j → ∀ j ∈ 1 ..^ R ¬ P ⁡ j = P ⁡ I
54 5 53 biimtrid ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j → ∀ j ∈ 1 ..^ R ¬ P ⁡ j = P ⁡ I
55 4 54 mpd ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → ∀ j ∈ 1 ..^ R ¬ P ⁡ j = P ⁡ I
56 ralnex ⊢ ∀ j ∈ 1 ..^ R ¬ P ⁡ j = P ⁡ I ↔ ¬ ∃ j ∈ 1 ..^ R P ⁡ j = P ⁡ I
57 55 56 sylib ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → ¬ ∃ j ∈ 1 ..^ R P ⁡ j = P ⁡ I
58 wrdf ⊢ P ∈ Word V → P : 0 ..^ P ⟶ V
59 ffun ⊢ P : 0 ..^ P ⟶ V → Fun ⁡ P
60 1 58 59 3syl ⊢ φ → Fun ⁡ P
61 60 3ad2ant1 ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → Fun ⁡ P
62 fvelima ⊢ Fun ⁡ P ∧ P ⁡ I ∈ P 1 ..^ R → ∃ j ∈ 1 ..^ R P ⁡ j = P ⁡ I
63 62 ex ⊢ Fun ⁡ P → P ⁡ I ∈ P 1 ..^ R → ∃ j ∈ 1 ..^ R P ⁡ j = P ⁡ I
64 61 63 syl ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → P ⁡ I ∈ P 1 ..^ R → ∃ j ∈ 1 ..^ R P ⁡ j = P ⁡ I
65 57 64 mtod ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → ¬ P ⁡ I ∈ P 1 ..^ R
66 df-nel ⊢ P ⁡ I ∉ P 1 ..^ R ↔ ¬ P ⁡ I ∈ P 1 ..^ R
67 65 66 sylibr ⊢ φ ∧ P ∈ ℕ ∧ I = 0 ∨ I = R → P ⁡ I ∉ P 1 ..^ R