fvmptnn04ifc

Description: The function value of a mapping from the nonnegative integers with four distinct cases for the third case. (Contributed by AV, 10-Nov-2019)

	Ref	Expression
Hypotheses	fvmptnn04if.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, A, if (n = S, C, if (S < n, D, B))))$
	fvmptnn04if.s	$⊢ φ \to S \in ℕ$
	fvmptnn04if.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	fvmptnn04ifc	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to G (N) = ⦋ N / n ⦌ C$

Proof

Step	Hyp	Ref	Expression
1		fvmptnn04if.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, A, if (n = S, C, if (S < n, D, B))))$
2		fvmptnn04if.s	$⊢ φ \to S \in ℕ$
3		fvmptnn04if.n	$⊢ φ \to N \in ℕ_{0}$
4	2	3ad2ant1	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to S \in ℕ$
5	3	3ad2ant1	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to N \in ℕ_{0}$
6		simp3	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to ⦋ N / n ⦌ C \in V$
7		nnne0	$⊢ S \in ℕ \to S \neq 0$
8	7	neneqd	$⊢ S \in ℕ \to \neg S = 0$
9	2 8	syl	$⊢ φ \to \neg S = 0$
10	9	adantr	$⊢ (φ \land N = S) \to \neg S = 0$
11		eqeq1	$⊢ N = S \to (N = 0 \leftrightarrow S = 0)$
12	11	notbid	$⊢ N = S \to (\neg N = 0 \leftrightarrow \neg S = 0)$
13	12	adantl	$⊢ (φ \land N = S) \to (\neg N = 0 \leftrightarrow \neg S = 0)$
14	10 13	mpbird	$⊢ (φ \land N = S) \to \neg N = 0$
15	14	3adant3	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to \neg N = 0$
16	15	pm2.21d	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to (N = 0 \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ A)$
17	16	imp	$⊢ ((φ \land N = S \land ⦋ N / n ⦌ C \in V) \land N = 0) \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ A$
18	3	nn0red	$⊢ φ \to N \in ℝ$
19	2	nnred	$⊢ φ \to S \in ℝ$
20	18 19	lttri3d	$⊢ φ \to (N = S \leftrightarrow (\neg N < S \land \neg S < N))$
21	20	simprbda	$⊢ (φ \land N = S) \to \neg N < S$
22	21	pm2.21d	$⊢ (φ \land N = S) \to (N < S \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ B)$
23	22	3adant3	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to (N < S \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ B)$
24	23	a1d	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to (0 < N \to (N < S \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ B))$
25	24	3imp	$⊢ ((φ \land N = S \land ⦋ N / n ⦌ C \in V) \land 0 < N \land N < S) \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ B$
26		eqidd	$⊢ ((φ \land N = S \land ⦋ N / n ⦌ C \in V) \land N = S) \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ C$
27	20	simplbda	$⊢ (φ \land N = S) \to \neg S < N$
28	27	3adant3	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to \neg S < N$
29	28	pm2.21d	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to (S < N \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ D)$
30	29	imp	$⊢ ((φ \land N = S \land ⦋ N / n ⦌ C \in V) \land S < N) \to ⦋ N / n ⦌ C = ⦋ N / n ⦌ D$
31	1 4 5 6 17 25 26 30	fvmptnn04if	$⊢ (φ \land N = S \land ⦋ N / n ⦌ C \in V) \to G (N) = ⦋ N / n ⦌ C$

Metamath Proof Explorer

Theorem fvmptnn04ifc

Proof