swrdswrdlem

		Ref	Expression
	Assertion	swrdswrdlem	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (W \in Word V \land M + K \in (0 \dots M + L) \land M + L \in (0 \dots \|W\|))$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to W \in Word V$
2		elfz2	$⊢ L \in (K \dots N - M) \leftrightarrow ((K \in ℤ \land N - M \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N - M))$
3		elfz2nn0	$⊢ K \in (0 \dots N - M) \leftrightarrow (K \in ℕ_{0} \land N - M \in ℕ_{0} \land K \leq N - M)$
4		elfz2nn0	$⊢ M \in (0 \dots N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
5		nn0addcl	$⊢ (M \in ℕ_{0} \land K \in ℕ_{0}) \to M + K \in ℕ_{0}$
6	5	adantrr	$⊢ (M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to M + K \in ℕ_{0}$
7	6	adantr	$⊢ ((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land K \leq L) \to M + K \in ℕ_{0}$
8		elnn0z	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℤ \land 0 \leq K)$
9		0red	$⊢ (K \in ℤ \land L \in ℤ) \to 0 \in ℝ$
10		zre	$⊢ K \in ℤ \to K \in ℝ$
11	10	adantr	$⊢ (K \in ℤ \land L \in ℤ) \to K \in ℝ$
12		zre	$⊢ L \in ℤ \to L \in ℝ$
13	12	adantl	$⊢ (K \in ℤ \land L \in ℤ) \to L \in ℝ$
14		letr	$⊢ (0 \in ℝ \land K \in ℝ \land L \in ℝ) \to ((0 \leq K \land K \leq L) \to 0 \leq L)$
15	9 11 13 14	syl3anc	$⊢ (K \in ℤ \land L \in ℤ) \to ((0 \leq K \land K \leq L) \to 0 \leq L)$
16		elnn0z	$⊢ L \in ℕ_{0} \leftrightarrow (L \in ℤ \land 0 \leq L)$
17		nn0addcl	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to M + L \in ℕ_{0}$
18	17	expcom	$⊢ L \in ℕ_{0} \to (M \in ℕ_{0} \to M + L \in ℕ_{0})$
19	16 18	sylbir	$⊢ (L \in ℤ \land 0 \leq L) \to (M \in ℕ_{0} \to M + L \in ℕ_{0})$
20	19	ex	$⊢ L \in ℤ \to (0 \leq L \to (M \in ℕ_{0} \to M + L \in ℕ_{0}))$
21	20	adantl	$⊢ (K \in ℤ \land L \in ℤ) \to (0 \leq L \to (M \in ℕ_{0} \to M + L \in ℕ_{0}))$
22	15 21	syld	$⊢ (K \in ℤ \land L \in ℤ) \to ((0 \leq K \land K \leq L) \to (M \in ℕ_{0} \to M + L \in ℕ_{0}))$
23	22	expd	$⊢ (K \in ℤ \land L \in ℤ) \to (0 \leq K \to (K \leq L \to (M \in ℕ_{0} \to M + L \in ℕ_{0})))$
24	23	com34	$⊢ (K \in ℤ \land L \in ℤ) \to (0 \leq K \to (M \in ℕ_{0} \to (K \leq L \to M + L \in ℕ_{0})))$
25	24	impancom	$⊢ (K \in ℤ \land 0 \leq K) \to (L \in ℤ \to (M \in ℕ_{0} \to (K \leq L \to M + L \in ℕ_{0})))$
26	8 25	sylbi	$⊢ K \in ℕ_{0} \to (L \in ℤ \to (M \in ℕ_{0} \to (K \leq L \to M + L \in ℕ_{0})))$
27	26	imp	$⊢ (K \in ℕ_{0} \land L \in ℤ) \to (M \in ℕ_{0} \to (K \leq L \to M + L \in ℕ_{0}))$
28	27	impcom	$⊢ (M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to (K \leq L \to M + L \in ℕ_{0})$
29	28	imp	$⊢ ((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land K \leq L) \to M + L \in ℕ_{0}$
30		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
31	30	adantr	$⊢ (K \in ℕ_{0} \land L \in ℤ) \to K \in ℝ$
32	31	adantl	$⊢ (M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to K \in ℝ$
33	12	adantl	$⊢ (K \in ℕ_{0} \land L \in ℤ) \to L \in ℝ$
34	33	adantl	$⊢ (M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to L \in ℝ$
35		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
36	35	adantr	$⊢ (M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to M \in ℝ$
37	32 34 36	leadd2d	$⊢ (M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to (K \leq L \leftrightarrow M + K \leq M + L)$
38	37	biimpa	$⊢ ((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land K \leq L) \to M + K \leq M + L$
39	7 29 38	3jca	$⊢ ((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land K \leq L) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)$
40	39	exp31	$⊢ M \in ℕ_{0} \to ((K \in ℕ_{0} \land L \in ℤ) \to (K \leq L \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)))$
41	40	com23	$⊢ M \in ℕ_{0} \to (K \leq L \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)))$
42	41	3ad2ant1	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (K \leq L \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)))$
43	4 42	sylbi	$⊢ M \in (0 \dots N) \to (K \leq L \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)))$
44	43	3ad2ant3	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (K \leq L \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)))$
45	44	com13	$⊢ (K \in ℕ_{0} \land L \in ℤ) \to (K \leq L \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)))$
46	45	ex	$⊢ K \in ℕ_{0} \to (L \in ℤ \to (K \leq L \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L))))$
47	46	3ad2ant1	$⊢ (K \in ℕ_{0} \land N - M \in ℕ_{0} \land K \leq N - M) \to (L \in ℤ \to (K \leq L \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L))))$
48	3 47	sylbi	$⊢ K \in (0 \dots N - M) \to (L \in ℤ \to (K \leq L \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L))))$
49	48	com13	$⊢ K \leq L \to (L \in ℤ \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L))))$
50	49	adantr	$⊢ (K \leq L \land L \leq N - M) \to (L \in ℤ \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L))))$
51	50	com12	$⊢ L \in ℤ \to ((K \leq L \land L \leq N - M) \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L))))$
52	51	3ad2ant3	$⊢ (K \in ℤ \land N - M \in ℤ \land L \in ℤ) \to ((K \leq L \land L \leq N - M) \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L))))$
53	52	imp	$⊢ ((K \in ℤ \land N - M \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N - M)) \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)))$
54	2 53	sylbi	$⊢ L \in (K \dots N - M) \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)))$
55	54	impcom	$⊢ (K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L))$
56	55	impcom	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)$
57		elfz2nn0	$⊢ M + K \in (0 \dots M + L) \leftrightarrow (M + K \in ℕ_{0} \land M + L \in ℕ_{0} \land M + K \leq M + L)$
58	56 57	sylibr	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to M + K \in (0 \dots M + L)$
59		elfz2nn0	$⊢ N \in (0 \dots \|W\|) \leftrightarrow (N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|)$
60	28	com12	$⊢ K \leq L \to ((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to M + L \in ℕ_{0})$
61	60	adantr	$⊢ (K \leq L \land L \leq N - M) \to ((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to M + L \in ℕ_{0})$
62	61	impcom	$⊢ ((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land (K \leq L \land L \leq N - M)) \to M + L \in ℕ_{0}$
63	62	adantr	$⊢ (((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land (K \leq L \land L \leq N - M)) \land (N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|)) \to M + L \in ℕ_{0}$
64		simpr2	$⊢ (((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land (K \leq L \land L \leq N - M)) \land (N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|)) \to \|W\| \in ℕ_{0}$
65		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
66	65 35	anim12i	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (N \in ℝ \land M \in ℝ)$
67		nn0re	$⊢ \|W\| \in ℕ_{0} \to \|W\| \in ℝ$
68	66 67	anim12i	$⊢ ((N \in ℕ_{0} \land M \in ℕ_{0}) \land \|W\| \in ℕ_{0}) \to ((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ)$
69		simpllr	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to M \in ℝ$
70		simpr	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to L \in ℝ$
71		simplll	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to N \in ℝ$
72	69 70 71	leaddsub2d	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to (M + L \leq N \leftrightarrow L \leq N - M)$
73		readdcl	$⊢ (M \in ℝ \land L \in ℝ) \to M + L \in ℝ$
74	73	ad4ant24	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to M + L \in ℝ$
75		simpr	$⊢ ((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \to \|W\| \in ℝ$
76	75	adantr	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to \|W\| \in ℝ$
77		letr	$⊢ (M + L \in ℝ \land N \in ℝ \land \|W\| \in ℝ) \to ((M + L \leq N \land N \leq \|W\|) \to M + L \leq \|W\|)$
78	77	expd	$⊢ (M + L \in ℝ \land N \in ℝ \land \|W\| \in ℝ) \to (M + L \leq N \to (N \leq \|W\| \to M + L \leq \|W\|))$
79	74 71 76 78	syl3anc	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to (M + L \leq N \to (N \leq \|W\| \to M + L \leq \|W\|))$
80	79	a1ddd	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to (M + L \leq N \to (N \leq \|W\| \to (0 \leq L \to M + L \leq \|W\|)))$
81	72 80	sylbird	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to (L \leq N - M \to (N \leq \|W\| \to (0 \leq L \to M + L \leq \|W\|)))$
82	81	com23	$⊢ (((N \in ℝ \land M \in ℝ) \land \|W\| \in ℝ) \land L \in ℝ) \to (N \leq \|W\| \to (L \leq N - M \to (0 \leq L \to M + L \leq \|W\|)))$
83	68 12 82	syl2an	$⊢ (((N \in ℕ_{0} \land M \in ℕ_{0}) \land \|W\| \in ℕ_{0}) \land L \in ℤ) \to (N \leq \|W\| \to (L \leq N - M \to (0 \leq L \to M + L \leq \|W\|)))$
84	83	ex	$⊢ ((N \in ℕ_{0} \land M \in ℕ_{0}) \land \|W\| \in ℕ_{0}) \to (L \in ℤ \to (N \leq \|W\| \to (L \leq N - M \to (0 \leq L \to M + L \leq \|W\|))))$
85	84	com25	$⊢ ((N \in ℕ_{0} \land M \in ℕ_{0}) \land \|W\| \in ℕ_{0}) \to (0 \leq L \to (N \leq \|W\| \to (L \leq N - M \to (L \in ℤ \to M + L \leq \|W\|))))$
86	85	ex	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (\|W\| \in ℕ_{0} \to (0 \leq L \to (N \leq \|W\| \to (L \leq N - M \to (L \in ℤ \to M + L \leq \|W\|)))))$
87	86	com24	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (N \leq \|W\| \to (0 \leq L \to (\|W\| \in ℕ_{0} \to (L \leq N - M \to (L \in ℤ \to M + L \leq \|W\|)))))$
88	87	ex	$⊢ N \in ℕ_{0} \to (M \in ℕ_{0} \to (N \leq \|W\| \to (0 \leq L \to (\|W\| \in ℕ_{0} \to (L \leq N - M \to (L \in ℤ \to M + L \leq \|W\|))))))$
89	88	com25	$⊢ N \in ℕ_{0} \to (\|W\| \in ℕ_{0} \to (N \leq \|W\| \to (0 \leq L \to (M \in ℕ_{0} \to (L \leq N - M \to (L \in ℤ \to M + L \leq \|W\|))))))$
90	89	3imp	$⊢ (N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to (0 \leq L \to (M \in ℕ_{0} \to (L \leq N - M \to (L \in ℤ \to M + L \leq \|W\|))))$
91	90	com15	$⊢ L \in ℤ \to (0 \leq L \to (M \in ℕ_{0} \to (L \leq N - M \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|))))$
92	91	adantl	$⊢ (K \in ℤ \land L \in ℤ) \to (0 \leq L \to (M \in ℕ_{0} \to (L \leq N - M \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|))))$
93	15 92	syld	$⊢ (K \in ℤ \land L \in ℤ) \to ((0 \leq K \land K \leq L) \to (M \in ℕ_{0} \to (L \leq N - M \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|))))$
94	93	expd	$⊢ (K \in ℤ \land L \in ℤ) \to (0 \leq K \to (K \leq L \to (M \in ℕ_{0} \to (L \leq N - M \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|)))))$
95	94	com35	$⊢ (K \in ℤ \land L \in ℤ) \to (0 \leq K \to (L \leq N - M \to (M \in ℕ_{0} \to (K \leq L \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|)))))$
96	95	com25	$⊢ (K \in ℤ \land L \in ℤ) \to (K \leq L \to (L \leq N - M \to (M \in ℕ_{0} \to (0 \leq K \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|)))))$
97	96	impd	$⊢ (K \in ℤ \land L \in ℤ) \to ((K \leq L \land L \leq N - M) \to (M \in ℕ_{0} \to (0 \leq K \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|))))$
98	97	com24	$⊢ (K \in ℤ \land L \in ℤ) \to (0 \leq K \to (M \in ℕ_{0} \to ((K \leq L \land L \leq N - M) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|))))$
99	98	impancom	$⊢ (K \in ℤ \land 0 \leq K) \to (L \in ℤ \to (M \in ℕ_{0} \to ((K \leq L \land L \leq N - M) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|))))$
100	8 99	sylbi	$⊢ K \in ℕ_{0} \to (L \in ℤ \to (M \in ℕ_{0} \to ((K \leq L \land L \leq N - M) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|))))$
101	100	imp	$⊢ (K \in ℕ_{0} \land L \in ℤ) \to (M \in ℕ_{0} \to ((K \leq L \land L \leq N - M) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|)))$
102	101	impcom	$⊢ (M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \to ((K \leq L \land L \leq N - M) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|))$
103	102	imp	$⊢ ((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land (K \leq L \land L \leq N - M)) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to M + L \leq \|W\|)$
104	103	imp	$⊢ (((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land (K \leq L \land L \leq N - M)) \land (N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|)) \to M + L \leq \|W\|$
105	63 64 104	3jca	$⊢ (((M \in ℕ_{0} \land (K \in ℕ_{0} \land L \in ℤ)) \land (K \leq L \land L \leq N - M)) \land (N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|)$
106	105	exp41	$⊢ M \in ℕ_{0} \to ((K \in ℕ_{0} \land L \in ℤ) \to ((K \leq L \land L \leq N - M) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
107	106	com24	$⊢ M \in ℕ_{0} \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
108	107	3ad2ant1	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
109	4 108	sylbi	$⊢ M \in (0 \dots N) \to ((N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
110	109	com12	$⊢ (N \in ℕ_{0} \land \|W\| \in ℕ_{0} \land N \leq \|W\|) \to (M \in (0 \dots N) \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
111	59 110	sylbi	$⊢ N \in (0 \dots \|W\|) \to (M \in (0 \dots N) \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
112	111	imp	$⊢ (N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|)))$
113	112	3adant1	$⊢ (W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to ((K \leq L \land L \leq N - M) \to ((K \in ℕ_{0} \land L \in ℤ) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|)))$
114	113	com13	$⊢ (K \in ℕ_{0} \land L \in ℤ) \to ((K \leq L \land L \leq N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|)))$
115	114	ex	$⊢ K \in ℕ_{0} \to (L \in ℤ \to ((K \leq L \land L \leq N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
116	115	3ad2ant1	$⊢ (K \in ℕ_{0} \land N - M \in ℕ_{0} \land K \leq N - M) \to (L \in ℤ \to ((K \leq L \land L \leq N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
117	3 116	sylbi	$⊢ K \in (0 \dots N - M) \to (L \in ℤ \to ((K \leq L \land L \leq N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
118	117	com3l	$⊢ L \in ℤ \to ((K \leq L \land L \leq N - M) \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
119	118	3ad2ant3	$⊢ (K \in ℤ \land N - M \in ℤ \land L \in ℤ) \to ((K \leq L \land L \leq N - M) \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))))$
120	119	imp	$⊢ ((K \in ℤ \land N - M \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N - M)) \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|)))$
121	2 120	sylbi	$⊢ L \in (K \dots N - M) \to (K \in (0 \dots N - M) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|)))$
122	121	impcom	$⊢ (K \in (0 \dots N - M) \land L \in (K \dots N - M)) \to ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|))$
123	122	impcom	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|)$
124		elfz2nn0	$⊢ M + L \in (0 \dots \|W\|) \leftrightarrow (M + L \in ℕ_{0} \land \|W\| \in ℕ_{0} \land M + L \leq \|W\|)$
125	123 124	sylibr	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to M + L \in (0 \dots \|W\|)$
126	1 58 125	3jca	$⊢ ((W \in Word V \land N \in (0 \dots \|W\|) \land M \in (0 \dots N)) \land (K \in (0 \dots N - M) \land L \in (K \dots N - M))) \to (W \in Word V \land M + K \in (0 \dots M + L) \land M + L \in (0 \dots \|W\|))$

Metamath Proof Explorer

Theorem swrdswrdlem

Proof