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∈WordV
pthd.r ⊢R=P−1
pthd.s ⊢φ→∀i∈0..^P∀j∈1..^Ri≠j→P⁡i≠P⁡j
Assertion pthdlem1 ⊢φ→Fun⁡P↾1..^R-1

Proof

Step Hyp Ref Expression
1 pthd.p ⊢φ→P∈WordV
2 pthd.r ⊢R=P−1
3 pthd.s ⊢φ→∀i∈0..^P∀j∈1..^Ri≠j→P⁡i≠P⁡j
4 wrdf ⊢P∈WordV→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∈WordV→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..^Ri≠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..^Ri≠j→P⁡i≠P⁡j↔∀i∈0∪1..^P−1∪P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j
61 ralunb ⊢∀i∈0∪1..^P−1∪P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j↔∀i∈0∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈1..^P−1∪P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j
62 ralunb ⊢∀i∈1..^P−1∪P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j↔∀i∈1..^P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j
63 62 anbi2i ⊢∀i∈0∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈1..^P−1∪P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j↔∀i∈0∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈1..^P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j
64 61 63 bitri ⊢∀i∈0∪1..^P−1∪P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j↔∀i∈0∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈1..^P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j
65 60 64 bitrdi ⊢φ∧1<P−1→∀i∈0..^P∀j∈1..^Ri≠j→P⁡i≠P⁡j↔∀i∈0∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈1..^P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈P−1∀j∈1..^Ri≠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..^Ri≠j→P⁡i≠P⁡j↔∀i∈1..^R∀j∈1..^Ri≠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..^Ri≠j→P⁡i≠P⁡j→∀j∈1..^Ri≠j→P↾1..^R⁡i≠P↾1..^R⁡j
80 79 ralimdva ⊢φ∧1<P−1→∀i∈1..^R∀j∈1..^Ri≠j→P⁡i≠P⁡j→∀i∈1..^R∀j∈1..^Ri≠j→P↾1..^R⁡i≠P↾1..^R⁡j
81 68 80 syl5bi ⊢φ∧1<P−1→∀i∈1..^P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j→∀i∈1..^R∀j∈1..^Ri≠j→P↾1..^R⁡i≠P↾1..^R⁡j
82 81 adantrd ⊢φ∧1<P−1→∀i∈1..^P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j→∀i∈1..^R∀j∈1..^Ri≠j→P↾1..^R⁡i≠P↾1..^R⁡j
83 82 adantld ⊢φ∧1<P−1→∀i∈0∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈1..^P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j∧∀i∈P−1∀j∈1..^Ri≠j→P⁡i≠P⁡j→∀i∈1..^R∀j∈1..^Ri≠j→P↾1..^R⁡i≠P↾1..^R⁡j
84 65 83 sylbid ⊢φ∧1<P−1→∀i∈0..^P∀j∈1..^Ri≠j→P⁡i≠P⁡j→∀i∈1..^R∀j∈1..^Ri≠j→P↾1..^R⁡i≠P↾1..^R⁡j
85 18 84 mpd ⊢φ∧1<P−1→∀i∈1..^R∀j∈1..^Ri≠j→P↾1..^R⁡i≠P↾1..^R⁡j
86 dff14a ⊢P↾1..^R:1..^R⟶1-1V↔P↾1..^R:1..^R⟶V∧∀i∈1..^R∀j∈1..^Ri≠j→P↾1..^R⁡i≠P↾1..^R⁡j
87 17 85 86 sylanbrc ⊢φ∧1<P−1→P↾1..^R:1..^R⟶1-1V
88 df-f1 ⊢P↾1..^R:1..^R⟶1-1V↔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