repswswrd

Description: A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption N <_ L is required, because otherwise ( L < N ) : ( ( S repeatS L ) substr <. M , N >. ) = (/) , but for M < N ( S repeatS ( N - M ) ) ) =/= (/) ! The proof is relatively long because the border cases ( M = N , -. ( M ..^ N ) C_ ( 0 ..^ L ) must have been considered. (Contributed by AV, 6-Nov-2018)

		Ref	Expression
	Assertion	repswswrd	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (S repeatS L) substr ⟨M, N⟩ = S repeatS (N - M)$

Proof

Step	Hyp	Ref	Expression
1		repsw	$⊢ (S \in V \land L \in ℕ_{0}) \to S repeatS L \in Word V$
2		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
3		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
4	2 3	anim12i	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \in ℤ \land N \in ℤ)$
5	1 4	anim12i	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (S repeatS L \in Word V \land (M \in ℤ \land N \in ℤ))$
6		3anass	$⊢ (S repeatS L \in Word V \land M \in ℤ \land N \in ℤ) \leftrightarrow (S repeatS L \in Word V \land (M \in ℤ \land N \in ℤ))$
7	5 6	sylibr	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (S repeatS L \in Word V \land M \in ℤ \land N \in ℤ)$
8	7	3adant3	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (S repeatS L \in Word V \land M \in ℤ \land N \in ℤ)$
9		swrdval	$⊢ (S repeatS L \in Word V \land M \in ℤ \land N \in ℤ) \to (S repeatS L) substr ⟨M, N⟩ = if ((M ..^N) \subseteq dom (S repeatS L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset)$
10	8 9	syl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (S repeatS L) substr ⟨M, N⟩ = if ((M ..^N) \subseteq dom (S repeatS L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset)$
11		repsf	$⊢ (S \in V \land L \in ℕ_{0}) \to (S repeatS L) : (0 ..^L) ⟶ V$
12	11	3ad2ant1	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (S repeatS L) : (0 ..^L) ⟶ V$
13	12	fdmd	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to dom (S repeatS L) = (0 ..^L)$
14	13	sseq2d	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to ((M ..^N) \subseteq dom (S repeatS L) \leftrightarrow (M ..^N) \subseteq (0 ..^L))$
15	14	ifbid	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to if ((M ..^N) \subseteq dom (S repeatS L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset)$
16		fzon	$⊢ (M \in ℤ \land N \in ℤ) \to (N \leq M \leftrightarrow (M ..^N) = \emptyset)$
17	4 16	syl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \leq M \leftrightarrow (M ..^N) = \emptyset)$
18	17	adantl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \leq M \leftrightarrow (M ..^N) = \emptyset)$
19	18	biimpac	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (M ..^N) = \emptyset$
20		0ss	$⊢ \emptyset \subseteq (0 ..^L)$
21	19 20	eqsstrdi	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (M ..^N) \subseteq (0 ..^L)$
22		iftrue	$⊢ (M ..^N) \subseteq (0 ..^L) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M))$
23	21 22	syl	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M))$
24		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
25		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
26	24 25	anim12ci	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \in ℝ \land M \in ℝ)$
27	26	adantl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \in ℝ \land M \in ℝ)$
28		suble0	$⊢ (N \in ℝ \land M \in ℝ) \to (N - M \leq 0 \leftrightarrow N \leq M)$
29	27 28	syl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N - M \leq 0 \leftrightarrow N \leq M)$
30	29	biimparc	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to N - M \leq 0$
31		0z	$⊢ 0 \in ℤ$
32		zsubcl	$⊢ (N \in ℤ \land M \in ℤ) \to N - M \in ℤ$
33	3 2 32	syl2anr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N - M \in ℤ$
34	33	adantl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to N - M \in ℤ$
35	34	adantl	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to N - M \in ℤ$
36		fzon	$⊢ (0 \in ℤ \land N - M \in ℤ) \to (N - M \leq 0 \leftrightarrow (0 ..^N - M) = \emptyset)$
37	31 35 36	sylancr	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (N - M \leq 0 \leftrightarrow (0 ..^N - M) = \emptyset)$
38	30 37	mpbid	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (0 ..^N - M) = \emptyset$
39	38	mpteq1d	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)) = (x \in \emptyset ⟼ (S repeatS L) (x + M))$
40		mpt0	$⊢ (x \in \emptyset ⟼ (S repeatS L) (x + M)) = \emptyset$
41		oveq2	$⊢ M = N \to N - M = N - N$
42	41	oveq2d	$⊢ M = N \to S repeatS (N - M) = S repeatS (N - N)$
43		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
44	43	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℂ$
45	44	subidd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N - N = 0$
46	45	adantl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to N - N = 0$
47	46	oveq2d	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to S repeatS (N - N) = S repeatS 0$
48		repsw0	$⊢ S \in V \to S repeatS 0 = \emptyset$
49	48	ad2antrr	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to S repeatS 0 = \emptyset$
50	47 49	eqtrd	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to S repeatS (N - N) = \emptyset$
51	42 50	sylan9eqr	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \land M = N) \to S repeatS (N - M) = \emptyset$
52	51	ex	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (M = N \to S repeatS (N - M) = \emptyset)$
53	52	adantl	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (M = N \to S repeatS (N - M) = \emptyset)$
54	53	com12	$⊢ M = N \to ((N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to S repeatS (N - M) = \emptyset)$
55		elnn0z	$⊢ N - M \in ℕ_{0} \leftrightarrow (N - M \in ℤ \land 0 \leq N - M)$
56		subge0	$⊢ (N \in ℝ \land M \in ℝ) \to (0 \leq N - M \leftrightarrow M \leq N)$
57	25 24 56	syl2anr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (0 \leq N - M \leftrightarrow M \leq N)$
58	24 25	anim12i	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \in ℝ \land N \in ℝ)$
59		letri3	$⊢ (M \in ℝ \land N \in ℝ) \to (M = N \leftrightarrow (M \leq N \land N \leq M))$
60	58 59	syl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M = N \leftrightarrow (M \leq N \land N \leq M))$
61	60	biimprd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((M \leq N \land N \leq M) \to M = N)$
62	61	expd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \leq N \to (N \leq M \to M = N))$
63	57 62	sylbid	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (0 \leq N - M \to (N \leq M \to M = N))$
64	63	com23	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \leq M \to (0 \leq N - M \to M = N))$
65	64	adantl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \leq M \to (0 \leq N - M \to M = N))$
66	65	impcom	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (0 \leq N - M \to M = N)$
67	66	com12	$⊢ 0 \leq N - M \to ((N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to M = N)$
68	55 67	simplbiim	$⊢ N - M \in ℕ_{0} \to ((N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to M = N)$
69	68	com12	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (N - M \in ℕ_{0} \to M = N)$
70	69	con3d	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (\neg M = N \to \neg N - M \in ℕ_{0})$
71	70	impcom	$⊢ (\neg M = N \land (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})))) \to \neg N - M \in ℕ_{0}$
72		df-nel	$⊢ (N - M) \notin ℕ_{0} \leftrightarrow \neg N - M \in ℕ_{0}$
73	71 72	sylibr	$⊢ (\neg M = N \land (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})))) \to (N - M) \notin ℕ_{0}$
74		repsundef	$⊢ (N - M) \notin ℕ_{0} \to S repeatS (N - M) = \emptyset$
75	73 74	syl	$⊢ (\neg M = N \land (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})))) \to S repeatS (N - M) = \emptyset$
76	75	ex	$⊢ \neg M = N \to ((N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to S repeatS (N - M) = \emptyset)$
77	54 76	pm2.61i	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to S repeatS (N - M) = \emptyset$
78	40 77	eqtr4id	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (x \in \emptyset ⟼ (S repeatS L) (x + M)) = S repeatS (N - M)$
79	23 39 78	3eqtrd	$⊢ (N \leq M \land ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M)$
80	79	expcom	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \leq M \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M))$
81	80	3adant3	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (N \leq M \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M))$
82		ltnle	$⊢ (M \in ℝ \land N \in ℝ) \to (M < N \leftrightarrow \neg N \leq M)$
83	58 82	syl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M < N \leftrightarrow \neg N \leq M)$
84	83	bicomd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (\neg N \leq M \leftrightarrow M < N)$
85	84	3ad2ant2	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (\neg N \leq M \leftrightarrow M < N)$
86	22	adantr	$⊢ ((M ..^N) \subseteq (0 ..^L) \land (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N)) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M))$
87	4	3ad2ant2	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (M \in ℤ \land N \in ℤ)$
88	87	adantr	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to (M \in ℤ \land N \in ℤ)$
89		0zd	$⊢ S \in V \to 0 \in ℤ$
90		nn0z	$⊢ L \in ℕ_{0} \to L \in ℤ$
91	89 90	anim12i	$⊢ (S \in V \land L \in ℕ_{0}) \to (0 \in ℤ \land L \in ℤ)$
92	91	3ad2ant1	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (0 \in ℤ \land L \in ℤ)$
93	92	adantr	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to (0 \in ℤ \land L \in ℤ)$
94		simpr	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to M < N$
95		ssfzo12bi	$⊢ ((M \in ℤ \land N \in ℤ) \land (0 \in ℤ \land L \in ℤ) \land M < N) \to ((M ..^N) \subseteq (0 ..^L) \leftrightarrow (0 \leq M \land N \leq L))$
96	88 93 94 95	syl3anc	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to ((M ..^N) \subseteq (0 ..^L) \leftrightarrow (0 \leq M \land N \leq L))$
97		simpl1l	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to S \in V$
98	97	ad2antrr	$⊢ (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \land x \in (0 ..^N - M)) \to S \in V$
99		simpl1r	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to L \in ℕ_{0}$
100	99	ad2antrr	$⊢ (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \land x \in (0 ..^N - M)) \to L \in ℕ_{0}$
101		nn0addcl	$⊢ (x \in ℕ_{0} \land M \in ℕ_{0}) \to x + M \in ℕ_{0}$
102	101	expcom	$⊢ M \in ℕ_{0} \to (x \in ℕ_{0} \to x + M \in ℕ_{0})$
103	102	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (x \in ℕ_{0} \to x + M \in ℕ_{0})$
104	103	3ad2ant2	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (x \in ℕ_{0} \to x + M \in ℕ_{0})$
105	104	ad2antrr	$⊢ ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to (x \in ℕ_{0} \to x + M \in ℕ_{0})$
106		elfzonn0	$⊢ x \in (0 ..^N - M) \to x \in ℕ_{0}$
107	105 106	impel	$⊢ (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \land x \in (0 ..^N - M)) \to x + M \in ℕ_{0}$
108	90	adantl	$⊢ (S \in V \land L \in ℕ_{0}) \to L \in ℤ$
109	108	3ad2ant1	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to L \in ℤ$
110	109	adantr	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to L \in ℤ$
111		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
112	111	adantl	$⊢ (S \in V \land L \in ℕ_{0}) \to L \in ℝ$
113	112 58	anim12ci	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to ((M \in ℝ \land N \in ℝ) \land L \in ℝ)$
114		df-3an	$⊢ (M \in ℝ \land N \in ℝ \land L \in ℝ) \leftrightarrow ((M \in ℝ \land N \in ℝ) \land L \in ℝ)$
115	113 114	sylibr	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (M \in ℝ \land N \in ℝ \land L \in ℝ)$
116		ltletr	$⊢ (M \in ℝ \land N \in ℝ \land L \in ℝ) \to ((M < N \land N \leq L) \to M < L)$
117	115 116	syl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to ((M < N \land N \leq L) \to M < L)$
118		elnn0z	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℤ \land 0 \leq M)$
119		0red	$⊢ (M \in ℤ \land (S \in V \land L \in ℕ_{0})) \to 0 \in ℝ$
120		zre	$⊢ M \in ℤ \to M \in ℝ$
121	120	adantr	$⊢ (M \in ℤ \land (S \in V \land L \in ℕ_{0})) \to M \in ℝ$
122	112	adantl	$⊢ (M \in ℤ \land (S \in V \land L \in ℕ_{0})) \to L \in ℝ$
123		lelttr	$⊢ (0 \in ℝ \land M \in ℝ \land L \in ℝ) \to ((0 \leq M \land M < L) \to 0 < L)$
124	119 121 122 123	syl3anc	$⊢ (M \in ℤ \land (S \in V \land L \in ℕ_{0})) \to ((0 \leq M \land M < L) \to 0 < L)$
125	124	expd	$⊢ (M \in ℤ \land (S \in V \land L \in ℕ_{0})) \to (0 \leq M \to (M < L \to 0 < L))$
126	125	impancom	$⊢ (M \in ℤ \land 0 \leq M) \to ((S \in V \land L \in ℕ_{0}) \to (M < L \to 0 < L))$
127	118 126	sylbi	$⊢ M \in ℕ_{0} \to ((S \in V \land L \in ℕ_{0}) \to (M < L \to 0 < L))$
128	127	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to ((S \in V \land L \in ℕ_{0}) \to (M < L \to 0 < L))$
129	128	impcom	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (M < L \to 0 < L)$
130	117 129	syld	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to ((M < N \land N \leq L) \to 0 < L)$
131	130	expcomd	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \leq L \to (M < N \to 0 < L))$
132	131	3impia	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (M < N \to 0 < L)$
133	132	imp	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to 0 < L$
134		elnnz	$⊢ L \in ℕ \leftrightarrow (L \in ℤ \land 0 < L)$
135	110 133 134	sylanbrc	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to L \in ℕ$
136	135	ad2antrr	$⊢ (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \land x \in (0 ..^N - M)) \to L \in ℕ$
137		elfzo0	$⊢ x \in (0 ..^N - M) \leftrightarrow (x \in ℕ_{0} \land N - M \in ℕ \land x < N - M)$
138		nn0readdcl	$⊢ (x \in ℕ_{0} \land M \in ℕ_{0}) \to x + M \in ℝ$
139	138	expcom	$⊢ M \in ℕ_{0} \to (x \in ℕ_{0} \to x + M \in ℝ)$
140	139	ad2antrl	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (x \in ℕ_{0} \to x + M \in ℝ)$
141	140	impcom	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to x + M \in ℝ$
142	25	adantl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℝ$
143	142	adantl	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to N \in ℝ$
144	143	adantl	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to N \in ℝ$
145	111	ad2antrl	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to L \in ℝ$
146	141 144 145	3jca	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (x + M \in ℝ \land N \in ℝ \land L \in ℝ)$
147	146	ex	$⊢ x \in ℕ_{0} \to ((L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (x + M \in ℝ \land N \in ℝ \land L \in ℝ))$
148	147	adantr	$⊢ (x \in ℕ_{0} \land x < N - M) \to ((L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (x + M \in ℝ \land N \in ℝ \land L \in ℝ))$
149	148	impcom	$⊢ ((L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \land (x \in ℕ_{0} \land x < N - M)) \to (x + M \in ℝ \land N \in ℝ \land L \in ℝ)$
150	149	adantr	$⊢ (((L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \land (x \in ℕ_{0} \land x < N - M)) \land N \leq L) \to (x + M \in ℝ \land N \in ℝ \land L \in ℝ)$
151		nn0re	$⊢ x \in ℕ_{0} \to x \in ℝ$
152	151	adantr	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to x \in ℝ$
153	24	ad2antrl	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to M \in ℝ$
154	153	adantl	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to M \in ℝ$
155	152 154 144	ltaddsubd	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (x + M < N \leftrightarrow x < N - M)$
156		idd	$⊢ ((x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \land N \leq L) \to (x + M < N \to x + M < N)$
157	156	ex	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (N \leq L \to (x + M < N \to x + M < N))$
158	157	com23	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (x + M < N \to (N \leq L \to x + M < N))$
159	155 158	sylbird	$⊢ (x \in ℕ_{0} \land (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to (x < N - M \to (N \leq L \to x + M < N))$
160	159	impancom	$⊢ (x \in ℕ_{0} \land x < N - M) \to ((L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \leq L \to x + M < N))$
161	160	impcom	$⊢ ((L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \land (x \in ℕ_{0} \land x < N - M)) \to (N \leq L \to x + M < N)$
162	161	impac	$⊢ (((L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \land (x \in ℕ_{0} \land x < N - M)) \land N \leq L) \to (x + M < N \land N \leq L)$
163		ltletr	$⊢ (x + M \in ℝ \land N \in ℝ \land L \in ℝ) \to ((x + M < N \land N \leq L) \to x + M < L)$
164	150 162 163	sylc	$⊢ (((L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \land (x \in ℕ_{0} \land x < N - M)) \land N \leq L) \to x + M < L$
165	164	exp31	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to ((x \in ℕ_{0} \land x < N - M) \to (N \leq L \to x + M < L))$
166	165	com23	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (N \leq L \to ((x \in ℕ_{0} \land x < N - M) \to x + M < L))$
167	166	ex	$⊢ L \in ℕ_{0} \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \leq L \to ((x \in ℕ_{0} \land x < N - M) \to x + M < L)))$
168	167	adantl	$⊢ (S \in V \land L \in ℕ_{0}) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \leq L \to ((x \in ℕ_{0} \land x < N - M) \to x + M < L)))$
169	168	3imp	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to ((x \in ℕ_{0} \land x < N - M) \to x + M < L)$
170	169	ad2antrr	$⊢ ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to ((x \in ℕ_{0} \land x < N - M) \to x + M < L)$
171	170	com12	$⊢ (x \in ℕ_{0} \land x < N - M) \to (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to x + M < L)$
172	171	3adant2	$⊢ (x \in ℕ_{0} \land N - M \in ℕ \land x < N - M) \to (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to x + M < L)$
173	137 172	sylbi	$⊢ x \in (0 ..^N - M) \to (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to x + M < L)$
174	173	impcom	$⊢ (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \land x \in (0 ..^N - M)) \to x + M < L$
175		elfzo0	$⊢ x + M \in (0 ..^L) \leftrightarrow (x + M \in ℕ_{0} \land L \in ℕ \land x + M < L)$
176	107 136 174 175	syl3anbrc	$⊢ (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \land x \in (0 ..^N - M)) \to x + M \in (0 ..^L)$
177		repswsymb	$⊢ (S \in V \land L \in ℕ_{0} \land x + M \in (0 ..^L)) \to (S repeatS L) (x + M) = S$
178	98 100 176 177	syl3anc	$⊢ (((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \land x \in (0 ..^N - M)) \to (S repeatS L) (x + M) = S$
179	178	mpteq2dva	$⊢ ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)) = (x \in (0 ..^N - M) ⟼ S)$
180	33	3ad2ant2	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to N - M \in ℤ$
181	180	adantr	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to N - M \in ℤ$
182	58	3ad2ant2	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (M \in ℝ \land N \in ℝ)$
183		ltle	$⊢ (M \in ℝ \land N \in ℝ) \to (M < N \to M \leq N)$
184	182 183	syl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (M < N \to M \leq N)$
185	26	3ad2ant2	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (N \in ℝ \land M \in ℝ)$
186	185 56	syl	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (0 \leq N - M \leftrightarrow M \leq N)$
187	184 186	sylibrd	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (M < N \to 0 \leq N - M)$
188	187	imp	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to 0 \leq N - M$
189	181 188 55	sylanbrc	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to N - M \in ℕ_{0}$
190	97 189	jca	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to (S \in V \land N - M \in ℕ_{0})$
191	190	adantr	$⊢ ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to (S \in V \land N - M \in ℕ_{0})$
192		reps	$⊢ (S \in V \land N - M \in ℕ_{0}) \to S repeatS (N - M) = (x \in (0 ..^N - M) ⟼ S)$
193	192	eqcomd	$⊢ (S \in V \land N - M \in ℕ_{0}) \to (x \in (0 ..^N - M) ⟼ S) = S repeatS (N - M)$
194	191 193	syl	$⊢ ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to (x \in (0 ..^N - M) ⟼ S) = S repeatS (N - M)$
195	179 194	eqtrd	$⊢ ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \land (0 \leq M \land N \leq L)) \to (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)) = S repeatS (N - M)$
196	195	ex	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to ((0 \leq M \land N \leq L) \to (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)) = S repeatS (N - M))$
197	96 196	sylbid	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to ((M ..^N) \subseteq (0 ..^L) \to (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)) = S repeatS (N - M))$
198	197	impcom	$⊢ ((M ..^N) \subseteq (0 ..^L) \land (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N)) \to (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)) = S repeatS (N - M)$
199	86 198	eqtrd	$⊢ ((M ..^N) \subseteq (0 ..^L) \land (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N)) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M)$
200		iffalse	$⊢ \neg (M ..^N) \subseteq (0 ..^L) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = \emptyset$
201	200	adantr	$⊢ (\neg (M ..^N) \subseteq (0 ..^L) \land (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N)) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = \emptyset$
202	96	notbid	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to (\neg (M ..^N) \subseteq (0 ..^L) \leftrightarrow \neg (0 \leq M \land N \leq L))$
203		ianor	$⊢ \neg (0 \leq M \land N \leq L) \leftrightarrow (\neg 0 \leq M \lor \neg N \leq L)$
204		nn0ge0	$⊢ M \in ℕ_{0} \to 0 \leq M$
205		pm2.24	$⊢ 0 \leq M \to (\neg 0 \leq M \to S repeatS (N - M) = \emptyset)$
206	204 205	syl	$⊢ M \in ℕ_{0} \to (\neg 0 \leq M \to S repeatS (N - M) = \emptyset)$
207	206	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (\neg 0 \leq M \to S repeatS (N - M) = \emptyset)$
208	207	3ad2ant2	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (\neg 0 \leq M \to S repeatS (N - M) = \emptyset)$
209	208	adantr	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to (\neg 0 \leq M \to S repeatS (N - M) = \emptyset)$
210	209	com12	$⊢ \neg 0 \leq M \to ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to S repeatS (N - M) = \emptyset)$
211		pm2.24	$⊢ N \leq L \to (\neg N \leq L \to S repeatS (N - M) = \emptyset)$
212	211	3ad2ant3	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (\neg N \leq L \to S repeatS (N - M) = \emptyset)$
213	212	adantr	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to (\neg N \leq L \to S repeatS (N - M) = \emptyset)$
214	213	com12	$⊢ \neg N \leq L \to ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to S repeatS (N - M) = \emptyset)$
215	210 214	jaoi	$⊢ (\neg 0 \leq M \lor \neg N \leq L) \to ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to S repeatS (N - M) = \emptyset)$
216	203 215	sylbi	$⊢ \neg (0 \leq M \land N \leq L) \to ((((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to S repeatS (N - M) = \emptyset)$
217	216	com12	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to (\neg (0 \leq M \land N \leq L) \to S repeatS (N - M) = \emptyset)$
218	202 217	sylbid	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to (\neg (M ..^N) \subseteq (0 ..^L) \to S repeatS (N - M) = \emptyset)$
219	218	impcom	$⊢ (\neg (M ..^N) \subseteq (0 ..^L) \land (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N)) \to S repeatS (N - M) = \emptyset$
220	201 219	eqtr4d	$⊢ (\neg (M ..^N) \subseteq (0 ..^L) \land (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N)) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M)$
221	199 220	pm2.61ian	$⊢ (((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \land M < N) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M)$
222	221	ex	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (M < N \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M))$
223	85 222	sylbid	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (\neg N \leq M \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M))$
224	81 223	pm2.61d	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to if ((M ..^N) \subseteq (0 ..^L), (x \in (0 ..^N - M) ⟼ (S repeatS L) (x + M)), \emptyset) = S repeatS (N - M)$
225	10 15 224	3eqtrd	$⊢ ((S \in V \land L \in ℕ_{0}) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq L) \to (S repeatS L) substr ⟨M, N⟩ = S repeatS (N - M)$

Metamath Proof Explorer

Theorem repswswrd

Proof