metakunt2

	Ref	Expression
Hypotheses	metakunt2.1	$⊢ φ \to M \in ℕ$
	metakunt2.2	$⊢ φ \to I \in ℕ$
	metakunt2.3	$⊢ φ \to I \leq M$
	metakunt2.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = M, I, if (x < I, x, x + 1)))$
Assertion	metakunt2	$⊢ φ \to A : (1 \dots M) ⟶ (1 \dots M)$

Proof

Step	Hyp	Ref	Expression
1		metakunt2.1	$⊢ φ \to M \in ℕ$
2		metakunt2.2	$⊢ φ \to I \in ℕ$
3		metakunt2.3	$⊢ φ \to I \leq M$
4		metakunt2.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = M, I, if (x < I, x, x + 1)))$
5		eleq1	$⊢ I = if (x = M, I, if (x < I, x, x + 1)) \to (I \in (1 \dots M) \leftrightarrow if (x = M, I, if (x < I, x, x + 1)) \in (1 \dots M))$
6		eleq1	$⊢ if (x < I, x, x + 1) = if (x = M, I, if (x < I, x, x + 1)) \to (if (x < I, x, x + 1) \in (1 \dots M) \leftrightarrow if (x = M, I, if (x < I, x, x + 1)) \in (1 \dots M))$
7		1zzd	$⊢ ((φ \land x \in (1 \dots M)) \land x = M) \to 1 \in ℤ$
8	1	nnzd	$⊢ φ \to M \in ℤ$
9	8	ad2antrr	$⊢ ((φ \land x \in (1 \dots M)) \land x = M) \to M \in ℤ$
10	2	nnzd	$⊢ φ \to I \in ℤ$
11	10	ad2antrr	$⊢ ((φ \land x \in (1 \dots M)) \land x = M) \to I \in ℤ$
12	2	nnge1d	$⊢ φ \to 1 \leq I$
13	12	ad2antrr	$⊢ ((φ \land x \in (1 \dots M)) \land x = M) \to 1 \leq I$
14	3	ad2antrr	$⊢ ((φ \land x \in (1 \dots M)) \land x = M) \to I \leq M$
15	7 9 11 13 14	elfzd	$⊢ ((φ \land x \in (1 \dots M)) \land x = M) \to I \in (1 \dots M)$
16		eleq1	$⊢ x = if (x < I, x, x + 1) \to (x \in (1 \dots M) \leftrightarrow if (x < I, x, x + 1) \in (1 \dots M))$
17		eleq1	$⊢ x + 1 = if (x < I, x, x + 1) \to (x + 1 \in (1 \dots M) \leftrightarrow if (x < I, x, x + 1) \in (1 \dots M))$
18		simpllr	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land x < I) \to x \in (1 \dots M)$
19		1zzd	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to 1 \in ℤ$
20	8	ad2antrr	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to M \in ℤ$
21		elfznn	$⊢ x \in (1 \dots M) \to x \in ℕ$
22	21	nnzd	$⊢ x \in (1 \dots M) \to x \in ℤ$
23	22	ad2antlr	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to x \in ℤ$
24	23	peano2zd	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to x + 1 \in ℤ$
25		0p1e1	$⊢ 0 + 1 = 1$
26		0red	$⊢ x \in (1 \dots M) \to 0 \in ℝ$
27	21	nnred	$⊢ x \in (1 \dots M) \to x \in ℝ$
28		1red	$⊢ x \in (1 \dots M) \to 1 \in ℝ$
29	21	nnnn0d	$⊢ x \in (1 \dots M) \to x \in ℕ_{0}$
30	29	nn0ge0d	$⊢ x \in (1 \dots M) \to 0 \leq x$
31	26 27 28 30	leadd1dd	$⊢ x \in (1 \dots M) \to 0 + 1 \leq x + 1$
32	25 31	eqbrtrrid	$⊢ x \in (1 \dots M) \to 1 \leq x + 1$
33	32	ad2antlr	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to 1 \leq x + 1$
34		simplr	$⊢ ((φ \land x \in (1 \dots M)) \land \neg x = M) \to x \in (1 \dots M)$
35		neqne	$⊢ \neg x = M \to x \neq M$
36	35	adantl	$⊢ ((φ \land x \in (1 \dots M)) \land \neg x = M) \to x \neq M$
37	34 36	fzne2d	$⊢ ((φ \land x \in (1 \dots M)) \land \neg x = M) \to x < M$
38	37	adantrr	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to x < M$
39	22	adantl	$⊢ (φ \land x \in (1 \dots M)) \to x \in ℤ$
40	8	adantr	$⊢ (φ \land x \in (1 \dots M)) \to M \in ℤ$
41	39 40	zltp1led	$⊢ (φ \land x \in (1 \dots M)) \to (x < M \leftrightarrow x + 1 \leq M)$
42	41	adantr	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to (x < M \leftrightarrow x + 1 \leq M)$
43	38 42	mpbid	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to x + 1 \leq M$
44	19 20 24 33 43	elfzd	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = M \land \neg x < I)) \to x + 1 \in (1 \dots M)$
45	44	anassrs	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = M) \land \neg x < I) \to x + 1 \in (1 \dots M)$
46	16 17 18 45	ifbothda	$⊢ ((φ \land x \in (1 \dots M)) \land \neg x = M) \to if (x < I, x, x + 1) \in (1 \dots M)$
47	5 6 15 46	ifbothda	$⊢ (φ \land x \in (1 \dots M)) \to if (x = M, I, if (x < I, x, x + 1)) \in (1 \dots M)$
48	47 4	fmptd	$⊢ φ \to A : (1 \dots M) ⟶ (1 \dots M)$

Metamath Proof Explorer

Theorem metakunt2

Proof