ssfzo12bi

Description: Subset relationship for half-open integer ranges. (Contributed by Alexander van der Vekens, 5-Nov-2018)

		Ref	Expression
	Assertion	ssfzo12bi	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to ((K ..^L) \subseteq (M ..^N) \leftrightarrow (M \leq K \land L \leq N))$

Proof

Step	Hyp	Ref	Expression
1		df-3an	$⊢ (K \in ℤ \land L \in ℤ \land K < L) \leftrightarrow ((K \in ℤ \land L \in ℤ) \land K < L)$
2	1	biimpri	$⊢ ((K \in ℤ \land L \in ℤ) \land K < L) \to (K \in ℤ \land L \in ℤ \land K < L)$
3	2	3adant2	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to (K \in ℤ \land L \in ℤ \land K < L)$
4		ssfzo12	$⊢ (K \in ℤ \land L \in ℤ \land K < L) \to ((K ..^L) \subseteq (M ..^N) \to (M \leq K \land L \leq N))$
5	3 4	syl	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to ((K ..^L) \subseteq (M ..^N) \to (M \leq K \land L \leq N))$
6		elfzo2	$⊢ x \in (K ..^L) \leftrightarrow (x \in ℤ_{\geq K} \land L \in ℤ \land x < L)$
7		eluz2	$⊢ x \in ℤ_{\geq K} \leftrightarrow (K \in ℤ \land x \in ℤ \land K \leq x)$
8		simprrl	$⊢ (x \in ℤ \land ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ))) \to M \in ℤ$
9	8	adantr	$⊢ ((x \in ℤ \land ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ))) \land (M \leq K \land K \leq x)) \to M \in ℤ$
10		simpll	$⊢ ((x \in ℤ \land ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ))) \land (M \leq K \land K \leq x)) \to x \in ℤ$
11		zre	$⊢ M \in ℤ \to M \in ℝ$
12	11	adantr	$⊢ (M \in ℤ \land N \in ℤ) \to M \in ℝ$
13	12	adantl	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to M \in ℝ$
14		zre	$⊢ K \in ℤ \to K \in ℝ$
15	14	adantr	$⊢ (K \in ℤ \land L \in ℤ) \to K \in ℝ$
16	15	adantr	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to K \in ℝ$
17		zre	$⊢ x \in ℤ \to x \in ℝ$
18	17	adantr	$⊢ (x \in ℤ \land ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ))) \to x \in ℝ$
19		letr	$⊢ (M \in ℝ \land K \in ℝ \land x \in ℝ) \to ((M \leq K \land K \leq x) \to M \leq x)$
20	13 16 18 19	syl2an23an	$⊢ (x \in ℤ \land ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ))) \to ((M \leq K \land K \leq x) \to M \leq x)$
21	20	imp	$⊢ ((x \in ℤ \land ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ))) \land (M \leq K \land K \leq x)) \to M \leq x$
22	9 10 21	3jca	$⊢ ((x \in ℤ \land ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ))) \land (M \leq K \land K \leq x)) \to (M \in ℤ \land x \in ℤ \land M \leq x)$
23	22	exp31	$⊢ x \in ℤ \to (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to ((M \leq K \land K \leq x) \to (M \in ℤ \land x \in ℤ \land M \leq x)))$
24	23	com23	$⊢ x \in ℤ \to ((M \leq K \land K \leq x) \to (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to (M \in ℤ \land x \in ℤ \land M \leq x)))$
25	24	expdimp	$⊢ (x \in ℤ \land M \leq K) \to (K \leq x \to (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to (M \in ℤ \land x \in ℤ \land M \leq x)))$
26	25	impancom	$⊢ (x \in ℤ \land K \leq x) \to (M \leq K \to (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to (M \in ℤ \land x \in ℤ \land M \leq x)))$
27	26	com13	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to (M \leq K \to ((x \in ℤ \land K \leq x) \to (M \in ℤ \land x \in ℤ \land M \leq x)))$
28	27	3adant3	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to (M \leq K \to ((x \in ℤ \land K \leq x) \to (M \in ℤ \land x \in ℤ \land M \leq x)))$
29	28	com12	$⊢ M \leq K \to (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to ((x \in ℤ \land K \leq x) \to (M \in ℤ \land x \in ℤ \land M \leq x)))$
30	29	adantr	$⊢ (M \leq K \land L \leq N) \to (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to ((x \in ℤ \land K \leq x) \to (M \in ℤ \land x \in ℤ \land M \leq x)))$
31	30	impcom	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to ((x \in ℤ \land K \leq x) \to (M \in ℤ \land x \in ℤ \land M \leq x))$
32	31	com12	$⊢ (x \in ℤ \land K \leq x) \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to (M \in ℤ \land x \in ℤ \land M \leq x))$
33	32	adantr	$⊢ ((x \in ℤ \land K \leq x) \land x < L) \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to (M \in ℤ \land x \in ℤ \land M \leq x))$
34	33	imp	$⊢ (((x \in ℤ \land K \leq x) \land x < L) \land (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N))) \to (M \in ℤ \land x \in ℤ \land M \leq x)$
35		eluz2	$⊢ x \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land x \in ℤ \land M \leq x)$
36	34 35	sylibr	$⊢ (((x \in ℤ \land K \leq x) \land x < L) \land (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N))) \to x \in ℤ_{\geq M}$
37		simpl2r	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to N \in ℤ$
38	37	adantl	$⊢ (((x \in ℤ \land K \leq x) \land x < L) \land (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N))) \to N \in ℤ$
39	17	adantl	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \land x \in ℤ) \to x \in ℝ$
40		zre	$⊢ L \in ℤ \to L \in ℝ$
41	40	ad3antlr	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \land x \in ℤ) \to L \in ℝ$
42		zre	$⊢ N \in ℤ \to N \in ℝ$
43	42	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to N \in ℝ$
44	43	adantl	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to N \in ℝ$
45	44	adantr	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \land x \in ℤ) \to N \in ℝ$
46		ltletr	$⊢ (x \in ℝ \land L \in ℝ \land N \in ℝ) \to ((x < L \land L \leq N) \to x < N)$
47	39 41 45 46	syl3anc	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \land x \in ℤ) \to ((x < L \land L \leq N) \to x < N)$
48	47	ex	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to (x \in ℤ \to ((x < L \land L \leq N) \to x < N))$
49	48	com23	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ)) \to ((x < L \land L \leq N) \to (x \in ℤ \to x < N))$
50	49	3adant3	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to ((x < L \land L \leq N) \to (x \in ℤ \to x < N))$
51	50	expcomd	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to (L \leq N \to (x < L \to (x \in ℤ \to x < N)))$
52	51	adantld	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to ((M \leq K \land L \leq N) \to (x < L \to (x \in ℤ \to x < N)))$
53	52	imp	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to (x < L \to (x \in ℤ \to x < N))$
54	53	com13	$⊢ x \in ℤ \to (x < L \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x < N))$
55	54	adantr	$⊢ (x \in ℤ \land K \leq x) \to (x < L \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x < N))$
56	55	imp	$⊢ ((x \in ℤ \land K \leq x) \land x < L) \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x < N)$
57	56	imp	$⊢ (((x \in ℤ \land K \leq x) \land x < L) \land (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N))) \to x < N$
58		elfzo2	$⊢ x \in (M ..^N) \leftrightarrow (x \in ℤ_{\geq M} \land N \in ℤ \land x < N)$
59	36 38 57 58	syl3anbrc	$⊢ (((x \in ℤ \land K \leq x) \land x < L) \land (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N))) \to x \in (M ..^N)$
60	59	exp31	$⊢ (x \in ℤ \land K \leq x) \to (x < L \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x \in (M ..^N)))$
61	60	3adant1	$⊢ (K \in ℤ \land x \in ℤ \land K \leq x) \to (x < L \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x \in (M ..^N)))$
62	7 61	sylbi	$⊢ x \in ℤ_{\geq K} \to (x < L \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x \in (M ..^N)))$
63	62	imp	$⊢ (x \in ℤ_{\geq K} \land x < L) \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x \in (M ..^N))$
64	63	3adant2	$⊢ (x \in ℤ_{\geq K} \land L \in ℤ \land x < L) \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x \in (M ..^N))$
65	6 64	sylbi	$⊢ x \in (K ..^L) \to ((((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to x \in (M ..^N))$
66	65	com12	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to (x \in (K ..^L) \to x \in (M ..^N))$
67	66	ssrdv	$⊢ (((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \land (M \leq K \land L \leq N)) \to (K ..^L) \subseteq (M ..^N)$
68	67	ex	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to ((M \leq K \land L \leq N) \to (K ..^L) \subseteq (M ..^N))$
69	5 68	impbid	$⊢ ((K \in ℤ \land L \in ℤ) \land (M \in ℤ \land N \in ℤ) \land K < L) \to ((K ..^L) \subseteq (M ..^N) \leftrightarrow (M \leq K \land L \leq N))$

Metamath Proof Explorer

Theorem ssfzo12bi

Proof