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