Metamath Proof Explorer


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 = n 0 if n = 0 A if n = S C if S < n D B
fvmptnn04if.s φ S
fvmptnn04if.n φ N 0
fvmptnn04if.y φ Y V
fvmptnn04if.a φ N = 0 Y = N / n A
fvmptnn04if.b φ 0 < N N < S Y = N / n B
fvmptnn04if.c φ N = S Y = N / n C
fvmptnn04if.d φ S < N Y = N / n D
Assertion fvmptnn04if φ G N = Y

Proof

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