metakunt12

Description: C is the right inverse for A. (Contributed by metakunt, 25-May-2024)

	Ref	Expression
Hypotheses	metakunt12.1	$⊢ φ \to M \in ℕ$
	metakunt12.2	$⊢ φ \to I \in ℕ$
	metakunt12.3	$⊢ φ \to I \leq M$
	metakunt12.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
	metakunt12.5	$⊢ C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
	metakunt12.6	$⊢ φ \to X \in (1 \dots M)$
Assertion	metakunt12	$⊢ (φ \land \neg (X = M \lor X < I)) \to A (C (X)) = X$

Proof

Step	Hyp	Ref	Expression
1		metakunt12.1	$⊢ φ \to M \in ℕ$
2		metakunt12.2	$⊢ φ \to I \in ℕ$
3		metakunt12.3	$⊢ φ \to I \leq M$
4		metakunt12.4	$⊢ A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
5		metakunt12.5	$⊢ C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
6		metakunt12.6	$⊢ φ \to X \in (1 \dots M)$
7		ioran	$⊢ \neg (X = M \lor X < I) \leftrightarrow (\neg X = M \land \neg X < I)$
8	4	a1i	$⊢ (φ \land \neg X = M \land \neg X < I) \to A = (x \in (1 \dots M) ⟼ if (x = I, M, if (x < I, x, x - 1)))$
9		eqeq1	$⊢ x = C (X) \to (x = I \leftrightarrow C (X) = I)$
10		breq1	$⊢ x = C (X) \to (x < I \leftrightarrow C (X) < I)$
11		id	$⊢ x = C (X) \to x = C (X)$
12		oveq1	$⊢ x = C (X) \to x - 1 = C (X) - 1$
13	10 11 12	ifbieq12d	$⊢ x = C (X) \to if (x < I, x, x - 1) = if (C (X) < I, C (X), C (X) - 1)$
14	9 13	ifbieq2d	$⊢ x = C (X) \to if (x = I, M, if (x < I, x, x - 1)) = if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1))$
15	14	adantl	$⊢ ((φ \land \neg X = M \land \neg X < I) \land x = C (X)) \to if (x = I, M, if (x < I, x, x - 1)) = if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1))$
16	5	a1i	$⊢ (φ \land \neg X = M \land \neg X < I) \to C = (y \in (1 \dots M) ⟼ if (y = M, I, if (y < I, y, y + 1)))$
17		eqeq1	$⊢ y = X \to (y = M \leftrightarrow X = M)$
18		breq1	$⊢ y = X \to (y < I \leftrightarrow X < I)$
19		id	$⊢ y = X \to y = X$
20		oveq1	$⊢ y = X \to y + 1 = X + 1$
21	18 19 20	ifbieq12d	$⊢ y = X \to if (y < I, y, y + 1) = if (X < I, X, X + 1)$
22	17 21	ifbieq2d	$⊢ y = X \to if (y = M, I, if (y < I, y, y + 1)) = if (X = M, I, if (X < I, X, X + 1))$
23	22	adantl	$⊢ ((φ \land \neg X = M \land \neg X < I) \land y = X) \to if (y = M, I, if (y < I, y, y + 1)) = if (X = M, I, if (X < I, X, X + 1))$
24		simp2	$⊢ (φ \land \neg X = M \land \neg X < I) \to \neg X = M$
25		iffalse	$⊢ \neg X = M \to if (X = M, I, if (X < I, X, X + 1)) = if (X < I, X, X + 1)$
26	24 25	syl	$⊢ (φ \land \neg X = M \land \neg X < I) \to if (X = M, I, if (X < I, X, X + 1)) = if (X < I, X, X + 1)$
27		simp3	$⊢ (φ \land \neg X = M \land \neg X < I) \to \neg X < I$
28		iffalse	$⊢ \neg X < I \to if (X < I, X, X + 1) = X + 1$
29	27 28	syl	$⊢ (φ \land \neg X = M \land \neg X < I) \to if (X < I, X, X + 1) = X + 1$
30	26 29	eqtrd	$⊢ (φ \land \neg X = M \land \neg X < I) \to if (X = M, I, if (X < I, X, X + 1)) = X + 1$
31	30	adantr	$⊢ ((φ \land \neg X = M \land \neg X < I) \land y = X) \to if (X = M, I, if (X < I, X, X + 1)) = X + 1$
32	23 31	eqtrd	$⊢ ((φ \land \neg X = M \land \neg X < I) \land y = X) \to if (y = M, I, if (y < I, y, y + 1)) = X + 1$
33	6	3ad2ant1	$⊢ (φ \land \neg X = M \land \neg X < I) \to X \in (1 \dots M)$
34	6	elfzelzd	$⊢ φ \to X \in ℤ$
35	34	3ad2ant1	$⊢ (φ \land \neg X = M \land \neg X < I) \to X \in ℤ$
36	35	peano2zd	$⊢ (φ \land \neg X = M \land \neg X < I) \to X + 1 \in ℤ$
37	16 32 33 36	fvmptd	$⊢ (φ \land \neg X = M \land \neg X < I) \to C (X) = X + 1$
38		eqeq1	$⊢ C (X) = X + 1 \to (C (X) = I \leftrightarrow X + 1 = I)$
39		breq1	$⊢ C (X) = X + 1 \to (C (X) < I \leftrightarrow X + 1 < I)$
40		id	$⊢ C (X) = X + 1 \to C (X) = X + 1$
41		oveq1	$⊢ C (X) = X + 1 \to C (X) - 1 = X + 1 - 1$
42	39 40 41	ifbieq12d	$⊢ C (X) = X + 1 \to if (C (X) < I, C (X), C (X) - 1) = if (X + 1 < I, X + 1, X + 1 - 1)$
43	38 42	ifbieq2d	$⊢ C (X) = X + 1 \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = if (X + 1 = I, M, if (X + 1 < I, X + 1, X + 1 - 1))$
44	37 43	syl	$⊢ (φ \land \neg X = M \land \neg X < I) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = if (X + 1 = I, M, if (X + 1 < I, X + 1, X + 1 - 1))$
45	2	nnred	$⊢ φ \to I \in ℝ$
46	45	3ad2ant1	$⊢ (φ \land \neg X = M \land \neg X < I) \to I \in ℝ$
47	35	zred	$⊢ (φ \land \neg X = M \land \neg X < I) \to X \in ℝ$
48	36	zred	$⊢ (φ \land \neg X = M \land \neg X < I) \to X + 1 \in ℝ$
49	46 47	lenltd	$⊢ (φ \land \neg X = M \land \neg X < I) \to (I \leq X \leftrightarrow \neg X < I)$
50	27 49	mpbird	$⊢ (φ \land \neg X = M \land \neg X < I) \to I \leq X$
51	47	ltp1d	$⊢ (φ \land \neg X = M \land \neg X < I) \to X < X + 1$
52	46 47 48 50 51	lelttrd	$⊢ (φ \land \neg X = M \land \neg X < I) \to I < X + 1$
53	46 52	ltned	$⊢ (φ \land \neg X = M \land \neg X < I) \to I \neq X + 1$
54	53	necomd	$⊢ (φ \land \neg X = M \land \neg X < I) \to X + 1 \neq I$
55	54	neneqd	$⊢ (φ \land \neg X = M \land \neg X < I) \to \neg X + 1 = I$
56		iffalse	$⊢ \neg X + 1 = I \to if (X + 1 = I, M, if (X + 1 < I, X + 1, X + 1 - 1)) = if (X + 1 < I, X + 1, X + 1 - 1)$
57	55 56	syl	$⊢ (φ \land \neg X = M \land \neg X < I) \to if (X + 1 = I, M, if (X + 1 < I, X + 1, X + 1 - 1)) = if (X + 1 < I, X + 1, X + 1 - 1)$
58	47	lep1d	$⊢ (φ \land \neg X = M \land \neg X < I) \to X \leq X + 1$
59	46 47 48 50 58	letrd	$⊢ (φ \land \neg X = M \land \neg X < I) \to I \leq X + 1$
60	46 48	lenltd	$⊢ (φ \land \neg X = M \land \neg X < I) \to (I \leq X + 1 \leftrightarrow \neg X + 1 < I)$
61	59 60	mpbid	$⊢ (φ \land \neg X = M \land \neg X < I) \to \neg X + 1 < I$
62		iffalse	$⊢ \neg X + 1 < I \to if (X + 1 < I, X + 1, X + 1 - 1) = X + 1 - 1$
63	61 62	syl	$⊢ (φ \land \neg X = M \land \neg X < I) \to if (X + 1 < I, X + 1, X + 1 - 1) = X + 1 - 1$
64	35	zcnd	$⊢ (φ \land \neg X = M \land \neg X < I) \to X \in ℂ$
65		1cnd	$⊢ (φ \land \neg X = M \land \neg X < I) \to 1 \in ℂ$
66	64 65	pncand	$⊢ (φ \land \neg X = M \land \neg X < I) \to X + 1 - 1 = X$
67	57 63 66	3eqtrd	$⊢ (φ \land \neg X = M \land \neg X < I) \to if (X + 1 = I, M, if (X + 1 < I, X + 1, X + 1 - 1)) = X$
68	44 67	eqtrd	$⊢ (φ \land \neg X = M \land \neg X < I) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = X$
69	68	adantr	$⊢ ((φ \land \neg X = M \land \neg X < I) \land x = C (X)) \to if (C (X) = I, M, if (C (X) < I, C (X), C (X) - 1)) = X$
70	15 69	eqtrd	$⊢ ((φ \land \neg X = M \land \neg X < I) \land x = C (X)) \to if (x = I, M, if (x < I, x, x - 1)) = X$
71	1 2 3 5	metakunt2	$⊢ φ \to C : (1 \dots M) ⟶ (1 \dots M)$
72	71	3ad2ant1	$⊢ (φ \land \neg X = M \land \neg X < I) \to C : (1 \dots M) ⟶ (1 \dots M)$
73	72 33	ffvelcdmd	$⊢ (φ \land \neg X = M \land \neg X < I) \to C (X) \in (1 \dots M)$
74	8 70 73 33	fvmptd	$⊢ (φ \land \neg X = M \land \neg X < I) \to A (C (X)) = X$
75	74	3expb	$⊢ (φ \land (\neg X = M \land \neg X < I)) \to A (C (X)) = X$
76	7 75	sylan2b	$⊢ (φ \land \neg (X = M \lor X < I)) \to A (C (X)) = X$

Metamath Proof Explorer

Theorem metakunt12

Proof