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 e. NN0 |-> if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) )
fvmptnn04if.s 
|- ( ph -> S e. NN )
fvmptnn04if.n 
|- ( ph -> N e. NN0 )
fvmptnn04if.y 
|- ( ph -> Y e. V )
fvmptnn04if.a 
|- ( ( ph /\ N = 0 ) -> Y = [_ N / n ]_ A )
fvmptnn04if.b 
|- ( ( ph /\ 0 < N /\ N < S ) -> Y = [_ N / n ]_ B )
fvmptnn04if.c 
|- ( ( ph /\ N = S ) -> Y = [_ N / n ]_ C )
fvmptnn04if.d 
|- ( ( ph /\ S < N ) -> Y = [_ N / n ]_ D )
Assertion fvmptnn04if 
|- ( ph -> ( G ` N ) = Y )

Proof

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