fvmptnn04ifd

Description: The function value of a mapping from the nonnegative integers with four distinct cases for the forth 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	fvmptnn04ifd	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to G (N) = ⦋ N / n ⦌ D$

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 S < N \land ⦋ N / n ⦌ D \in V) \to S \in ℕ$
5	3	3ad2ant1	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to N \in ℕ_{0}$
6		simp3	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to ⦋ N / n ⦌ D \in V$
7		0red	$⊢ φ \to 0 \in ℝ$
8	2	nnred	$⊢ φ \to S \in ℝ$
9	2	nngt0d	$⊢ φ \to 0 < S$
10	7 8 9	ltnsymd	$⊢ φ \to \neg S < 0$
11	10	adantr	$⊢ (φ \land N = 0) \to \neg S < 0$
12		breq2	$⊢ N = 0 \to (S < N \leftrightarrow S < 0)$
13	12	notbid	$⊢ N = 0 \to (\neg S < N \leftrightarrow \neg S < 0)$
14	13	adantl	$⊢ (φ \land N = 0) \to (\neg S < N \leftrightarrow \neg S < 0)$
15	11 14	mpbird	$⊢ (φ \land N = 0) \to \neg S < N$
16	15	pm2.21d	$⊢ (φ \land N = 0) \to (S < N \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ A)$
17	16	impancom	$⊢ (φ \land S < N) \to (N = 0 \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ A)$
18	17	3adant3	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to (N = 0 \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ A)$
19	18	imp	$⊢ ((φ \land S < N \land ⦋ N / n ⦌ D \in V) \land N = 0) \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ A$
20	3	nn0red	$⊢ φ \to N \in ℝ$
21		ltnsym	$⊢ (S \in ℝ \land N \in ℝ) \to (S < N \to \neg N < S)$
22	8 20 21	syl2anc	$⊢ φ \to (S < N \to \neg N < S)$
23	22	imp	$⊢ (φ \land S < N) \to \neg N < S$
24	23	3adant3	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to \neg N < S$
25	24	pm2.21d	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to (N < S \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ B)$
26	25	a1d	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to (0 < N \to (N < S \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ B))$
27	26	3imp	$⊢ ((φ \land S < N \land ⦋ N / n ⦌ D \in V) \land 0 < N \land N < S) \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ B$
28	20 8	lttri3d	$⊢ φ \to (N = S \leftrightarrow (\neg N < S \land \neg S < N))$
29	28	simplbda	$⊢ (φ \land N = S) \to \neg S < N$
30	29	pm2.21d	$⊢ (φ \land N = S) \to (S < N \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ C)$
31	30	impancom	$⊢ (φ \land S < N) \to (N = S \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ C)$
32	31	3adant3	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to (N = S \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ C)$
33	32	imp	$⊢ ((φ \land S < N \land ⦋ N / n ⦌ D \in V) \land N = S) \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ C$
34		eqidd	$⊢ ((φ \land S < N \land ⦋ N / n ⦌ D \in V) \land S < N) \to ⦋ N / n ⦌ D = ⦋ N / n ⦌ D$
35	1 4 5 6 19 27 33 34	fvmptnn04if	$⊢ (φ \land S < N \land ⦋ N / n ⦌ D \in V) \to G (N) = ⦋ N / n ⦌ D$

Metamath Proof Explorer

Theorem fvmptnn04ifd

Proof