Metamath Proof Explorer

Theorem pthdlem1

Description: Lemma 1 for pthd . (Contributed by Alexander van der Vekens, 13-Nov-2017) (Revised by AV, 9-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 pthdlem1 ⊢ φ → Fun ⁡ P ↾ 1 ..^ R -1

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 wrdf ⊢ P ∈ Word V → P : 0 ..^ P ⟶ V
5 1 4 syl ⊢ φ → P : 0 ..^ P ⟶ V
6 fzo0ss1 ⊢ 1 ..^ R ⊆ 0 ..^ R
7 2 a1i ⊢ φ → R = P − 1
8 7 oveq2d ⊢ φ → 0 ..^ R = 0 ..^ P − 1
9 6 8 sseqtrid ⊢ φ → 1 ..^ R ⊆ 0 ..^ P − 1
10 lencl ⊢ P ∈ Word V → P ∈ ℕ 0
11 nn0z ⊢ P ∈ ℕ 0 → P ∈ ℤ
12 1 10 11 3syl ⊢ φ → P ∈ ℤ
13 fzossrbm1 ⊢ P ∈ ℤ → 0 ..^ P − 1 ⊆ 0 ..^ P
14 12 13 syl ⊢ φ → 0 ..^ P − 1 ⊆ 0 ..^ P
15 9 14 sstrd ⊢ φ → 1 ..^ R ⊆ 0 ..^ P
16 5 15 fssresd ⊢ φ → P ↾ 1 ..^ R : 1 ..^ R ⟶ V
17 16 adantr ⊢ φ ∧ 1 < P − 1 → P ↾ 1 ..^ R : 1 ..^ R ⟶ V
18 3 adantr ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
19 1 10 syl ⊢ φ → P ∈ ℕ 0
20 nn0re ⊢ P ∈ ℕ 0 → P ∈ ℝ
21 20 ltm1d ⊢ P ∈ ℕ 0 → P − 1 < P
22 1re ⊢ 1 ∈ ℝ
23 peano2rem ⊢ P ∈ ℝ → P − 1 ∈ ℝ
24 20 23 syl ⊢ P ∈ ℕ 0 → P − 1 ∈ ℝ
25 lttr ⊢ 1 ∈ ℝ ∧ P − 1 ∈ ℝ ∧ P ∈ ℝ → 1 < P − 1 ∧ P − 1 < P → 1 < P
26 22 24 20 25 mp3an2i ⊢ P ∈ ℕ 0 → 1 < P − 1 ∧ P − 1 < P → 1 < P
27 1red ⊢ P ∈ ℕ 0 → 1 ∈ ℝ
28 ltle ⊢ 1 ∈ ℝ ∧ P ∈ ℝ → 1 < P → 1 ≤ P
29 27 20 28 syl2anc ⊢ P ∈ ℕ 0 → 1 < P → 1 ≤ P
30 26 29 syld ⊢ P ∈ ℕ 0 → 1 < P − 1 ∧ P − 1 < P → 1 ≤ P
31 21 30 mpan2d ⊢ P ∈ ℕ 0 → 1 < P − 1 → 1 ≤ P
32 31 imdistani ⊢ P ∈ ℕ 0 ∧ 1 < P − 1 → P ∈ ℕ 0 ∧ 1 ≤ P
33 elnnnn0c ⊢ P ∈ ℕ ↔ P ∈ ℕ 0 ∧ 1 ≤ P
34 32 33 sylibr ⊢ P ∈ ℕ 0 ∧ 1 < P − 1 → P ∈ ℕ
35 19 34 sylan ⊢ φ ∧ 1 < P − 1 → P ∈ ℕ
36 fzo0sn0fzo1 ⊢ P ∈ ℕ → 0 ..^ P = 0 ∪ 1 ..^ P
37 35 36 syl ⊢ φ ∧ 1 < P − 1 → 0 ..^ P = 0 ∪ 1 ..^ P
38 1zzd ⊢ φ ∧ 1 < P − 1 → 1 ∈ ℤ
39 1p1e2 ⊢ 1 + 1 = 2
40 2z ⊢ 2 ∈ ℤ
41 39 40 eqeltri ⊢ 1 + 1 ∈ ℤ
42 41 a1i ⊢ P ∈ ℕ 0 ∧ 1 < P − 1 → 1 + 1 ∈ ℤ
43 11 adantr ⊢ P ∈ ℕ 0 ∧ 1 < P − 1 → P ∈ ℤ
44 ltaddsub ⊢ 1 ∈ ℝ ∧ 1 ∈ ℝ ∧ P ∈ ℝ → 1 + 1 < P ↔ 1 < P − 1
45 44 bicomd ⊢ 1 ∈ ℝ ∧ 1 ∈ ℝ ∧ P ∈ ℝ → 1 < P − 1 ↔ 1 + 1 < P
46 22 27 20 45 mp3an2i ⊢ P ∈ ℕ 0 → 1 < P − 1 ↔ 1 + 1 < P
47 2re ⊢ 2 ∈ ℝ
48 39 47 eqeltri ⊢ 1 + 1 ∈ ℝ
49 ltle ⊢ 1 + 1 ∈ ℝ ∧ P ∈ ℝ → 1 + 1 < P → 1 + 1 ≤ P
50 48 20 49 sylancr ⊢ P ∈ ℕ 0 → 1 + 1 < P → 1 + 1 ≤ P
51 46 50 sylbid ⊢ P ∈ ℕ 0 → 1 < P − 1 → 1 + 1 ≤ P
52 51 imp ⊢ P ∈ ℕ 0 ∧ 1 < P − 1 → 1 + 1 ≤ P
53 eluz2 ⊢ P ∈ ℤ ≥ 1 + 1 ↔ 1 + 1 ∈ ℤ ∧ P ∈ ℤ ∧ 1 + 1 ≤ P
54 42 43 52 53 syl3anbrc ⊢ P ∈ ℕ 0 ∧ 1 < P − 1 → P ∈ ℤ ≥ 1 + 1
55 19 54 sylan ⊢ φ ∧ 1 < P − 1 → P ∈ ℤ ≥ 1 + 1
56 fzosplitsnm1 ⊢ 1 ∈ ℤ ∧ P ∈ ℤ ≥ 1 + 1 → 1 ..^ P = 1 ..^ P − 1 ∪ P − 1
57 38 55 56 syl2anc ⊢ φ ∧ 1 < P − 1 → 1 ..^ P = 1 ..^ P − 1 ∪ P − 1
58 57 uneq2d ⊢ φ ∧ 1 < P − 1 → 0 ∪ 1 ..^ P = 0 ∪ 1 ..^ P − 1 ∪ P − 1
59 37 58 eqtrd ⊢ φ ∧ 1 < P − 1 → 0 ..^ P = 0 ∪ 1 ..^ P − 1 ∪ P − 1
60 59 raleqdv ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ i ∈ 0 ∪ 1 ..^ P − 1 ∪ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
61 ralunb ⊢ ∀ i ∈ 0 ∪ 1 ..^ P − 1 ∪ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ i ∈ 0 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ 1 ..^ P − 1 ∪ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
62 ralunb ⊢ ∀ i ∈ 1 ..^ P − 1 ∪ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ i ∈ 1 ..^ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
63 62 anbi2i ⊢ ∀ i ∈ 0 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ 1 ..^ P − 1 ∪ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ i ∈ 0 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ 1 ..^ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
64 61 63 bitri ⊢ ∀ i ∈ 0 ∪ 1 ..^ P − 1 ∪ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ i ∈ 0 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ 1 ..^ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
65 60 64 bitrdi ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ i ∈ 0 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ 1 ..^ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
66 2 eqcomi ⊢ P − 1 = R
67 66 oveq2i ⊢ 1 ..^ P − 1 = 1 ..^ R
68 67 raleqi ⊢ ∀ i ∈ 1 ..^ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ↔ ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j
69 fvres ⊢ i ∈ 1 ..^ R → P ↾ 1 ..^ R ⁡ i = P ⁡ i
70 69 eqcomd ⊢ i ∈ 1 ..^ R → P ⁡ i = P ↾ 1 ..^ R ⁡ i
71 70 adantl ⊢ φ ∧ 1 < P − 1 ∧ i ∈ 1 ..^ R → P ⁡ i = P ↾ 1 ..^ R ⁡ i
72 71 adantr ⊢ φ ∧ 1 < P − 1 ∧ i ∈ 1 ..^ R ∧ j ∈ 1 ..^ R → P ⁡ i = P ↾ 1 ..^ R ⁡ i
73 fvres ⊢ j ∈ 1 ..^ R → P ↾ 1 ..^ R ⁡ j = P ⁡ j
74 73 eqcomd ⊢ j ∈ 1 ..^ R → P ⁡ j = P ↾ 1 ..^ R ⁡ j
75 74 adantl ⊢ φ ∧ 1 < P − 1 ∧ i ∈ 1 ..^ R ∧ j ∈ 1 ..^ R → P ⁡ j = P ↾ 1 ..^ R ⁡ j
76 72 75 neeq12d ⊢ φ ∧ 1 < P − 1 ∧ i ∈ 1 ..^ R ∧ j ∈ 1 ..^ R → P ⁡ i ≠ P ⁡ j ↔ P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
77 76 biimpd ⊢ φ ∧ 1 < P − 1 ∧ i ∈ 1 ..^ R ∧ j ∈ 1 ..^ R → P ⁡ i ≠ P ⁡ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
78 77 imim2d ⊢ φ ∧ 1 < P − 1 ∧ i ∈ 1 ..^ R ∧ j ∈ 1 ..^ R → i ≠ j → P ⁡ i ≠ P ⁡ j → i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
79 78 ralimdva ⊢ φ ∧ 1 < P − 1 ∧ i ∈ 1 ..^ R → ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j → ∀ j ∈ 1 ..^ R i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
80 79 ralimdva ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j → ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
81 68 80 biimtrid ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 1 ..^ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j → ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
82 81 adantrd ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 1 ..^ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j → ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
83 82 adantld ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 0 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ 1 ..^ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j ∧ ∀ i ∈ P − 1 ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j → ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
84 65 83 sylbid ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 0 ..^ P ∀ j ∈ 1 ..^ R i ≠ j → P ⁡ i ≠ P ⁡ j → ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
85 18 84 mpd ⊢ φ ∧ 1 < P − 1 → ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
86 dff14a ⊢ P ↾ 1 ..^ R : 1 ..^ R ⟶ 1-1 V ↔ P ↾ 1 ..^ R : 1 ..^ R ⟶ V ∧ ∀ i ∈ 1 ..^ R ∀ j ∈ 1 ..^ R i ≠ j → P ↾ 1 ..^ R ⁡ i ≠ P ↾ 1 ..^ R ⁡ j
87 17 85 86 sylanbrc ⊢ φ ∧ 1 < P − 1 → P ↾ 1 ..^ R : 1 ..^ R ⟶ 1-1 V
88 df-f1 ⊢ P ↾ 1 ..^ R : 1 ..^ R ⟶ 1-1 V ↔ P ↾ 1 ..^ R : 1 ..^ R ⟶ V ∧ Fun ⁡ P ↾ 1 ..^ R -1
89 87 88 sylib ⊢ φ ∧ 1 < P − 1 → P ↾ 1 ..^ R : 1 ..^ R ⟶ V ∧ Fun ⁡ P ↾ 1 ..^ R -1
90 89 simprd ⊢ φ ∧ 1 < P − 1 → Fun ⁡ P ↾ 1 ..^ R -1
91 funcnv0 ⊢ Fun ⁡ ∅ -1
92 19 nn0zd ⊢ φ → P ∈ ℤ
93 peano2zm ⊢ P ∈ ℤ → P − 1 ∈ ℤ
94 92 93 syl ⊢ φ → P − 1 ∈ ℤ
95 94 zred ⊢ φ → P − 1 ∈ ℝ
96 1red ⊢ φ → 1 ∈ ℝ
97 95 96 lenltd ⊢ φ → P − 1 ≤ 1 ↔ ¬ 1 < P − 1
98 97 biimpar ⊢ φ ∧ ¬ 1 < P − 1 → P − 1 ≤ 1
99 2 98 eqbrtrid ⊢ φ ∧ ¬ 1 < P − 1 → R ≤ 1
100 1zzd ⊢ φ → 1 ∈ ℤ
101 2 94 eqeltrid ⊢ φ → R ∈ ℤ
102 100 101 jca ⊢ φ → 1 ∈ ℤ ∧ R ∈ ℤ
103 102 adantr ⊢ φ ∧ ¬ 1 < P − 1 → 1 ∈ ℤ ∧ R ∈ ℤ
104 fzon ⊢ 1 ∈ ℤ ∧ R ∈ ℤ → R ≤ 1 ↔ 1 ..^ R = ∅
105 104 bicomd ⊢ 1 ∈ ℤ ∧ R ∈ ℤ → 1 ..^ R = ∅ ↔ R ≤ 1
106 103 105 syl ⊢ φ ∧ ¬ 1 < P − 1 → 1 ..^ R = ∅ ↔ R ≤ 1
107 99 106 mpbird ⊢ φ ∧ ¬ 1 < P − 1 → 1 ..^ R = ∅
108 107 reseq2d ⊢ φ ∧ ¬ 1 < P − 1 → P ↾ 1 ..^ R = P ↾ ∅
109 res0 ⊢ P ↾ ∅ = ∅
110 108 109 eqtrdi ⊢ φ ∧ ¬ 1 < P − 1 → P ↾ 1 ..^ R = ∅
111 110 cnveqd ⊢ φ ∧ ¬ 1 < P − 1 → P ↾ 1 ..^ R -1 = ∅ -1
112 111 funeqd ⊢ φ ∧ ¬ 1 < P − 1 → Fun ⁡ P ↾ 1 ..^ R -1 ↔ Fun ⁡ ∅ -1
113 91 112 mpbiri ⊢ φ ∧ ¬ 1 < P − 1 → Fun ⁡ P ↾ 1 ..^ R -1
114 90 113 pm2.61dan ⊢ φ → Fun ⁡ P ↾ 1 ..^ R -1