Metamath Proof Explorer

Theorem swrdnnn0nd

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

Ref Expression
Assertion swrdnnn0nd 
|- ( ( S e. Word V /\ -. ( F e. NN0 /\ L e. NN0 ) ) -> ( S substr <. F , L >. ) = (/) )

Proof

Step Hyp Ref Expression
1 ianor 
 |-  ( -. ( F e. NN0 /\ L e. NN0 ) <-> ( -. F e. NN0 \/ -. L e. NN0 ) )
2 ianor 
 |-  ( -. ( F e. ZZ /\ 0 <_ F ) <-> ( -. F e. ZZ \/ -. 0 <_ F ) )
3 elnn0z 
 |-  ( F e. NN0 <-> ( F e. ZZ /\ 0 <_ F ) )
4 2 3 xchnxbir 
 |-  ( -. F e. NN0 <-> ( -. F e. ZZ \/ -. 0 <_ F ) )
5 ianor 
 |-  ( -. ( L e. ZZ /\ 0 <_ L ) <-> ( -. L e. ZZ \/ -. 0 <_ L ) )
6 elnn0z 
 |-  ( L e. NN0 <-> ( L e. ZZ /\ 0 <_ L ) )
7 5 6 xchnxbir 
 |-  ( -. L e. NN0 <-> ( -. L e. ZZ \/ -. 0 <_ L ) )
8 4 7 orbi12i 
 |-  ( ( -. F e. NN0 \/ -. L e. NN0 ) <-> ( ( -. F e. ZZ \/ -. 0 <_ F ) \/ ( -. L e. ZZ \/ -. 0 <_ L ) ) )
9 or4 
 |-  ( ( ( -. F e. ZZ \/ -. 0 <_ F ) \/ ( -. L e. ZZ \/ -. 0 <_ L ) ) <-> ( ( -. F e. ZZ \/ -. L e. ZZ ) \/ ( -. 0 <_ F \/ -. 0 <_ L ) ) )
10 ianor 
 |-  ( -. ( F e. ZZ /\ L e. ZZ ) <-> ( -. F e. ZZ \/ -. L e. ZZ ) )
11 10 bicomi 
 |-  ( ( -. F e. ZZ \/ -. L e. ZZ ) <-> -. ( F e. ZZ /\ L e. ZZ ) )
12 11 orbi1i 
 |-  ( ( ( -. F e. ZZ \/ -. L e. ZZ ) \/ ( -. 0 <_ F \/ -. 0 <_ L ) ) <-> ( -. ( F e. ZZ /\ L e. ZZ ) \/ ( -. 0 <_ F \/ -. 0 <_ L ) ) )
13 9 12 bitri 
 |-  ( ( ( -. F e. ZZ \/ -. 0 <_ F ) \/ ( -. L e. ZZ \/ -. 0 <_ L ) ) <-> ( -. ( F e. ZZ /\ L e. ZZ ) \/ ( -. 0 <_ F \/ -. 0 <_ L ) ) )
14 8 13 bitri 
 |-  ( ( -. F e. NN0 \/ -. L e. NN0 ) <-> ( -. ( F e. ZZ /\ L e. ZZ ) \/ ( -. 0 <_ F \/ -. 0 <_ L ) ) )
15 1 14 bitri 
 |-  ( -. ( F e. NN0 /\ L e. NN0 ) <-> ( -. ( F e. ZZ /\ L e. ZZ ) \/ ( -. 0 <_ F \/ -. 0 <_ L ) ) )
16 swrdnznd 
 |-  ( -. ( F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) = (/) )
17 16 a1d 
 |-  ( -. ( F e. ZZ /\ L e. ZZ ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
18 notnotb 
 |-  ( ( F e. ZZ /\ L e. ZZ ) <-> -. -. ( F e. ZZ /\ L e. ZZ ) )
19 zre 
 |-  ( F e. ZZ -> F e. RR )
20 0red 
 |-  ( F e. ZZ -> 0 e. RR )
21 19 20 jca 
 |-  ( F e. ZZ -> ( F e. RR /\ 0 e. RR ) )
22 21 3ad2ant2 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F e. RR /\ 0 e. RR ) )
23 ltnle 
 |-  ( ( F e. RR /\ 0 e. RR ) -> ( F < 0 <-> -. 0 <_ F ) )
24 22 23 syl 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F < 0 <-> -. 0 <_ F ) )
25 orc 
 |-  ( F < 0 -> ( F < 0 \/ L <_ F ) )
26 24 25 biimtrrdi 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( -. 0 <_ F -> ( F < 0 \/ L <_ F ) ) )
27 26 com12 
 |-  ( -. 0 <_ F -> ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F < 0 \/ L <_ F ) ) )
28 notnotb 
 |-  ( 0 <_ F <-> -. -. 0 <_ F )
