Theorem metakunt18

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

	Ref	Expression
Hypotheses	metakunt18.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	metakunt18.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
	metakunt18.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
Assertion	metakunt18	⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) ∧ ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		metakunt18.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		metakunt18.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3		metakunt18.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4	2	nnred	⊢ ( 𝜑 → 𝐼 ∈ ℝ )
5	4	ltm1d	⊢ ( 𝜑 → ( 𝐼 − 1 ) < 𝐼 )
6		fzdisj	⊢ ( ( 𝐼 − 1 ) < 𝐼 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ )
7	5 6	syl	⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ )
8	1	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9		fzsn	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
10	8 9	syl	⊢ ( 𝜑 → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
11	10	eqcomd	⊢ ( 𝜑 → { 𝑀 } = ( 𝑀 ... 𝑀 ) )
12	11	ineq2d	⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) )
13	2	nnzd	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
14		zlem1lt	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐼 ≤ 𝑀 ↔ ( 𝐼 − 1 ) < 𝑀 ) )
15	13 8 14	syl2anc	⊢ ( 𝜑 → ( 𝐼 ≤ 𝑀 ↔ ( 𝐼 − 1 ) < 𝑀 ) )
16	3 15	mpbid	⊢ ( 𝜑 → ( 𝐼 − 1 ) < 𝑀 )
17		fzdisj	⊢ ( ( 𝐼 − 1 ) < 𝑀 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
18	16 17	syl	⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
19	12 18	eqtrd	⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
20	11	ineq2d	⊢ ( 𝜑 → ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) )
21	1	nnred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
22	21	ltm1d	⊢ ( 𝜑 → ( 𝑀 − 1 ) < 𝑀 )
23		fzdisj	⊢ ( ( 𝑀 − 1 ) < 𝑀 → ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
24	22 23	syl	⊢ ( 𝜑 → ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
25	20 24	eqtrd	⊢ ( 𝜑 → ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
26	7 19 25	3jca	⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) )
27		incom	⊢ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) )
28	27	a1i	⊢ ( 𝜑 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) )
29	21 4	resubcld	⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) ∈ ℝ )
30	29	ltp1d	⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) < ( ( 𝑀 − 𝐼 ) + 1 ) )
31		fzdisj	⊢ ( ( 𝑀 − 𝐼 ) < ( ( 𝑀 − 𝐼 ) + 1 ) → ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) = ∅ )
32	30 31	syl	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) = ∅ )
33	28 32	eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ )
34	11	ineq2d	⊢ ( 𝜑 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) )
35		fzdisj	⊢ ( ( 𝑀 − 1 ) < 𝑀 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
36	22 35	syl	⊢ ( 𝜑 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
37	34 36	eqtrd	⊢ ( 𝜑 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
38	11	ineq2d	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ ( 𝑀 ... 𝑀 ) ) )
39	2	nnrpd	⊢ ( 𝜑 → 𝐼 ∈ ℝ+ )
40	21 39	ltsubrpd	⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) < 𝑀 )
41		fzdisj	⊢ ( ( 𝑀 − 𝐼 ) < 𝑀 → ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
42	40 41	syl	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ ( 𝑀 ... 𝑀 ) ) = ∅ )
43	38 42	eqtrd	⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ )
44	33 37 43	3jca	⊢ ( 𝜑 → ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) )
45	26 44	jca	⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) ∧ ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) ) )