metakunt1

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

Proof

Step	Hyp	Ref	Expression
1		metakunt1.1	$⊢ φ \to M \in ℕ$
2		metakunt1.2	$⊢ φ \to I \in ℕ$
3		metakunt1.3	$⊢ φ \to I \leq M$
4		metakunt1.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
5		eleq1	$⊢ M = if (x = I, M, if (x < I, x, x - 1)) \to (M \in (1 \dots M) \leftrightarrow if (x = I, M, if (x < I, x, x - 1)) \in (1 \dots M))$
6		eleq1	$⊢ if (x < I, x, x - 1) = if (x = I, M, if (x < I, x, x - 1)) \to (if (x < I, x, x - 1) \in (1 \dots M) \leftrightarrow if (x = I, M, if (x < I, x, x - 1)) \in (1 \dots M))$
7		1zzd	$⊢ ((φ \land x \in (1 \dots M)) \land x = I) \to 1 \in ℤ$
8	1	nnzd	$⊢ φ \to M \in ℤ$
9	8	ad2antrr	$⊢ ((φ \land x \in (1 \dots M)) \land x = I) \to M \in ℤ$
10	1	ad2antrr	$⊢ ((φ \land x \in (1 \dots M)) \land x = I) \to M \in ℕ$
11	10	nnge1d	$⊢ ((φ \land x \in (1 \dots M)) \land x = I) \to 1 \leq M$
12	1	nnred	$⊢ φ \to M \in ℝ$
13	12	ad2antrr	$⊢ ((φ \land x \in (1 \dots M)) \land x = I) \to M \in ℝ$
14	13	leidd	$⊢ ((φ \land x \in (1 \dots M)) \land x = I) \to M \leq M$
15	7 9 9 11 14	elfzd	$⊢ ((φ \land x \in (1 \dots M)) \land x = I) \to M \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 = I) \land x < I) \to x \in (1 \dots M)$
19		pm4.56	$⊢ (\neg x = I \land \neg x < I) \leftrightarrow \neg (x = I \lor x < I)$
20	19	anbi2i	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = I \land \neg x < I)) \leftrightarrow ((φ \land x \in (1 \dots M)) \land \neg (x = I \lor x < I))$
21	2	nnred	$⊢ φ \to I \in ℝ$
22	21	adantr	$⊢ (φ \land x \in (1 \dots M)) \to I \in ℝ$
23		elfznn	$⊢ x \in (1 \dots M) \to x \in ℕ$
24	23	nnred	$⊢ x \in (1 \dots M) \to x \in ℝ$
25	24	adantl	$⊢ (φ \land x \in (1 \dots M)) \to x \in ℝ$
26	22 25	jca	$⊢ (φ \land x \in (1 \dots M)) \to (I \in ℝ \land x \in ℝ)$
27		axlttri	$⊢ (I \in ℝ \land x \in ℝ) \to (I < x \leftrightarrow \neg (I = x \lor x < I))$
28	26 27	syl	$⊢ (φ \land x \in (1 \dots M)) \to (I < x \leftrightarrow \neg (I = x \lor x < I))$
29		eqcom	$⊢ I = x \leftrightarrow x = I$
30	29	orbi1i	$⊢ (I = x \lor x < I) \leftrightarrow (x = I \lor x < I)$
31	30	notbii	$⊢ \neg (I = x \lor x < I) \leftrightarrow \neg (x = I \lor x < I)$
32	28 31	bitrdi	$⊢ (φ \land x \in (1 \dots M)) \to (I < x \leftrightarrow \neg (x = I \lor x < I))$
33		1zzd	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to 1 \in ℤ$
34	8	3ad2ant1	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to M \in ℤ$
35		simp2	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to x \in (1 \dots M)$
36	35	elfzelzd	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to x \in ℤ$
37	36 33	zsubcld	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to x - 1 \in ℤ$
38		1red	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to 1 \in ℝ$
39	22	3adant3	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to I \in ℝ$
40	35 24	syl	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to x \in ℝ$
41	2	nnge1d	$⊢ φ \to 1 \leq I$
42	41	3ad2ant1	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to 1 \leq I$
43		simp3	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to I < x$
44	38 39 40 42 43	lelttrd	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to 1 < x$
45	33 36	zltlem1d	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to (1 < x \leftrightarrow 1 \leq x - 1)$
46	44 45	mpbid	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to 1 \leq x - 1$
47		1red	$⊢ (φ \land x \in (1 \dots M)) \to 1 \in ℝ$
48	25 47	resubcld	$⊢ (φ \land x \in (1 \dots M)) \to x - 1 \in ℝ$
49	12	adantr	$⊢ (φ \land x \in (1 \dots M)) \to M \in ℝ$
50		0le1	$⊢ 0 \leq 1$
51	50	a1i	$⊢ x \in (1 \dots M) \to 0 \leq 1$
52		1red	$⊢ x \in (1 \dots M) \to 1 \in ℝ$
53	24 52	subge02d	$⊢ x \in (1 \dots M) \to (0 \leq 1 \leftrightarrow x - 1 \leq x)$
54	51 53	mpbid	$⊢ x \in (1 \dots M) \to x - 1 \leq x$
55	54	adantl	$⊢ (φ \land x \in (1 \dots M)) \to x - 1 \leq x$
56		elfzle2	$⊢ x \in (1 \dots M) \to x \leq M$
57	56	adantl	$⊢ (φ \land x \in (1 \dots M)) \to x \leq M$
58	48 25 49 55 57	letrd	$⊢ (φ \land x \in (1 \dots M)) \to x - 1 \leq M$
59	58	3adant3	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to x - 1 \leq M$
60	33 34 37 46 59	elfzd	$⊢ (φ \land x \in (1 \dots M) \land I < x) \to x - 1 \in (1 \dots M)$
61	60	3expia	$⊢ (φ \land x \in (1 \dots M)) \to (I < x \to x - 1 \in (1 \dots M))$
62	32 61	sylbird	$⊢ (φ \land x \in (1 \dots M)) \to (\neg (x = I \lor x < I) \to x - 1 \in (1 \dots M))$
63	62	imp	$⊢ ((φ \land x \in (1 \dots M)) \land \neg (x = I \lor x < I)) \to x - 1 \in (1 \dots M)$
64	20 63	sylbi	$⊢ ((φ \land x \in (1 \dots M)) \land (\neg x = I \land \neg x < I)) \to x - 1 \in (1 \dots M)$
65	64	anassrs	$⊢ (((φ \land x \in (1 \dots M)) \land \neg x = I) \land \neg x < I) \to x - 1 \in (1 \dots M)$
66	16 17 18 65	ifbothda	$⊢ ((φ \land x \in (1 \dots M)) \land \neg x = I) \to if (x < I, x, x - 1) \in (1 \dots M)$
67	5 6 15 66	ifbothda	$⊢ (φ \land x \in (1 \dots M)) \to if (x = I, M, if (x < I, x, x - 1)) \in (1 \dots M)$
68	67 4	fmptd	$⊢ φ \to A : (1 \dots M) ⟶ (1 \dots M)$

Metamath Proof Explorer

Theorem metakunt1

Proof