metakunt24 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > metakunt24		Structured version Visualization version GIF version

Theorem metakunt24 39655

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

**Hypotheses**
Ref	Expression
metakunt24.1	⊢ (𝜑 → 𝑀 ∈ ℕ)
metakunt24.2	⊢ (𝜑 → 𝐼 ∈ ℕ)
metakunt24.3	⊢ (𝜑 → 𝐼 ≤ 𝑀)

**Assertion**
Ref	Expression
metakunt24	⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀})))

**Proof of Theorem metakunt24**
Step	Hyp	Ref	Expression
1		indir 4176	. . . 4 ⊢ (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀}))
2	1	a1i 11	. . 3 ⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})))
3		metakunt24.1	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4		metakunt24.2	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ∈ ℕ)
5		metakunt24.3	. . . . . . . 8 ⊢ (𝜑 → 𝐼 ≤ 𝑀)
6	3, 4, 5	metakunt18 39649	. . . . . . 7 ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅)))
7	6	simpld 499	. . . . . 6 ⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅))
8	7	simp2d 1141	. . . . 5 ⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅)
9	7	simp3d 1142	. . . . 5 ⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)
10	8, 9	uneq12d 4065	. . . 4 ⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = (∅ ∪ ∅))
11		unidm 4053	. . . . 5 ⊢ (∅ ∪ ∅) = ∅
12	11	a1i 11	. . . 4 ⊢ (𝜑 → (∅ ∪ ∅) = ∅)
13	10, 12	eqtrd 2794	. . 3 ⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = ∅)
14	2, 13	eqtrd 2794	. 2 ⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅)
15		1zzd 12037	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
16	3	nnzd 12110	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
17	3	nnge1d 11707	. . . . 5 ⊢ (𝜑 → 1 ≤ 𝑀)
18	3	nnred 11674	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
19	18	leidd 11229	. . . . 5 ⊢ (𝜑 → 𝑀 ≤ 𝑀)
20	15, 16, 16, 17, 19	elfzd 12932	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (1...𝑀))
21	20	fzsplitnd 39535	. . 3 ⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)))
22		oveq1 7150	. . . . . . . . . 10 ⊢ (𝐼 = 𝑀 → (𝐼 − 1) = (𝑀 − 1))
23	22	oveq2d 7159	. . . . . . . . 9 ⊢ (𝐼 = 𝑀 → (1...(𝐼 − 1)) = (1...(𝑀 − 1)))
24		oveq1 7150	. . . . . . . . 9 ⊢ (𝐼 = 𝑀 → (𝐼...(𝑀 − 1)) = (𝑀...(𝑀 − 1)))
25	23, 24	uneq12d 4065	. . . . . . . 8 ⊢ (𝐼 = 𝑀 → ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) = ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))))
26	25	uneq1d 4063	. . . . . . 7 ⊢ (𝐼 = 𝑀 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀)))
27	26	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀)))
28	18	ltm1d 11595	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
29	16, 15	zsubcld 12116	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
30		fzn 12957	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
31	16, 29, 30	syl2anc 588	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
32	28, 31	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅)
33	32	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀...(𝑀 − 1)) = ∅)
34	33	uneq2d 4064	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) = ((1...(𝑀 − 1)) ∪ ∅))
35		un0 4280	. . . . . . . . 9 ⊢ ((1...(𝑀 − 1)) ∪ ∅) = (1...(𝑀 − 1))
36	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ ∅) = (1...(𝑀 − 1)))
37	34, 36	eqtrd 2794	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) = (1...(𝑀 − 1)))
38	37	uneq1d 4063	. . . . . 6 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)))
39	27, 38	eqtrd 2794	. . . . 5 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)))
40	39	eqcomd 2765	. . . 4 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)))
41	15	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ∈ ℤ)
42	16	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ∈ ℤ)
43	42, 41	zsubcld 12116	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 1) ∈ ℤ)
44	4	nnzd 12110	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ ℤ)
45	44	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ∈ ℤ)
46	4	nnge1d 11707	. . . . . . 7 ⊢ (𝜑 → 1 ≤ 𝐼)
47	46	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ≤ 𝐼)
48		eqid 2759	. . . . . . . . . . 11 ⊢ 𝑀 = 𝑀
49		eqeq1 2763	. . . . . . . . . . 11 ⊢ (𝑀 = 𝐼 → (𝑀 = 𝑀 ↔ 𝐼 = 𝑀))
50	48, 49	mpbii 236	. . . . . . . . . 10 ⊢ (𝑀 = 𝐼 → 𝐼 = 𝑀)
51	50	necon3bi 2975	. . . . . . . . 9 ⊢ (¬ 𝐼 = 𝑀 → 𝑀 ≠ 𝐼)
52	51	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ≠ 𝐼)
53	4	nnred 11674	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ ℝ)
54	53, 18, 5	leltned 10816	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 < 𝑀 ↔ 𝑀 ≠ 𝐼))
55	54	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝐼 < 𝑀 ↔ 𝑀 ≠ 𝐼))
56	52, 55	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 < 𝑀)
57		zltlem1 12059	. . . . . . . . 9 ⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
58	44, 16, 57	syl2anc 588	. . . . . . . 8 ⊢ (𝜑 → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
59	58	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1)))
60	56, 59	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ≤ (𝑀 − 1))
61	41, 43, 45, 47, 60	fzsplitnr 39536	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))
62	61	uneq1d 4063	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)))
63	40, 62	pm2.61dan 813	. . 3 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)))
64		fzsn 12983	. . . . 5 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
65	16, 64	syl 17	. . . 4 ⊢ (𝜑 → (𝑀...𝑀) = {𝑀})
66	65	uneq2d 4064	. . 3 ⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}))
67	21, 63, 66	3eqtrd 2798	. 2 ⊢ (𝜑 → (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}))
68		uncom 4054	. . . . . 6 ⊢ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))
69	68	a1i 11	. . . . 5 ⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))))
70	69	uneq1d 4063	. . . 4 ⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀}))
71	65	uneq2d 4064	. . . . . 6 ⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀}))
72	71	eqcomd 2765	. . . . 5 ⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀}) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)))
73		fz10 12962	. . . . . . . . . . . . . . 15 ⊢ (1...0) = ∅
74	73	uneq1i 4060	. . . . . . . . . . . . . 14 ⊢ ((1...0) ∪ (1...(𝑀 − 1))) = (∅ ∪ (1...(𝑀 − 1)))
75	74	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...0) ∪ (1...(𝑀 − 1))) = (∅ ∪ (1...(𝑀 − 1))))
76	75	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = (∅ ∪ (1...(𝑀 − 1))))
77		uncom 4054	. . . . . . . . . . . . . . 15 ⊢ ((1...(𝑀 − 1)) ∪ ∅) = (∅ ∪ (1...(𝑀 − 1)))
78	77	eqeq1i 2764	. . . . . . . . . . . . . 14 ⊢ (((1...(𝑀 − 1)) ∪ ∅) = (1...(𝑀 − 1)) ↔ (∅ ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1)))
79	78	imbi2i 340	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ ∅) = (1...(𝑀 − 1))) ↔ ((𝜑 ∧ 𝐼 = 𝑀) → (∅ ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1))))
80	36, 79	mpbi 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (∅ ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1)))
81	76, 80	eqtrd 2794	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1)))
82	81	eqcomd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...0) ∪ (1...(𝑀 − 1))))
83		oveq2 7151	. . . . . . . . . . . . . . 15 ⊢ (𝐼 = 𝑀 → (𝑀 − 𝐼) = (𝑀 − 𝑀))
84	83	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝐼) = (𝑀 − 𝑀))
85	18	recnd 10692	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℂ)
86	85	subidd 11008	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 − 𝑀) = 0)
87	86	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝑀) = 0)
88	84, 87	eqtrd 2794	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝐼) = 0)
89	88	oveq2d 7159	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 𝐼)) = (1...0))
90	83	oveq1d 7158	. . . . . . . . . . . . . . . 16 ⊢ (𝐼 = 𝑀 → ((𝑀 − 𝐼) + 1) = ((𝑀 − 𝑀) + 1))
91	90	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = ((𝑀 − 𝑀) + 1))
92	87	oveq1d 7158	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝑀) + 1) = (0 + 1))
93	91, 92	eqtrd 2794	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = (0 + 1))
94		1e0p1 12164	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
95	93, 94	eqtr4di 2812	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = 1)
96	95	oveq1d 7158	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((𝑀 − 𝐼) + 1)...(𝑀 − 1)) = (1...(𝑀 − 1)))
97	89, 96	uneq12d 4065	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) = ((1...0) ∪ (1...(𝑀 − 1))))
98	97	eqcomd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))))
99	82, 98	eqtrd 2794	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))))
100	42, 45	zsubcld 12116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ∈ ℤ)
101	53	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ∈ ℝ)
102	18	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ∈ ℝ)
103		1red 10665	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ∈ ℝ)
104	101, 102, 103, 60	lesubd 11267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ≤ (𝑀 − 𝐼))
105	103, 101, 102, 47	lesub2dd 11280	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ≤ (𝑀 − 1))
106	41, 43, 100, 104, 105	elfzd 12932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ∈ (1...(𝑀 − 1)))
107		fzsplit 12967	. . . . . . . . . 10 ⊢ ((𝑀 − 𝐼) ∈ (1...(𝑀 − 1)) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))))
108	106, 107	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))))
109	99, 108	pm2.61dan 813	. . . . . . . 8 ⊢ (𝜑 → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))))
110	109	uneq1d 4063	. . . . . . 7 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)))
111	21, 110	eqtrd 2794	. . . . . 6 ⊢ (𝜑 → (1...𝑀) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)))
112	111	eqcomd 2765	. . . . 5 ⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (1...𝑀))
113	72, 112	eqtrd 2794	. . . 4 ⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀}) = (1...𝑀))
114	70, 113	eqtrd 2794	. . 3 ⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}) = (1...𝑀))
115	114	eqcomd 2765	. 2 ⊢ (𝜑 → (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))
116	14, 67, 115	3jca 1126	1 ⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1085 = wceq 1539 ∈ wcel 2112 ≠ wne 2949 ∪ cun 3852 ∩ cin 3853 ∅c0 4221 {csn 4515 class class class wbr 5025 (class class class)co 7143 ℝcr 10559 0cc0 10560 1c1 10561 + caddc 10563 < clt 10698 ≤ cle 10699 − cmin 10893 ℕcn 11659 ℤcz 12005 ...cfz 12924

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-cnex 10616 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 ax-pre-mulgt0 10637

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-iun 4878 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-riota 7101 df-ov 7146 df-oprab 7147 df-mpo 7148 df-om 7573 df-1st 7686 df-2nd 7687 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-en 8521 df-dom 8522 df-sdom 8523 df-pnf 10700 df-mnf 10701 df-xr 10702 df-ltxr 10703 df-le 10704 df-sub 10895 df-neg 10896 df-nn 11660 df-n0 11920 df-z 12006 df-uz 12268 df-rp 12416 df-fz 12925

This theorem is referenced by: metakunt25 39656

W3C validator