fvmptnn04ifb

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

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 (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to S \in ℕ$
5	3	3ad2ant1	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to N \in ℕ_{0}$
6		simp3	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to ⦋ N / n ⦌ B \in V$
7		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
8		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
9	7 8	jca	$⊢ N \in ℕ_{0} \to (N \in ℝ \land 0 \leq N)$
10		ne0gt0	$⊢ (N \in ℝ \land 0 \leq N) \to (N \neq 0 \leftrightarrow 0 < N)$
11	3 9 10	3syl	$⊢ φ \to (N \neq 0 \leftrightarrow 0 < N)$
12	11	biimprcd	$⊢ 0 < N \to (φ \to N \neq 0)$
13	12	adantr	$⊢ (0 < N \land N < S) \to (φ \to N \neq 0)$
14	13	impcom	$⊢ (φ \land (0 < N \land N < S)) \to N \neq 0$
15	14	3adant3	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to N \neq 0$
16		neneq	$⊢ N \neq 0 \to \neg N = 0$
17	16	pm2.21d	$⊢ N \neq 0 \to (N = 0 \to ⦋ N / n ⦌ B = ⦋ N / n ⦌ A)$
18	15 17	syl	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to (N = 0 \to ⦋ N / n ⦌ B = ⦋ N / n ⦌ A)$
19	18	imp	$⊢ ((φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \land N = 0) \to ⦋ N / n ⦌ B = ⦋ N / n ⦌ A$
20		eqidd	$⊢ ((φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \land 0 < N \land N < S) \to ⦋ N / n ⦌ B = ⦋ N / n ⦌ B$
21	3 7	syl	$⊢ φ \to N \in ℝ$
22	21	adantr	$⊢ (φ \land N < S) \to N \in ℝ$
23		simpr	$⊢ (φ \land N < S) \to N < S$
24	22 23	ltned	$⊢ (φ \land N < S) \to N \neq S$
25	24	neneqd	$⊢ (φ \land N < S) \to \neg N = S$
26	25	adantrl	$⊢ (φ \land (0 < N \land N < S)) \to \neg N = S$
27	26	3adant3	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to \neg N = S$
28	27	pm2.21d	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to (N = S \to ⦋ N / n ⦌ B = ⦋ N / n ⦌ C)$
29	28	imp	$⊢ ((φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \land N = S) \to ⦋ N / n ⦌ B = ⦋ N / n ⦌ C$
30	2	nnred	$⊢ φ \to S \in ℝ$
31		ltnsym	$⊢ (N \in ℝ \land S \in ℝ) \to (N < S \to \neg S < N)$
32	21 30 31	syl2anc	$⊢ φ \to (N < S \to \neg S < N)$
33	32	com12	$⊢ N < S \to (φ \to \neg S < N)$
34	33	adantl	$⊢ (0 < N \land N < S) \to (φ \to \neg S < N)$
35	34	impcom	$⊢ (φ \land (0 < N \land N < S)) \to \neg S < N$
36	35	3adant3	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to \neg S < N$
37	36	pm2.21d	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to (S < N \to ⦋ N / n ⦌ B = ⦋ N / n ⦌ D)$
38	37	imp	$⊢ ((φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \land S < N) \to ⦋ N / n ⦌ B = ⦋ N / n ⦌ D$
39	1 4 5 6 19 20 29 38	fvmptnn04if	$⊢ (φ \land (0 < N \land N < S) \land ⦋ N / n ⦌ B \in V) \to G (N) = ⦋ N / n ⦌ B$

Metamath Proof Explorer

Theorem fvmptnn04ifb

Proof