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