MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmptnn04if Structured version   Unicode version

Theorem fvmptnn04if 19110
Description: The function values of a mapping from the nonnegative integers with four distinct cases. (Contributed by AV, 10-Nov-2019.)
Hypotheses
Ref Expression
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
Ref Expression
fvmptnn04if  |-  ( ph  ->  ( G `  N
)  =  Y )
Distinct variable groups:    n, N    S, n
Allowed substitution hints:    ph( n)    A( n)    B( n)    C( n)    D( n)    G( n)    V( n)    Y( n)

Proof of Theorem fvmptnn04if
StepHypRef Expression
1 fvmptnn04if.n . . . 4  |-  ( ph  ->  N  e.  NN0 )
2 fvmptnn04if.a . . . . . . 7  |-  ( (
ph  /\  N  = 
0 )  ->  Y  =  [_ N  /  n ]_ A )
3 fvmptnn04if.y . . . . . . . . . . 11  |-  ( ph  ->  Y  e.  V )
43adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  N  = 
0 )  ->  Y  e.  V )
54adantl 466 . . . . . . . . 9  |-  ( ( Y  =  [_ N  /  n ]_ A  /\  ( ph  /\  N  =  0 ) )  ->  Y  e.  V )
6 simpl 457 . . . . . . . . . . 11  |-  ( ( Y  =  [_ N  /  n ]_ A  /\  ( ph  /\  N  =  0 ) )  ->  Y  =  [_ N  /  n ]_ A )
76eqcomd 2468 . . . . . . . . . 10  |-  ( ( Y  =  [_ N  /  n ]_ A  /\  ( ph  /\  N  =  0 ) )  ->  [_ N  /  n ]_ A  =  Y
)
87eleq1d 2529 . . . . . . . . 9  |-  ( ( Y  =  [_ N  /  n ]_ A  /\  ( ph  /\  N  =  0 ) )  -> 
( [_ N  /  n ]_ A  e.  V  <->  Y  e.  V ) )
95, 8mpbird 232 . . . . . . . 8  |-  ( ( Y  =  [_ N  /  n ]_ A  /\  ( ph  /\  N  =  0 ) )  ->  [_ N  /  n ]_ A  e.  V
)
109ex 434 . . . . . . 7  |-  ( Y  =  [_ N  /  n ]_ A  ->  (
( ph  /\  N  =  0 )  ->  [_ N  /  n ]_ A  e.  V ) )
112, 10mpcom 36 . . . . . 6  |-  ( (
ph  /\  N  = 
0 )  ->  [_ N  /  n ]_ A  e.  V )
123ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  -.  N  =  0 )  /\  N  =  S )  ->  Y  e.  V )
13 fvmptnn04if.c . . . . . . . . . . . . 13  |-  ( (
ph  /\  N  =  S )  ->  Y  =  [_ N  /  n ]_ C )
1413eqcomd 2468 . . . . . . . . . . . 12  |-  ( (
ph  /\  N  =  S )  ->  [_ N  /  n ]_ C  =  Y )
1514ex 434 . . . . . . . . . . 11  |-  ( ph  ->  ( N  =  S  ->  [_ N  /  n ]_ C  =  Y
) )
1615adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  -.  N  =  0 )  -> 
( N  =  S  ->  [_ N  /  n ]_ C  =  Y
) )
1716imp 429 . . . . . . . . 9  |-  ( ( ( ph  /\  -.  N  =  0 )  /\  N  =  S )  ->  [_ N  /  n ]_ C  =  Y )
1817eleq1d 2529 . . . . . . . 8  |-  ( ( ( ph  /\  -.  N  =  0 )  /\  N  =  S )  ->  ( [_ N  /  n ]_ C  e.  V  <->  Y  e.  V
) )
1912, 18mpbird 232 . . . . . . 7  |-  ( ( ( ph  /\  -.  N  =  0 )  /\  N  =  S )  ->  [_ N  /  n ]_ C  e.  V
)
203ad3antrrr 729 . . . . . . . . 9  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  S  <  N )  ->  Y  e.  V )
21 fvmptnn04if.d . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  S  <  N )  ->  Y  =  [_ N  /  n ]_ D )
2221eqcomd 2468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  S  <  N )  ->  [_ N  /  n ]_ D  =  Y )
2322ex 434 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  <  N  ->  [_ N  /  n ]_ D  =  Y
) )
2423adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  N  =  0 )  -> 
( S  <  N  ->  [_ N  /  n ]_ D  =  Y
) )
2524adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  N  =  0 )  /\  -.  N  =  S )  ->  ( S  <  N  ->  [_ N  /  n ]_ D  =  Y ) )
2625imp 429 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  S  <  N )  ->  [_ N  /  n ]_ D  =  Y )
2726eleq1d 2529 . . . . . . . . 9  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  S  <  N )  ->  ( [_ N  /  n ]_ D  e.  V  <->  Y  e.  V ) )
2820, 27mpbird 232 . . . . . . . 8  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  S  <  N )  ->  [_ N  /  n ]_ D  e.  V )
293ad3antrrr 729 . . . . . . . . 9  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  -.  S  <  N )  ->  Y  e.  V )
30 simplll 757 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  -.  S  <  N )  ->  ph )
31 df-ne 2657 . . . . . . . . . . . . . . . 16  |-  ( N  =/=  0  <->  -.  N  =  0 )
32 elnnne0 10798 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  <->  ( N  e.  NN0  /\  N  =/=  0 ) )
33 nngt0 10554 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  0  <  N )
3432, 33sylbir 213 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  NN0  /\  N  =/=  0 )  -> 
0  <  N )
3534expcom 435 . . . . . . . . . . . . . . . 16  |-  ( N  =/=  0  ->  ( N  e.  NN0  ->  0  <  N ) )
3631, 35sylbir 213 . . . . . . . . . . . . . . 15  |-  ( -.  N  =  0  -> 
( N  e.  NN0  ->  0  <  N ) )
3736adantr 465 . . . . . . . . . . . . . 14  |-  ( ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N ) )  -> 
( N  e.  NN0  ->  0  <  N ) )
381, 37mpan9 469 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  ->  0  <  N
)
39 ancom 450 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  <-> 
( ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N
) )  /\  ph ) )
40 anass 649 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  -.  S  <  N )  <->  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )
4140bicomi 202 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N ) )  <->  ( ( -.  N  =  0  /\  -.  N  =  S )  /\  -.  S  <  N ) )
4241anbi1i 695 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N ) )  /\  ph )  <->  ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  -.  S  <  N
)  /\  ph ) )
43 anass 649 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  -.  S  <  N
)  /\  ph )  <->  ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ( -.  S  <  N  /\  ph ) ) )
4442, 43bitri 249 . . . . . . . . . . . . . . . . 17  |-  ( ( ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N ) )  /\  ph )  <->  ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ( -.  S  <  N  /\  ph ) ) )
4539, 44bitri 249 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  <-> 
( ( -.  N  =  0  /\  -.  N  =  S )  /\  ( -.  S  < 
N  /\  ph ) ) )
46 ancom 450 . . . . . . . . . . . . . . . . . 18  |-  ( ( -.  S  <  N  /\  ph )  <->  ( ph  /\ 
-.  S  <  N
) )
4746anbi2i 694 . . . . . . . . . . . . . . . . 17  |-  ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ( -.  S  <  N  /\  ph ) )  <->  ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ( ph  /\ 
-.  S  <  N
) ) )
48 anass 649 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ph )  /\  -.  S  <  N )  <->  ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ( ph  /\ 
-.  S  <  N
) ) )
4948bicomi 202 . . . . . . . . . . . . . . . . 17  |-  ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ( ph  /\  -.  S  < 
N ) )  <->  ( (
( -.  N  =  0  /\  -.  N  =  S )  /\  ph )  /\  -.  S  < 
N ) )
5047, 49bitri 249 . . . . . . . . . . . . . . . 16  |-  ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ( -.  S  <  N  /\  ph ) )  <->  ( (
( -.  N  =  0  /\  -.  N  =  S )  /\  ph )  /\  -.  S  < 
N ) )
5145, 50bitri 249 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  <-> 
( ( ( -.  N  =  0  /\ 
-.  N  =  S )  /\  ph )  /\  -.  S  <  N
) )
52 anass 649 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ph ) 
<->  ( -.  N  =  0  /\  ( -.  N  =  S  /\  ph ) ) )
53 ancom 450 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( -.  N  =  S  /\  ph )  <->  ( ph  /\ 
-.  N  =  S ) )
5453anbi2i 694 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  N  =  0  /\  ( -.  N  =  S  /\  ph )
)  <->  ( -.  N  =  0  /\  ( ph  /\  -.  N  =  S ) ) )
55 anass 649 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( -.  N  =  0  /\  ph )  /\  -.  N  =  S )  <->  ( -.  N  =  0  /\  ( ph  /\  -.  N  =  S ) ) )
5655bicomi 202 . . . . . . . . . . . . . . . . . . 19  |-  ( ( -.  N  =  0  /\  ( ph  /\  -.  N  =  S
) )  <->  ( ( -.  N  =  0  /\  ph )  /\  -.  N  =  S )
)
5754, 56bitri 249 . . . . . . . . . . . . . . . . . 18  |-  ( ( -.  N  =  0  /\  ( -.  N  =  S  /\  ph )
)  <->  ( ( -.  N  =  0  /\ 
ph )  /\  -.  N  =  S )
)
5852, 57bitri 249 . . . . . . . . . . . . . . . . 17  |-  ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ph ) 
<->  ( ( -.  N  =  0  /\  ph )  /\  -.  N  =  S ) )
59 ancom 450 . . . . . . . . . . . . . . . . . 18  |-  ( ( -.  N  =  0  /\  ph )  <->  ( ph  /\ 
-.  N  =  0 ) )
6059anbi1i 695 . . . . . . . . . . . . . . . . 17  |-  ( ( ( -.  N  =  0  /\  ph )  /\  -.  N  =  S )  <->  ( ( ph  /\ 
-.  N  =  0 )  /\  -.  N  =  S ) )
6158, 60bitri 249 . . . . . . . . . . . . . . . 16  |-  ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ph ) 
<->  ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S ) )
6261anbi1i 695 . . . . . . . . . . . . . . 15  |-  ( ( ( ( -.  N  =  0  /\  -.  N  =  S )  /\  ph )  /\  -.  S  <  N )  <->  ( (
( ph  /\  -.  N  =  0 )  /\  -.  N  =  S
)  /\  -.  S  <  N ) )
6351, 62bitri 249 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  <-> 
( ( ( ph  /\ 
-.  N  =  0 )  /\  -.  N  =  S )  /\  -.  S  <  N ) )
6463imbi1i 325 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N ) ) )  ->  0  <  N
)  <->  ( ( ( ( ph  /\  -.  N  =  0 )  /\  -.  N  =  S )  /\  -.  S  <  N )  -> 
0  <  N )
)
6538, 64mpbi 208 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  -.  S  <  N )  -> 
0  <  N )
661nn0red 10842 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  RR )
67 fvmptnn04if.s . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  S  e.  NN )
6867nnred 10540 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  S  e.  RR )
6966, 68lenltd 9719 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( N  <_  S  <->  -.  S  <  N ) )
7069biimprd 223 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -.  S  < 
N  ->  N  <_  S ) )
7170adantld 467 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( -.  N  =  S  /\  -.  S  <  N )  ->  N  <_  S ) )
7271adantld 467 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N
) )  ->  N  <_  S ) )
7372imp 429 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  ->  N  <_  S
)
74 nesym 2732 . . . . . . . . . . . . . . . . . 18  |-  ( S  =/=  N  <->  -.  N  =  S )
7574biimpri 206 . . . . . . . . . . . . . . . . 17  |-  ( -.  N  =  S  ->  S  =/=  N )
7675adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( -.  N  =  S  /\  -.  S  < 
N )  ->  S  =/=  N )
7776adantl 466 . . . . . . . . . . . . . . 15  |-  ( ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N ) )  ->  S  =/=  N )
7877adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  ->  S  =/=  N
)
7966adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  ->  N  e.  RR )
8068adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  ->  S  e.  RR )
8179, 80ltlend 9718 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  ->  ( N  < 
S  <->  ( N  <_  S  /\  S  =/=  N
) ) )
8273, 78, 81mpbir2and 915 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  < 
N ) ) )  ->  N  <  S
)
8363imbi1i 325 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( -.  N  =  0  /\  ( -.  N  =  S  /\  -.  S  <  N ) ) )  ->  N  <  S
)  <->  ( ( ( ( ph  /\  -.  N  =  0 )  /\  -.  N  =  S )  /\  -.  S  <  N )  ->  N  <  S ) )
8482, 83mpbi 208 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  -.  S  <  N )  ->  N  <  S )
8530, 65, 843jca 1171 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  -.  S  <  N )  -> 
( ph  /\  0  <  N  /\  N  < 
S ) )
86 fvmptnn04if.b . . . . . . . . . . . 12  |-  ( (
ph  /\  0  <  N  /\  N  <  S
)  ->  Y  =  [_ N  /  n ]_ B )
8786eqcomd 2468 . . . . . . . . . . 11  |-  ( (
ph  /\  0  <  N  /\  N  <  S
)  ->  [_ N  /  n ]_ B  =  Y )
8885, 87syl 16 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  -.  S  <  N )  ->  [_ N  /  n ]_ B  =  Y
)
8988eleq1d 2529 . . . . . . . . 9  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  -.  S  <  N )  -> 
( [_ N  /  n ]_ B  e.  V  <->  Y  e.  V ) )
9029, 89mpbird 232 . . . . . . . 8  |-  ( ( ( ( ph  /\  -.  N  =  0
)  /\  -.  N  =  S )  /\  -.  S  <  N )  ->  [_ N  /  n ]_ B  e.  V
)
9128, 90ifclda 3964 . . . . . . 7  |-  ( ( ( ph  /\  -.  N  =  0 )  /\  -.  N  =  S )  ->  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B )  e.  V )
9219, 91ifclda 3964 . . . . . 6  |-  ( (
ph  /\  -.  N  =  0 )  ->  if ( N  =  S ,  [_ N  /  n ]_ C ,  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B ) )  e.  V )
9311, 92ifclda 3964 . . . . 5  |-  ( ph  ->  if ( N  =  0 ,  [_ N  /  n ]_ A ,  if ( N  =  S ,  [_ N  /  n ]_ C ,  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B ) ) )  e.  V
)
94 csbif 3982 . . . . . . . 8  |-  [_ 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 ) ) )
9594a1i 11 . . . . . . 7  |-  ( ph  ->  [_ 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 ) ) ) )
96 eqsbc3 3364 . . . . . . . . 9  |-  ( N  e.  NN0  ->  ( [. N  /  n ]. n  =  0  <->  N  = 
0 ) )
971, 96syl 16 . . . . . . . 8  |-  ( ph  ->  ( [. N  /  n ]. n  =  0  <-> 
N  =  0 ) )
98 eqidd 2461 . . . . . . . 8  |-  ( ph  ->  [_ N  /  n ]_ A  =  [_ N  /  n ]_ A )
99 csbif 3982 . . . . . . . . . 10  |-  [_ 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 ) )
10099a1i 11 . . . . . . . . 9  |-  ( ph  ->  [_ 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 ) ) )
101 eqsbc3 3364 . . . . . . . . . . 11  |-  ( N  e.  NN0  ->  ( [. N  /  n ]. n  =  S  <->  N  =  S
) )
1021, 101syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( [. N  /  n ]. n  =  S  <-> 
N  =  S ) )
103 eqidd 2461 . . . . . . . . . 10  |-  ( ph  ->  [_ N  /  n ]_ C  =  [_ N  /  n ]_ C )
104 csbif 3982 . . . . . . . . . . . 12  |-  [_ N  /  n ]_ if ( S  <  n ,  D ,  B )  =  if ( [. N  /  n ]. S  <  n ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B )
105104a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  [_ N  /  n ]_ if ( S  < 
n ,  D ,  B )  =  if ( [. N  /  n ]. S  <  n ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B ) )
106 sbcbr2g 4496 . . . . . . . . . . . . . 14  |-  ( N  e.  NN0  ->  ( [. N  /  n ]. S  <  n  <->  S  <  [_ N  /  n ]_ n ) )
1071, 106syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( [. N  /  n ]. S  <  n  <->  S  <  [_ N  /  n ]_ n ) )
108 csbvarg 3841 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  [_ N  /  n ]_ n  =  N )
1091, 108syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  [_ N  /  n ]_ n  =  N
)
110109breq2d 4452 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  <  [_ N  /  n ]_ n  <->  S  <  N ) )
111107, 110bitrd 253 . . . . . . . . . . . 12  |-  ( ph  ->  ( [. N  /  n ]. S  <  n  <->  S  <  N ) )
112111ifbid 3954 . . . . . . . . . . 11  |-  ( ph  ->  if ( [. N  /  n ]. S  < 
n ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B )  =  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B ) )
113105, 112eqtrd 2501 . . . . . . . . . 10  |-  ( ph  ->  [_ N  /  n ]_ if ( S  < 
n ,  D ,  B )  =  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B ) )
114102, 103, 113ifbieq12d 3959 . . . . . . . . 9  |-  ( 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 ) ) )
115100, 114eqtrd 2501 . . . . . . . 8  |-  ( 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 ) ) )
11697, 98, 115ifbieq12d 3959 . . . . . . 7  |-  ( 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 ) ) ) )
11795, 116eqtrd 2501 . . . . . 6  |-  ( 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 ) ) ) )
118117eleq1d 2529 . . . . 5  |-  ( ph  ->  ( [_ N  /  n ]_ if ( n  =  0 ,  A ,  if ( n  =  S ,  C ,  if ( S  <  n ,  D ,  B ) ) )  e.  V  <->  if ( N  =  0 ,  [_ N  /  n ]_ A ,  if ( N  =  S ,  [_ N  /  n ]_ C ,  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B ) ) )  e.  V
) )
11993, 118mpbird 232 . . . 4  |-  ( ph  ->  [_ N  /  n ]_ if ( n  =  0 ,  A ,  if ( n  =  S ,  C ,  if ( S  <  n ,  D ,  B ) ) )  e.  V
)
1201, 119jca 532 . . 3  |-  ( ph  ->  ( N  e.  NN0  /\ 
[_ N  /  n ]_ if ( n  =  0 ,  A ,  if ( n  =  S ,  C ,  if ( S  <  n ,  D ,  B ) ) )  e.  V
) )
121 fvmptnn04if.g . . . 4  |-  G  =  ( n  e.  NN0  |->  if ( n  =  0 ,  A ,  if ( n  =  S ,  C ,  if ( S  <  n ,  D ,  B ) ) ) )
122121fvmpts 5943 . . 3  |-  ( ( 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 ) ) ) )
123120, 122syl 16 . 2  |-  ( ph  ->  ( G `  N
)  =  [_ N  /  n ]_ if ( n  =  0 ,  A ,  if ( n  =  S ,  C ,  if ( S  <  n ,  D ,  B ) ) ) )
124 eqcom 2469 . . . . . 6  |-  ( Y  =  [_ N  /  n ]_ A  <->  [_ N  /  n ]_ A  =  Y )
125124imbi2i 312 . . . . 5  |-  ( ( ( ph  /\  N  =  0 )  ->  Y  =  [_ N  /  n ]_ A )  <->  ( ( ph  /\  N  =  0 )  ->  [_ N  /  n ]_ A  =  Y ) )
1262, 125mpbi 208 . . . 4  |-  ( (
ph  /\  N  = 
0 )  ->  [_ N  /  n ]_ A  =  Y )
12726, 88ifeqda 3965 . . . . 5  |-  ( ( ( ph  /\  -.  N  =  0 )  /\  -.  N  =  S )  ->  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B )  =  Y )
12817, 127ifeqda 3965 . . . 4  |-  ( (
ph  /\  -.  N  =  0 )  ->  if ( N  =  S ,  [_ N  /  n ]_ C ,  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B ) )  =  Y )
129126, 128ifeqda 3965 . . 3  |-  ( ph  ->  if ( N  =  0 ,  [_ N  /  n ]_ A ,  if ( N  =  S ,  [_ N  /  n ]_ C ,  if ( S  <  N ,  [_ N  /  n ]_ D ,  [_ N  /  n ]_ B ) ) )  =  Y )
130117, 129eqtrd 2501 . 2  |-  ( ph  ->  [_ N  /  n ]_ if ( n  =  0 ,  A ,  if ( n  =  S ,  C ,  if ( S  <  n ,  D ,  B ) ) )  =  Y )
131123, 130eqtrd 2501 1  |-  ( ph  ->  ( G `  N
)  =  Y )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 968    = wceq 1374    e. wcel 1762    =/= wne 2655   [.wsbc 3324   [_csb 3428   ifcif 3932   class class class wbr 4440    |-> cmpt 4498   ` cfv 5579   RRcr 9480   0cc0 9481    < clt 9617    <_ cle 9618   NNcn 10525   NN0cn0 10784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-fal 1380  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6672  df-recs 7032  df-rdg 7066  df-er 7301  df-en 7507  df-dom 7508  df-sdom 7509  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-nn 10526  df-n0 10785
This theorem is referenced by:  fvmptnn04ifa  19111  fvmptnn04ifb  19112  fvmptnn04ifc  19113  fvmptnn04ifd  19114
  Copyright terms: Public domain W3C validator