29 28 a1i 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( 0 <_ F <-> -. -. 0 <_ F ) )
30 zre 
 |-  ( L e. ZZ -> L e. RR )
31 0red 
 |-  ( L e. ZZ -> 0 e. RR )
32 30 31 jca 
 |-  ( L e. ZZ -> ( L e. RR /\ 0 e. RR ) )
33 32 3ad2ant3 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( L e. RR /\ 0 e. RR ) )
34 ltnle 
 |-  ( ( L e. RR /\ 0 e. RR ) -> ( L < 0 <-> -. 0 <_ L ) )
35 33 34 syl 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( L < 0 <-> -. 0 <_ L ) )
36 29 35 anbi12d 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( 0 <_ F /\ L < 0 ) <-> ( -. -. 0 <_ F /\ -. 0 <_ L ) ) )
37 30 3ad2ant3 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> L e. RR )
38 0red 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> 0 e. RR )
39 19 3ad2ant2 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> F e. RR )
40 ltleletr 
 |-  ( ( L e. RR /\ 0 e. RR /\ F e. RR ) -> ( ( L < 0 /\ 0 <_ F ) -> L <_ F ) )
41 37 38 39 40 syl3anc 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( L < 0 /\ 0 <_ F ) -> L <_ F ) )
42 olc 
 |-  ( L <_ F -> ( F < 0 \/ L <_ F ) )
43 41 42 syl6 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( L < 0 /\ 0 <_ F ) -> ( F < 0 \/ L <_ F ) ) )
44 43 ancomsd 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( 0 <_ F /\ L < 0 ) -> ( F < 0 \/ L <_ F ) ) )
45 36 44 sylbird 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( -. -. 0 <_ F /\ -. 0 <_ L ) -> ( F < 0 \/ L <_ F ) ) )
46 45 com12 
 |-  ( ( -. -. 0 <_ F /\ -. 0 <_ L ) -> ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F < 0 \/ L <_ F ) ) )
47 27 46 jaoi3 
 |-  ( ( -. 0 <_ F \/ -. 0 <_ L ) -> ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F < 0 \/ L <_ F ) ) )
48 47 impcom 
 |-  ( ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ ( -. 0 <_ F \/ -. 0 <_ L ) ) -> ( F < 0 \/ L <_ F ) )
49 48 orcd 
 |-  ( ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ ( -. 0 <_ F \/ -. 0 <_ L ) ) -> ( ( F < 0 \/ L <_ F ) \/ ( # ` S ) < L ) )
50 df-3or 
 |-  ( ( F < 0 \/ L <_ F \/ ( # ` S ) < L ) <-> ( ( F < 0 \/ L <_ F ) \/ ( # ` S ) < L ) )
51 49 50 sylibr 
 |-  ( ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ ( -. 0 <_ F \/ -. 0 <_ L ) ) -> ( F < 0 \/ L <_ F \/ ( # ` S ) < L ) )
52 swrdnd 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( F < 0 \/ L <_ F \/ ( # ` S ) < L ) -> ( S substr <. F , L >. ) = (/) ) )
53 52 imp 
 |-  ( ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ ( F < 0 \/ L <_ F \/ ( # ` S ) < L ) ) -> ( S substr <. F , L >. ) = (/) )
54 51 53 syldan 
 |-  ( ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ ( -. 0 <_ F \/ -. 0 <_ L ) ) -> ( S substr <. F , L >. ) = (/) )
55 54 ex 
 |-  ( ( S e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( -. 0 <_ F \/ -. 0 <_ L ) -> ( S substr <. F , L >. ) = (/) ) )
56 55 3expb 
 |-  ( ( S e. Word V /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( ( -. 0 <_ F \/ -. 0 <_ L ) -> ( S substr <. F , L >. ) = (/) ) )
57 56 expcom 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( S e. Word V -> ( ( -. 0 <_ F \/ -. 0 <_ L ) -> ( S substr <. F , L >. ) = (/) ) ) )
58 57 com23 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( ( -. 0 <_ F \/ -. 0 <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
59 18 58 sylbir 
 |-  ( -. -. ( F e. ZZ /\ L e. ZZ ) -> ( ( -. 0 <_ F \/ -. 0 <_ L ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) ) )
60 59 imp 
 |-  ( ( -. -. ( F e. ZZ /\ L e. ZZ ) /\ ( -. 0 <_ F \/ -. 0 <_ L ) ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
61 17 60 jaoi3 
 |-  ( ( -. ( F e. ZZ /\ L e. ZZ ) \/ ( -. 0 <_ F \/ -. 0 <_ L ) ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
62 15 61 sylbi 
 |-  ( -. ( F e. NN0 /\ L e. NN0 ) -> ( S e. Word V -> ( S substr <. F , L >. ) = (/) ) )
63 62 impcom 
 |-  ( ( S e. Word V /\ -. ( F e. NN0 /\ L e. NN0 ) ) -> ( S substr <. F , L >. ) = (/) )