Metamath Proof Explorer

Theorem swrdnd0

Description: The value of a subword operation for inproper arguments is the empty set. (Contributed by AV, 2-Dec-2022)

Ref Expression
Assertion swrdnd0 
|- ( S e. Word V -> ( -. ( F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) = (/) ) )

Proof

Step Hyp Ref Expression
1 ianor 
 |-  ( -. ( F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) <-> ( -. F e. ( 0 ... L ) \/ -. L e. ( 0 ... ( # ` S ) ) ) )
2 3ianor 
 |-  ( -. ( F e. NN0 /\ L e. NN0 /\ F <_ L ) <-> ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) )
3 elfz2nn0 
 |-  ( F e. ( 0 ... L ) <-> ( F e. NN0 /\ L e. NN0 /\ F <_ L ) )
4 2 3 xchnxbir 
 |-  ( -. F e. ( 0 ... L ) <-> ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) )
5 3ianor 
 |-  ( -. ( L e. NN0 /\ ( # ` S ) e. NN0 /\ L <_ ( # ` S ) ) <-> ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) )
6 elfz2nn0 
 |-  ( L e. ( 0 ... ( # ` S ) ) <-> ( L e. NN0 /\ ( # ` S ) e. NN0 /\ L <_ ( # ` S ) ) )
7 5 6 xchnxbir 
 |-  ( -. L e. ( 0 ... ( # ` S ) ) <-> ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) )
8 4 7 orbi12i 
 |-  ( ( -. F e. ( 0 ... L ) \/ -. L e. ( 0 ... ( # ` S ) ) ) <-> ( ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) \/ ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) ) )
9 1 8 bitri 
 |-  ( -. ( F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) <-> ( ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) \/ ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) ) )
10 df-3or 
 |-  ( ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) <-> ( ( -. F e. NN0 \/ -. L e. NN0 ) \/ -. F <_ L ) )
11 ianor 
 |-  ( -. ( F e. NN0 /\ L e. NN0 ) <-> ( -. F e. NN0 \/ -. L e. NN0 ) )
12 swrdnnn0nd 
 |-  ( ( S e. Word V /\ -. ( F e. NN0 /\ L e. NN0 ) ) -> ( S substr <. F , L >. ) = (/) )
13 12 expcom 
 |-  ( -. ( F e. NN0 /\ L e. NN0 ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
14 11 13 sylbir 
 |-  ( ( -. F e. NN0 \/ -. L e. NN0 ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
15 anor 
 |-  ( ( F e. NN0 /\ L e. NN0 ) <-> -. ( -. F e. NN0 \/ -. L e. NN0 ) )
16 nn0re 
 |-  ( L e. NN0 -> L e. RR )
17 nn0re 
 |-  ( F e. NN0 -> F e. RR )
18 ltnle 
 |-  ( ( L e. RR /\ F e. RR ) -> ( L < F <-> -. F <_ L ) )
19 16 17 18 syl2anr 
 |-  ( ( F e. NN0 /\ L e. NN0 ) -> ( L < F <-> -. F <_ L ) )
20 nn0z 
 |-  ( F e. NN0 -> F e. ZZ )
21 nn0z 
 |-  ( L e. NN0 -> L e. ZZ )
22 20 21 anim12i 
 |-  ( ( F e. NN0 /\ L e. NN0 ) -> ( F e. ZZ /\ L e. ZZ ) )
23 22 anim2i 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) -> ( S e. Word V /\ ( F e. ZZ /\ L e. ZZ ) ) )
24 3anass 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) <-> ( S e. Word V /\ ( F e. ZZ /\ L e. ZZ ) ) )
25 23 24 sylibr 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) -> ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) )
26 25 adantr 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) /\ L < F ) -> ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) )
27 17 16 anim12ci 
 |-  ( ( F e. NN0 /\ L e. NN0 ) -> ( L e. RR /\ F e. RR ) )
28 27 adantl 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) -> ( L e. RR /\ F e. RR ) )
29 ltle 
 |-  ( ( L e. RR /\ F e. RR ) -> ( L < F -> L <_ F ) )
30 28 29 syl 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) -> ( L < F -> L <_ F ) )
31 30 imp 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) /\ L < F ) -> L <_ F )
32 31 3mix2d 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) /\ L < F ) -> ( F < 0 \/ L <_ F \/ ( # ` S ) < L ) )
33 swrdnd 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( F < 0 \/ L <_ F \/ ( # ` S ) < L ) -> ( S substr <. F , L >. ) = (/) ) )
34 26 32 33 sylc 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) /\ L < F ) -> ( S substr <. F , L >. ) = (/) )
35 34 ex 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. NN0 ) ) -> ( L < F -> ( S substr <. F , L >. ) = (/) ) )
36 35 expcom 
 |-  ( ( F e. NN0 /\ L e. NN0 ) -> ( S e. Word V -> ( L < F -> ( S substr <. F , L >. ) = (/) ) ) )
