Theorem fvmptnn04if

Description: The function values of a mapping from the nonnegative integers with four distinct cases. (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$$
	fvmptnn04if.y	$$⊢\phi \to Y\in V$$
	fvmptnn04if.a	$$⊢\left(\phi \wedge N=0\right)\to Y=⦋N/n⦌A$$
	fvmptnn04if.b	$$⊢\left(\phi \wedge 0<N\wedge N<S\right)\to Y=⦋N/n⦌B$$
	fvmptnn04if.c	$$⊢\left(\phi \wedge N=S\right)\to Y=⦋N/n⦌C$$
	fvmptnn04if.d	$$⊢\left(\phi \wedge S<N\right)\to Y=⦋N/n⦌D$$
Assertion	fvmptnn04if	$$⊢\phi \to G\left(N\right)=Y$$

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		fvmptnn04if.y	$$⊢\phi \to Y\in V$$
5		fvmptnn04if.a	$$⊢\left(\phi \wedge N=0\right)\to Y=⦋N/n⦌A$$
6		fvmptnn04if.b	$$⊢\left(\phi \wedge 0<N\wedge N<S\right)\to Y=⦋N/n⦌B$$
7		fvmptnn04if.c	$$⊢\left(\phi \wedge N=S\right)\to Y=⦋N/n⦌C$$
8		fvmptnn04if.d	$$⊢\left(\phi \wedge S<N\right)\to Y=⦋N/n⦌D$$
9		csbif	$$⊢⦋N/n⦌if\left(n=0,A,if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)=if\left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}n=0,⦋N/n⦌A,⦋N/n⦌if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)$$
10		eqsbc3	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}n=0\leftrightarrow N=0\right)$$
11	3 10	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}n=0\leftrightarrow N=0\right)$$
12		csbif	$$⊢⦋N/n⦌if\left(n=S,C,if\left(S<n,D,B\right)\right)=if\left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}n=S,⦋N/n⦌C,⦋N/n⦌if\left(S<n,D,B\right)\right)$$
13		eqsbc3	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}n=S\leftrightarrow N=S\right)$$
14	3 13	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}n=S\leftrightarrow N=S\right)$$
15		csbif	$$⊢⦋N/n⦌if\left(S<n,D,B\right)=if\left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}S<n,⦋N/n⦌D,⦋N/n⦌B\right)$$
16		sbcbr2g	$$⊢N\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}S<n\leftrightarrow S<⦋N/n⦌n\right)$$
17	3 16	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}S<n\leftrightarrow S<⦋N/n⦌n\right)$$
18		csbvarg	$$⊢N\in {\mathbb{N}}_0\to ⦋N/n⦌n=N$$
19	3 18	syl	$$⊢\phi \to ⦋N/n⦌n=N$$
20	19	breq2d	$$⊢\phi \to \left(S<⦋N/n⦌n\leftrightarrow S<N\right)$$
21	17 20	bitrd	$$⊢\phi \to \left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}S<n\leftrightarrow S<N\right)$$
22	21	ifbid	$$⊢\phi \to if\left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}S<n,⦋N/n⦌D,⦋N/n⦌B\right)=if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)$$
23	15 22	syl5eq	$$⊢\phi \to ⦋N/n⦌if\left(S<n,D,B\right)=if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)$$
24	14 23	ifbieq2d	$$⊢\phi \to if\left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}n=S,⦋N/n⦌C,⦋N/n⦌if\left(S<n,D,B\right)\right)=if\left(N=S,⦋N/n⦌C,if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\right)$$
25	12 24	syl5eq	$$⊢\phi \to ⦋N/n⦌if\left(n=S,C,if\left(S<n,D,B\right)\right)=if\left(N=S,⦋N/n⦌C,if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\right)$$
26	11 25	ifbieq2d	$$⊢\phi \to if\left(\underset{\dot{}}{[}N/n\underset{\dot{}}{]}n=0,⦋N/n⦌A,⦋N/n⦌if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)=if\left(N=0,⦋N/n⦌A,if\left(N=S,⦋N/n⦌C,if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\right)\right)$$
27	9 26	syl5eq	$$⊢\phi \to ⦋N/n⦌if\left(n=0,A,if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)=if\left(N=0,⦋N/n⦌A,if\left(N=S,⦋N/n⦌C,if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\right)\right)$$
28	4	adantr	$$⊢\left(\phi \wedge N=0\right)\to Y\in V$$
29	5 28	eqeltrrd	$$⊢\left(\phi \wedge N=0\right)\to ⦋N/n⦌A\in V$$
30	7	eqcomd	$$⊢\left(\phi \wedge N=S\right)\to ⦋N/n⦌C=Y$$
31	30	adantlr	$$⊢\left(\left(\phi \wedge \neg N=0\right)\wedge N=S\right)\to ⦋N/n⦌C=Y$$
32	4	ad2antrr	$$⊢\left(\left(\phi \wedge \neg N=0\right)\wedge N=S\right)\to Y\in V$$
33	31 32	eqeltrd	$$⊢\left(\left(\phi \wedge \neg N=0\right)\wedge N=S\right)\to ⦋N/n⦌C\in V$$
34	8	eqcomd	$$⊢\left(\phi \wedge S<N\right)\to ⦋N/n⦌D=Y$$
35	34	ad4ant14	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge S<N\right)\to ⦋N/n⦌D=Y$$
36	4	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge S<N\right)\to Y\in V$$
37	35 36	eqeltrd	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge S<N\right)\to ⦋N/n⦌D\in V$$
38		simplll	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge \neg S<N\right)\to \phi$$
39		anass	$$⊢\left(\left(\neg N=0\wedge \neg N=S\right)\wedge \neg S<N\right)\leftrightarrow \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)$$
40	39	bicomi	$$⊢\left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\leftrightarrow \left(\left(\neg N=0\wedge \neg N=S\right)\wedge \neg S<N\right)$$
41	40	bianassc	$$⊢\left(\phi \wedge \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\right)\leftrightarrow \left(\left(\left(\neg N=0\wedge \neg N=S\right)\wedge \phi \right)\wedge \neg S<N\right)$$
42		an32	$$⊢\left(\left(\neg N=0\wedge \neg N=S\right)\wedge \phi \right)\leftrightarrow \left(\left(\neg N=0\wedge \phi \right)\wedge \neg N=S\right)$$
43		ancom	$$⊢\left(\neg N=0\wedge \phi \right)\leftrightarrow \left(\phi \wedge \neg N=0\right)$$
44	43	anbi1i	$$⊢\left(\left(\neg N=0\wedge \phi \right)\wedge \neg N=S\right)\leftrightarrow \left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)$$
45	42 44	bitri	$$⊢\left(\left(\neg N=0\wedge \neg N=S\right)\wedge \phi \right)\leftrightarrow \left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)$$
46	45	anbi1i	$$⊢\left(\left(\left(\neg N=0\wedge \neg N=S\right)\wedge \phi \right)\wedge \neg S<N\right)\leftrightarrow \left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge \neg S<N\right)$$
47	41 46	bitri	$$⊢\left(\phi \wedge \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\right)\leftrightarrow \left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge \neg S<N\right)$$
48		df-ne	$$⊢N\ne 0\leftrightarrow \neg N=0$$
49		elnnne0	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
50		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
51	49 50	sylbir	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)\to 0<N$$
52	51	expcom	$$⊢N\ne 0\to \left(N\in {\mathbb{N}}_0\to 0<N\right)$$
53	48 52	sylbir	$$⊢\neg N=0\to \left(N\in {\mathbb{N}}_0\to 0<N\right)$$
54	53	adantr	$$⊢\left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\to \left(N\in {\mathbb{N}}_0\to 0<N\right)$$
55	3 54	mpan9	$$⊢\left(\phi \wedge \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\right)\to 0<N$$
56	47 55	sylbir	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge \neg S<N\right)\to 0<N$$
57	3	nn0red	$$⊢\phi \to N\in ℝ$$
58	57	adantr	$$⊢\left(\phi \wedge \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\right)\to N\in ℝ$$
59	2	nnred	$$⊢\phi \to S\in ℝ$$
60	59	adantr	$$⊢\left(\phi \wedge \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\right)\to S\in ℝ$$
61	57 59	lenltd	$$⊢\phi \to \left(N\le S\leftrightarrow \neg S<N\right)$$
62	61	biimprd	$$⊢\phi \to \left(\neg S<N\to N\le S\right)$$
63	62	adantld	$$⊢\phi \to \left(\left(\neg N=S\wedge \neg S<N\right)\to N\le S\right)$$
64	63	adantld	$$⊢\phi \to \left(\left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\to N\le S\right)$$
65	64	imp	$$⊢\left(\phi \wedge \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\right)\to N\le S$$
66		nesym	$$⊢S\ne N\leftrightarrow \neg N=S$$
67	66	biimpri	$$⊢\neg N=S\to S\ne N$$
68	67	adantr	$$⊢\left(\neg N=S\wedge \neg S<N\right)\to S\ne N$$
69	68	ad2antll	$$⊢\left(\phi \wedge \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\right)\to S\ne N$$
70	58 60 65 69	leneltd	$$⊢\left(\phi \wedge \left(\neg N=0\wedge \left(\neg N=S\wedge \neg S<N\right)\right)\right)\to N<S$$
71	47 70	sylbir	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge \neg S<N\right)\to N<S$$
72	6	eqcomd	$$⊢\left(\phi \wedge 0<N\wedge N<S\right)\to ⦋N/n⦌B=Y$$
73	38 56 71 72	syl3anc	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge \neg S<N\right)\to ⦋N/n⦌B=Y$$
74	4	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge \neg S<N\right)\to Y\in V$$
75	73 74	eqeltrd	$$⊢\left(\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\wedge \neg S<N\right)\to ⦋N/n⦌B\in V$$
76	37 75	ifclda	$$⊢\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\to if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\in V$$
77	33 76	ifclda	$$⊢\left(\phi \wedge \neg N=0\right)\to if\left(N=S,⦋N/n⦌C,if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\right)\in V$$
78	29 77	ifclda	$$⊢\phi \to if\left(N=0,⦋N/n⦌A,if\left(N=S,⦋N/n⦌C,if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\right)\right)\in V$$
79	27 78	eqeltrd	$$⊢\phi \to ⦋N/n⦌if\left(n=0,A,if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)\in V$$
80	1	fvmpts	$$⊢\left(N\in {\mathbb{N}}_0\wedge ⦋N/n⦌if\left(n=0,A,if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)\in V\right)\to G\left(N\right)=⦋N/n⦌if\left(n=0,A,if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)$$
81	3 79 80	syl2anc	$$⊢\phi \to G\left(N\right)=⦋N/n⦌if\left(n=0,A,if\left(n=S,C,if\left(S<n,D,B\right)\right)\right)$$
82	5	eqcomd	$$⊢\left(\phi \wedge N=0\right)\to ⦋N/n⦌A=Y$$
83	35 73	ifeqda	$$⊢\left(\left(\phi \wedge \neg N=0\right)\wedge \neg N=S\right)\to if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)=Y$$
84	31 83	ifeqda	$$⊢\left(\phi \wedge \neg N=0\right)\to if\left(N=S,⦋N/n⦌C,if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\right)=Y$$
85	82 84	ifeqda	$$⊢\phi \to if\left(N=0,⦋N/n⦌A,if\left(N=S,⦋N/n⦌C,if\left(S<N,⦋N/n⦌D,⦋N/n⦌B\right)\right)\right)=Y$$
86	81 27 85	3eqtrd	$$⊢\phi \to G\left(N\right)=Y$$