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 syl5ibr 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 syl6bi 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 syl5ibr 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 syl5ibr 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 syl5ibr 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 syl6ib φ 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 syl5bi φ 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