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 = (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}$
	fvmptnn04if.y	$⊢ φ \to Y \in V$
	fvmptnn04if.a	$⊢ (φ \land N = 0) \to Y = ⦋ N / n ⦌ A$
	fvmptnn04if.b	$⊢ (φ \land 0 < N \land N < S) \to Y = ⦋ N / n ⦌ B$
	fvmptnn04if.c	$⊢ (φ \land N = S) \to Y = ⦋ N / n ⦌ C$
	fvmptnn04if.d	$⊢ (φ \land S < N) \to Y = ⦋ N / n ⦌ D$
Assertion	fvmptnn04if	$⊢ φ \to G (N) = Y$

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

Metamath Proof Explorer

Theorem fvmptnn04if

Proof