metakunt18

Description: Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024)

	Ref	Expression
Hypotheses	metakunt18.1	$⊢ φ \to M \in ℕ$
	metakunt18.2	$⊢ φ \to I \in ℕ$
	metakunt18.3	$⊢ φ \to I \leq M$
Assertion	metakunt18	$⊢ φ \to (((1 \dots I - 1) \cap (I \dots M - 1) = \emptyset \land (1 \dots I - 1) \cap \{M\} = \emptyset \land (I \dots M - 1) \cap \{M\} = \emptyset) \land ((M - I + 1 \dots M - 1) \cap (1 \dots M - I) = \emptyset \land (M - I + 1 \dots M - 1) \cap \{M\} = \emptyset \land (1 \dots M - I) \cap \{M\} = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		metakunt18.1	$⊢ φ \to M \in ℕ$
2		metakunt18.2	$⊢ φ \to I \in ℕ$
3		metakunt18.3	$⊢ φ \to I \leq M$
4	2	nnred	$⊢ φ \to I \in ℝ$
5	4	ltm1d	$⊢ φ \to I - 1 < I$
6		fzdisj	$⊢ I - 1 < I \to (1 \dots I - 1) \cap (I \dots M - 1) = \emptyset$
7	5 6	syl	$⊢ φ \to (1 \dots I - 1) \cap (I \dots M - 1) = \emptyset$
8	1	nnzd	$⊢ φ \to M \in ℤ$
9		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
10	8 9	syl	$⊢ φ \to (M \dots M) = \{M\}$
11	10	eqcomd	$⊢ φ \to \{M\} = (M \dots M)$
12	11	ineq2d	$⊢ φ \to (1 \dots I - 1) \cap \{M\} = (1 \dots I - 1) \cap (M \dots M)$
13	2	nnzd	$⊢ φ \to I \in ℤ$
14		zlem1lt	$⊢ (I \in ℤ \land M \in ℤ) \to (I \leq M \leftrightarrow I - 1 < M)$
15	13 8 14	syl2anc	$⊢ φ \to (I \leq M \leftrightarrow I - 1 < M)$
16	3 15	mpbid	$⊢ φ \to I - 1 < M$
17		fzdisj	$⊢ I - 1 < M \to (1 \dots I - 1) \cap (M \dots M) = \emptyset$
18	16 17	syl	$⊢ φ \to (1 \dots I - 1) \cap (M \dots M) = \emptyset$
19	12 18	eqtrd	$⊢ φ \to (1 \dots I - 1) \cap \{M\} = \emptyset$
20	11	ineq2d	$⊢ φ \to (I \dots M - 1) \cap \{M\} = (I \dots M - 1) \cap (M \dots M)$
21	1	nnred	$⊢ φ \to M \in ℝ$
22	21	ltm1d	$⊢ φ \to M - 1 < M$
23		fzdisj	$⊢ M - 1 < M \to (I \dots M - 1) \cap (M \dots M) = \emptyset$
24	22 23	syl	$⊢ φ \to (I \dots M - 1) \cap (M \dots M) = \emptyset$
25	20 24	eqtrd	$⊢ φ \to (I \dots M - 1) \cap \{M\} = \emptyset$
26	7 19 25	3jca	$⊢ φ \to ((1 \dots I - 1) \cap (I \dots M - 1) = \emptyset \land (1 \dots I - 1) \cap \{M\} = \emptyset \land (I \dots M - 1) \cap \{M\} = \emptyset)$
27		incom	$⊢ (M - I + 1 \dots M - 1) \cap (1 \dots M - I) = (1 \dots M - I) \cap (M - I + 1 \dots M - 1)$
28	27	a1i	$⊢ φ \to (M - I + 1 \dots M - 1) \cap (1 \dots M - I) = (1 \dots M - I) \cap (M - I + 1 \dots M - 1)$
29	21 4	resubcld	$⊢ φ \to M - I \in ℝ$
30	29	ltp1d	$⊢ φ \to M - I < M - I + 1$
31		fzdisj	$⊢ M - I < M - I + 1 \to (1 \dots M - I) \cap (M - I + 1 \dots M - 1) = \emptyset$
32	30 31	syl	$⊢ φ \to (1 \dots M - I) \cap (M - I + 1 \dots M - 1) = \emptyset$
33	28 32	eqtrd	$⊢ φ \to (M - I + 1 \dots M - 1) \cap (1 \dots M - I) = \emptyset$
34	11	ineq2d	$⊢ φ \to (M - I + 1 \dots M - 1) \cap \{M\} = (M - I + 1 \dots M - 1) \cap (M \dots M)$
35		fzdisj	$⊢ M - 1 < M \to (M - I + 1 \dots M - 1) \cap (M \dots M) = \emptyset$
36	22 35	syl	$⊢ φ \to (M - I + 1 \dots M - 1) \cap (M \dots M) = \emptyset$
37	34 36	eqtrd	$⊢ φ \to (M - I + 1 \dots M - 1) \cap \{M\} = \emptyset$
38	11	ineq2d	$⊢ φ \to (1 \dots M - I) \cap \{M\} = (1 \dots M - I) \cap (M \dots M)$
39	2	nnrpd	$⊢ φ \to I \in ℝ^{+}$
40	21 39	ltsubrpd	$⊢ φ \to M - I < M$
41		fzdisj	$⊢ M - I < M \to (1 \dots M - I) \cap (M \dots M) = \emptyset$
42	40 41	syl	$⊢ φ \to (1 \dots M - I) \cap (M \dots M) = \emptyset$
43	38 42	eqtrd	$⊢ φ \to (1 \dots M - I) \cap \{M\} = \emptyset$
44	33 37 43	3jca	$⊢ φ \to ((M - I + 1 \dots M - 1) \cap (1 \dots M - I) = \emptyset \land (M - I + 1 \dots M - 1) \cap \{M\} = \emptyset \land (1 \dots M - I) \cap \{M\} = \emptyset)$
45	26 44	jca	$⊢ φ \to (((1 \dots I - 1) \cap (I \dots M - 1) = \emptyset \land (1 \dots I - 1) \cap \{M\} = \emptyset \land (I \dots M - 1) \cap \{M\} = \emptyset) \land ((M - I + 1 \dots M - 1) \cap (1 \dots M - I) = \emptyset \land (M - I + 1 \dots M - 1) \cap \{M\} = \emptyset \land (1 \dots M - I) \cap \{M\} = \emptyset))$

Metamath Proof Explorer

Theorem metakunt18

Proof