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 |
2
|
3ad2ant1 |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> S e. NN ) |
5 |
3
|
3ad2ant1 |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> N e. NN0 ) |
6 |
|
simp3 |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> [_ N / n ]_ D e. V ) |
7 |
|
0red |
|- ( ph -> 0 e. RR ) |
8 |
2
|
nnred |
|- ( ph -> S e. RR ) |
9 |
2
|
nngt0d |
|- ( ph -> 0 < S ) |
10 |
7 8 9
|
ltnsymd |
|- ( ph -> -. S < 0 ) |
11 |
10
|
adantr |
|- ( ( ph /\ N = 0 ) -> -. S < 0 ) |
12 |
|
breq2 |
|- ( N = 0 -> ( S < N <-> S < 0 ) ) |
13 |
12
|
notbid |
|- ( N = 0 -> ( -. S < N <-> -. S < 0 ) ) |
14 |
13
|
adantl |
|- ( ( ph /\ N = 0 ) -> ( -. S < N <-> -. S < 0 ) ) |
15 |
11 14
|
mpbird |
|- ( ( ph /\ N = 0 ) -> -. S < N ) |
16 |
15
|
pm2.21d |
|- ( ( ph /\ N = 0 ) -> ( S < N -> [_ N / n ]_ D = [_ N / n ]_ A ) ) |
17 |
16
|
impancom |
|- ( ( ph /\ S < N ) -> ( N = 0 -> [_ N / n ]_ D = [_ N / n ]_ A ) ) |
18 |
17
|
3adant3 |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> ( N = 0 -> [_ N / n ]_ D = [_ N / n ]_ A ) ) |
19 |
18
|
imp |
|- ( ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) /\ N = 0 ) -> [_ N / n ]_ D = [_ N / n ]_ A ) |
20 |
3
|
nn0red |
|- ( ph -> N e. RR ) |
21 |
|
ltnsym |
|- ( ( S e. RR /\ N e. RR ) -> ( S < N -> -. N < S ) ) |
22 |
8 20 21
|
syl2anc |
|- ( ph -> ( S < N -> -. N < S ) ) |
23 |
22
|
imp |
|- ( ( ph /\ S < N ) -> -. N < S ) |
24 |
23
|
3adant3 |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> -. N < S ) |
25 |
24
|
pm2.21d |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> ( N < S -> [_ N / n ]_ D = [_ N / n ]_ B ) ) |
26 |
25
|
a1d |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> ( 0 < N -> ( N < S -> [_ N / n ]_ D = [_ N / n ]_ B ) ) ) |
27 |
26
|
3imp |
|- ( ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) /\ 0 < N /\ N < S ) -> [_ N / n ]_ D = [_ N / n ]_ B ) |
28 |
20 8
|
lttri3d |
|- ( ph -> ( N = S <-> ( -. N < S /\ -. S < N ) ) ) |
29 |
28
|
simplbda |
|- ( ( ph /\ N = S ) -> -. S < N ) |
30 |
29
|
pm2.21d |
|- ( ( ph /\ N = S ) -> ( S < N -> [_ N / n ]_ D = [_ N / n ]_ C ) ) |
31 |
30
|
impancom |
|- ( ( ph /\ S < N ) -> ( N = S -> [_ N / n ]_ D = [_ N / n ]_ C ) ) |
32 |
31
|
3adant3 |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> ( N = S -> [_ N / n ]_ D = [_ N / n ]_ C ) ) |
33 |
32
|
imp |
|- ( ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) /\ N = S ) -> [_ N / n ]_ D = [_ N / n ]_ C ) |
34 |
|
eqidd |
|- ( ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) /\ S < N ) -> [_ N / n ]_ D = [_ N / n ]_ D ) |
35 |
1 4 5 6 19 27 33 34
|
fvmptnn04if |
|- ( ( ph /\ S < N /\ [_ N / n ]_ D e. V ) -> ( G ` N ) = [_ N / n ]_ D ) |