metakunt24

Description: Technical condition such that metakunt17 holds. (Contributed by metakunt, 28-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		metakunt24.1	$⊢ φ \to M \in ℕ$
2		metakunt24.2	$⊢ φ \to I \in ℕ$
3		metakunt24.3	$⊢ φ \to I \leq M$
4		indir	$⊢ ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\})$
5	4	a1i	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\})$
6	1 2 3	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))$
7	6	simpld	$⊢ φ \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)$
8	7	simp2d	$⊢ φ \to (1 \dots I - 1) \cap \{M\} = \emptyset$
9	7	simp3d	$⊢ φ \to (I \dots M - 1) \cap \{M\} = \emptyset$
10	8 9	uneq12d	$⊢ φ \to ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\}) = \emptyset \cup \emptyset$
11		unidm	$⊢ \emptyset \cup \emptyset = \emptyset$
12	11	a1i	$⊢ φ \to \emptyset \cup \emptyset = \emptyset$
13	10 12	eqtrd	$⊢ φ \to ((1 \dots I - 1) \cap \{M\}) \cup ((I \dots M - 1) \cap \{M\}) = \emptyset$
14	5 13	eqtrd	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = \emptyset$
15		1zzd	$⊢ φ \to 1 \in ℤ$
16	1	nnzd	$⊢ φ \to M \in ℤ$
17	1	nnge1d	$⊢ φ \to 1 \leq M$
18	1	nnred	$⊢ φ \to M \in ℝ$
19	18	leidd	$⊢ φ \to M \leq M$
20	15 16 16 17 19	elfzd	$⊢ φ \to M \in (1 \dots M)$
21	20	fzsplitnd	$⊢ φ \to (1 \dots M) = (1 \dots M - 1) \cup (M \dots M)$
22		oveq1	$⊢ I = M \to I - 1 = M - 1$
23	22	oveq2d	$⊢ I = M \to (1 \dots I - 1) = (1 \dots M - 1)$
24		oveq1	$⊢ I = M \to (I \dots M - 1) = (M \dots M - 1)$
25	23 24	uneq12d	$⊢ I = M \to (1 \dots I - 1) \cup (I \dots M - 1) = (1 \dots M - 1) \cup (M \dots M - 1)$
26	25	uneq1d	$⊢ I = M \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cup (M \dots M) = ((1 \dots M - 1) \cup (M \dots M - 1)) \cup (M \dots M)$
27	26	adantl	$⊢ (φ \land I = M) \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cup (M \dots M) = ((1 \dots M - 1) \cup (M \dots M - 1)) \cup (M \dots M)$
28	18	ltm1d	$⊢ φ \to M - 1 < M$
29	16 15	zsubcld	$⊢ φ \to M - 1 \in ℤ$
30		fzn	$⊢ (M \in ℤ \land M - 1 \in ℤ) \to (M - 1 < M \leftrightarrow (M \dots M - 1) = \emptyset)$
31	16 29 30	syl2anc	$⊢ φ \to (M - 1 < M \leftrightarrow (M \dots M - 1) = \emptyset)$
32	28 31	mpbid	$⊢ φ \to (M \dots M - 1) = \emptyset$
33	32	adantr	$⊢ (φ \land I = M) \to (M \dots M - 1) = \emptyset$
34	33	uneq2d	$⊢ (φ \land I = M) \to (1 \dots M - 1) \cup (M \dots M - 1) = (1 \dots M - 1) \cup \emptyset$
35		un0	$⊢ (1 \dots M - 1) \cup \emptyset = (1 \dots M - 1)$
36	35	a1i	$⊢ (φ \land I = M) \to (1 \dots M - 1) \cup \emptyset = (1 \dots M - 1)$
37	34 36	eqtrd	$⊢ (φ \land I = M) \to (1 \dots M - 1) \cup (M \dots M - 1) = (1 \dots M - 1)$
38	37	uneq1d	$⊢ (φ \land I = M) \to ((1 \dots M - 1) \cup (M \dots M - 1)) \cup (M \dots M) = (1 \dots M - 1) \cup (M \dots M)$
39	27 38	eqtrd	$⊢ (φ \land I = M) \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cup (M \dots M) = (1 \dots M - 1) \cup (M \dots M)$
40	39	eqcomd	$⊢ (φ \land I = M) \to (1 \dots M - 1) \cup (M \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cup (M \dots M)$
41	15	adantr	$⊢ (φ \land \neg I = M) \to 1 \in ℤ$
42	16	adantr	$⊢ (φ \land \neg I = M) \to M \in ℤ$
43	42 41	zsubcld	$⊢ (φ \land \neg I = M) \to M - 1 \in ℤ$
44	2	nnzd	$⊢ φ \to I \in ℤ$
45	44	adantr	$⊢ (φ \land \neg I = M) \to I \in ℤ$
46	2	nnge1d	$⊢ φ \to 1 \leq I$
47	46	adantr	$⊢ (φ \land \neg I = M) \to 1 \leq I$
48		eqid	$⊢ M = M$
49		eqeq1	$⊢ M = I \to (M = M \leftrightarrow I = M)$
50	48 49	mpbii	$⊢ M = I \to I = M$
51	50	necon3bi	$⊢ \neg I = M \to M \neq I$
52	51	adantl	$⊢ (φ \land \neg I = M) \to M \neq I$
53	2	nnred	$⊢ φ \to I \in ℝ$
54	53 18 3	leltned	$⊢ φ \to (I < M \leftrightarrow M \neq I)$
55	54	adantr	$⊢ (φ \land \neg I = M) \to (I < M \leftrightarrow M \neq I)$
56	52 55	mpbird	$⊢ (φ \land \neg I = M) \to I < M$
57		zltlem1	$⊢ (I \in ℤ \land M \in ℤ) \to (I < M \leftrightarrow I \leq M - 1)$
58	44 16 57	syl2anc	$⊢ φ \to (I < M \leftrightarrow I \leq M - 1)$
59	58	adantr	$⊢ (φ \land \neg I = M) \to (I < M \leftrightarrow I \leq M - 1)$
60	56 59	mpbid	$⊢ (φ \land \neg I = M) \to I \leq M - 1$
61	41 43 45 47 60	fzsplitnr	$⊢ (φ \land \neg I = M) \to (1 \dots M - 1) = (1 \dots I - 1) \cup (I \dots M - 1)$
62	61	uneq1d	$⊢ (φ \land \neg I = M) \to (1 \dots M - 1) \cup (M \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cup (M \dots M)$
63	40 62	pm2.61dan	$⊢ φ \to (1 \dots M - 1) \cup (M \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cup (M \dots M)$
64		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
65	16 64	syl	$⊢ φ \to (M \dots M) = \{M\}$
66	65	uneq2d	$⊢ φ \to ((1 \dots I - 1) \cup (I \dots M - 1)) \cup (M \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cup \{M\}$
67	21 63 66	3eqtrd	$⊢ φ \to (1 \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cup \{M\}$
68		uncom	$⊢ (M - I + 1 \dots M - 1) \cup (1 \dots M - I) = (1 \dots M - I) \cup (M - I + 1 \dots M - 1)$
69	68	a1i	$⊢ φ \to (M - I + 1 \dots M - 1) \cup (1 \dots M - I) = (1 \dots M - I) \cup (M - I + 1 \dots M - 1)$
70	69	uneq1d	$⊢ φ \to ((M - I + 1 \dots M - 1) \cup (1 \dots M - I)) \cup \{M\} = ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup \{M\}$
71	65	uneq2d	$⊢ φ \to ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup (M \dots M) = ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup \{M\}$
72	71	eqcomd	$⊢ φ \to ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup \{M\} = ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup (M \dots M)$
73		fz10	$⊢ (1 \dots 0) = \emptyset$
74	73	uneq1i	$⊢ (1 \dots 0) \cup (1 \dots M - 1) = \emptyset \cup (1 \dots M - 1)$
75	74	a1i	$⊢ φ \to (1 \dots 0) \cup (1 \dots M - 1) = \emptyset \cup (1 \dots M - 1)$
76	75	adantr	$⊢ (φ \land I = M) \to (1 \dots 0) \cup (1 \dots M - 1) = \emptyset \cup (1 \dots M - 1)$
77		uncom	$⊢ (1 \dots M - 1) \cup \emptyset = \emptyset \cup (1 \dots M - 1)$
78	77	eqeq1i	$⊢ (1 \dots M - 1) \cup \emptyset = (1 \dots M - 1) \leftrightarrow \emptyset \cup (1 \dots M - 1) = (1 \dots M - 1)$
79	78	imbi2i	$⊢ ((φ \land I = M) \to (1 \dots M - 1) \cup \emptyset = (1 \dots M - 1)) \leftrightarrow ((φ \land I = M) \to \emptyset \cup (1 \dots M - 1) = (1 \dots M - 1))$
80	36 79	mpbi	$⊢ (φ \land I = M) \to \emptyset \cup (1 \dots M - 1) = (1 \dots M - 1)$
81	76 80	eqtrd	$⊢ (φ \land I = M) \to (1 \dots 0) \cup (1 \dots M - 1) = (1 \dots M - 1)$
82	81	eqcomd	$⊢ (φ \land I = M) \to (1 \dots M - 1) = (1 \dots 0) \cup (1 \dots M - 1)$
83		oveq2	$⊢ I = M \to M - I = M - M$
84	83	adantl	$⊢ (φ \land I = M) \to M - I = M - M$
85	18	recnd	$⊢ φ \to M \in ℂ$
86	85	subidd	$⊢ φ \to M - M = 0$
87	86	adantr	$⊢ (φ \land I = M) \to M - M = 0$
88	84 87	eqtrd	$⊢ (φ \land I = M) \to M - I = 0$
89	88	oveq2d	$⊢ (φ \land I = M) \to (1 \dots M - I) = (1 \dots 0)$
90	83	oveq1d	$⊢ I = M \to M - I + 1 = M - M + 1$
91	90	adantl	$⊢ (φ \land I = M) \to M - I + 1 = M - M + 1$
92	87	oveq1d	$⊢ (φ \land I = M) \to M - M + 1 = 0 + 1$
93	91 92	eqtrd	$⊢ (φ \land I = M) \to M - I + 1 = 0 + 1$
94		1e0p1	$⊢ 1 = 0 + 1$
95	93 94	eqtr4di	$⊢ (φ \land I = M) \to M - I + 1 = 1$
96	95	oveq1d	$⊢ (φ \land I = M) \to (M - I + 1 \dots M - 1) = (1 \dots M - 1)$
97	89 96	uneq12d	$⊢ (φ \land I = M) \to (1 \dots M - I) \cup (M - I + 1 \dots M - 1) = (1 \dots 0) \cup (1 \dots M - 1)$
98	97	eqcomd	$⊢ (φ \land I = M) \to (1 \dots 0) \cup (1 \dots M - 1) = (1 \dots M - I) \cup (M - I + 1 \dots M - 1)$
99	82 98	eqtrd	$⊢ (φ \land I = M) \to (1 \dots M - 1) = (1 \dots M - I) \cup (M - I + 1 \dots M - 1)$
100	42 45	zsubcld	$⊢ (φ \land \neg I = M) \to M - I \in ℤ$
101	53	adantr	$⊢ (φ \land \neg I = M) \to I \in ℝ$
102	18	adantr	$⊢ (φ \land \neg I = M) \to M \in ℝ$
103		1red	$⊢ (φ \land \neg I = M) \to 1 \in ℝ$
104	101 102 103 60	lesubd	$⊢ (φ \land \neg I = M) \to 1 \leq M - I$
105	103 101 102 47	lesub2dd	$⊢ (φ \land \neg I = M) \to M - I \leq M - 1$
106	41 43 100 104 105	elfzd	$⊢ (φ \land \neg I = M) \to M - I \in (1 \dots M - 1)$
107		fzsplit	$⊢ M - I \in (1 \dots M - 1) \to (1 \dots M - 1) = (1 \dots M - I) \cup (M - I + 1 \dots M - 1)$
108	106 107	syl	$⊢ (φ \land \neg I = M) \to (1 \dots M - 1) = (1 \dots M - I) \cup (M - I + 1 \dots M - 1)$
109	99 108	pm2.61dan	$⊢ φ \to (1 \dots M - 1) = (1 \dots M - I) \cup (M - I + 1 \dots M - 1)$
110	109	uneq1d	$⊢ φ \to (1 \dots M - 1) \cup (M \dots M) = ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup (M \dots M)$
111	21 110	eqtrd	$⊢ φ \to (1 \dots M) = ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup (M \dots M)$
112	111	eqcomd	$⊢ φ \to ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup (M \dots M) = (1 \dots M)$
113	72 112	eqtrd	$⊢ φ \to ((1 \dots M - I) \cup (M - I + 1 \dots M - 1)) \cup \{M\} = (1 \dots M)$
114	70 113	eqtrd	$⊢ φ \to ((M - I + 1 \dots M - 1) \cup (1 \dots M - I)) \cup \{M\} = (1 \dots M)$
115	114	eqcomd	$⊢ φ \to (1 \dots M) = ((M - I + 1 \dots M - 1) \cup (1 \dots M - I)) \cup \{M\}$
116	14 67 115	3jca	$⊢ φ \to (((1 \dots I - 1) \cup (I \dots M - 1)) \cap \{M\} = \emptyset \land (1 \dots M) = ((1 \dots I - 1) \cup (I \dots M - 1)) \cup \{M\} \land (1 \dots M) = ((M - I + 1 \dots M - 1) \cup (1 \dots M - I)) \cup \{M\})$

Metamath Proof Explorer

Theorem metakunt24

Proof