Theorem 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=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,A,if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)\right)$$
	fvmptnn04if.s	$$⊢\phi \to S\in \mathbb{N}$$
	fvmptnn04if.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	fvmptnn04ifb	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to G\left(N\right)=⦋N/n⦌B$$

Proof

Step	Hyp	Ref	Expression
1		fvmptnn04if.g	$$⊢G=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,A,if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)\right)$$
2		fvmptnn04if.s	$$⊢\phi \to S\in \mathbb{N}$$
3		fvmptnn04if.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4	2	3ad2ant1	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to S\in \mathbb{N}$$
5	3	3ad2ant1	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to N\in {\mathbb{N}}_0$$
6		simp3	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to ⦋N/n⦌B\in V$$
7		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
8		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
9	7 8	jca	$$⊢N\in {\mathbb{N}}_0\to \left(N\in ℝ\wedge 0\le N\right)$$
10		ne0gt0	$$⊢\left(N\in ℝ\wedge 0\le N\right)\to \left(N\ne 0\leftrightarrow 0<N\right)$$
11	3 9 10	3syl	$$⊢\phi \to \left(N\ne 0\leftrightarrow 0<N\right)$$
12	11	biimprcd	$$⊢0<N\to \left(\phi \to N\ne 0\right)$$
13	12	adantr	$$⊢\left(0<N\wedge N<S\right)\to \left(\phi \to N\ne 0\right)$$
14	13	impcom	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\right)\to N\ne 0$$
15	14	3adant3	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to N\ne 0$$
16		neneq	$$⊢N\ne 0\to \neg N=0$$
17	16	pm2.21d	$$⊢N\ne 0\to \left(N=0\to ⦋N/n⦌B=⦋N/n⦌A\right)$$
18	15 17	syl	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to \left(N=0\to ⦋N/n⦌B=⦋N/n⦌A\right)$$
19	18	imp	$$⊢\left(\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\wedge N=0\right)\to ⦋N/n⦌B=⦋N/n⦌A$$
20		eqidd	$$⊢\left(\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\wedge 0<N\wedge N<S\right)\to ⦋N/n⦌B=⦋N/n⦌B$$
21	3 7	syl	$$⊢\phi \to N\in ℝ$$
22	21	adantr	$$⊢\left(\phi \wedge N<S\right)\to N\in ℝ$$
23		simpr	$$⊢\left(\phi \wedge N<S\right)\to N<S$$
24	22 23	ltned	$$⊢\left(\phi \wedge N<S\right)\to N\ne S$$
25	24	neneqd	$$⊢\left(\phi \wedge N<S\right)\to \neg N=S$$
26	25	adantrl	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\right)\to \neg N=S$$
27	26	3adant3	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to \neg N=S$$
28	27	pm2.21d	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to \left(N=S\to ⦋N/n⦌B=⦋N/n⦌C\right)$$
29	28	imp	$$⊢\left(\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\wedge N=S\right)\to ⦋N/n⦌B=⦋N/n⦌C$$
30	2	nnred	$$⊢\phi \to S\in ℝ$$
31		ltnsym	$$⊢\left(N\in ℝ\wedge S\in ℝ\right)\to \left(N<S\to \neg S<N\right)$$
32	21 30 31	syl2anc	$$⊢\phi \to \left(N<S\to \neg S<N\right)$$
33	32	com12	$$⊢N<S\to \left(\phi \to \neg S<N\right)$$
34	33	adantl	$$⊢\left(0<N\wedge N<S\right)\to \left(\phi \to \neg S<N\right)$$
35	34	impcom	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\right)\to \neg S<N$$
36	35	3adant3	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to \neg S<N$$
37	36	pm2.21d	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to \left(S<N\to ⦋N/n⦌B=⦋N/n⦌D\right)$$
38	37	imp	$$⊢\left(\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\wedge S<N\right)\to ⦋N/n⦌B=⦋N/n⦌D$$
39	1 4 5 6 19 20 29 38	fvmptnn04if	$$⊢\left(\phi \wedge \left(0<N\wedge N<S\right)\wedge ⦋N/n⦌B\in V\right)\to G\left(N\right)=⦋N/n⦌B$$