37 36 com23 
 |-  ( ( F e. NN0 /\ L e. NN0 ) -> ( L < F -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
38 19 37 sylbird 
 |-  ( ( F e. NN0 /\ L e. NN0 ) -> ( -. F <_ L -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
39 15 38 sylbir 
 |-  ( -. ( -. F e. NN0 \/ -. L e. NN0 ) -> ( -. F <_ L -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
40 39 imp 
 |-  ( ( -. ( -. F e. NN0 \/ -. L e. NN0 ) /\ -. F <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
41 14 40 jaoi3 
 |-  ( ( ( -. F e. NN0 \/ -. L e. NN0 ) \/ -. F <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
42 10 41 sylbi 
 |-  ( ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
43 3anor 
 |-  ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) <-> -. ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) )
44 pm2.24 
 |-  ( L e. NN0 -> ( -. L e. NN0 -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
45 44 3ad2ant2 
 |-  ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) -> ( -. L e. NN0 -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
46 45 com12 
 |-  ( -. L e. NN0 -> ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
47 pm2.24 
 |-  ( ( # ` S ) e. NN0 -> ( -. ( # ` S ) e. NN0 -> ( S substr <. F , L >. ) = (/) ) )
48 lencl 
 |-  ( S e. Word V -> ( # ` S ) e. NN0 )
49 47 48 syl11 
 |-  ( -. ( # ` S ) e. NN0 -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
50 49 a1d 
 |-  ( -. ( # ` S ) e. NN0 -> ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
51 48 nn0red 
 |-  ( S e. Word V -> ( # ` S ) e. RR )
52 16 3ad2ant2 
 |-  ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) -> L e. RR )
53 ltnle 
 |-  ( ( ( # ` S ) e. RR /\ L e. RR ) -> ( ( # ` S ) < L <-> -. L <_ ( # ` S ) ) )
54 51 52 53 syl2anr 
 |-  ( ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) /\ S e. Word V ) -> ( ( # ` S ) < L <-> -. L <_ ( # ` S ) ) )
55 simpr 
 |-  ( ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) /\ S e. Word V ) -> S e. Word V )
56 20 3ad2ant1 
 |-  ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) -> F e. ZZ )
57 56 adantr 
 |-  ( ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) /\ S e. Word V ) -> F e. ZZ )
58 21 3ad2ant2 
 |-  ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) -> L e. ZZ )
59 58 adantr 
 |-  ( ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) /\ S e. Word V ) -> L e. ZZ )
60 55 57 59 3jca 
 |-  ( ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) /\ S e. Word V ) -> ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) )
61 3mix3 
 |-  ( ( # ` S ) < L -> ( F < 0 \/ L <_ F \/ ( # ` S ) < L ) )
62 60 61 33 syl2im 
 |-  ( ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) /\ S e. Word V ) -> ( ( # ` S ) < L -> ( S substr <. F , L >. ) = (/) ) )
63 54 62 sylbird 
 |-  ( ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) /\ S e. Word V ) -> ( -. L <_ ( # ` S ) -> ( S substr <. F , L >. ) = (/) ) )
64 63 com12 
 |-  ( -. L <_ ( # ` S ) -> ( ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) /\ S e. Word V ) -> ( S substr <. F , L >. ) = (/) ) )
65 64 expd 
 |-  ( -. L <_ ( # ` S ) -> ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
66 46 50 65 3jaoi 
 |-  ( ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) -> ( ( F e. NN0 /\ L e. NN0 /\ F <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
67 43 66 syl5bir 
 |-  ( ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) -> ( -. ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
68 67 impcom 
 |-  ( ( -. ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) /\ ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
69 42 68 jaoi3 
 |-  ( ( ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) \/ ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
70 69 com12 
 |-  ( S e. Word V -> ( ( ( -. F e. NN0 \/ -. L e. NN0 \/ -. F <_ L ) \/ ( -. L e. NN0 \/ -. ( # ` S ) e. NN0 \/ -. L <_ ( # ` S ) ) ) -> ( S substr <. F , L >. ) = (/) ) )
71 9 70 syl5bi 
 |-  ( S e. Word V -> ( -. ( F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) = (/) ) )