Metamath Proof Explorer

Theorem monotoddzz

Description: A function (given implicitly) which is odd and monotonic on NN0 is monotonic on ZZ . This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014)

Ref Expression
Hypotheses monotoddzz.1 
|- ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> E < F ) )
monotoddzz.2 
|- ( ( ph /\ x e. ZZ ) -> E e. RR )
monotoddzz.3 
|- ( ( ph /\ y e. ZZ ) -> G = -u F )
monotoddzz.4 
|- ( x = A -> E = C )
monotoddzz.5 
|- ( x = B -> E = D )
monotoddzz.6 
|- ( x = y -> E = F )
monotoddzz.7 
|- ( x = -u y -> E = G )
Assertion monotoddzz 
|- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> C < D ) )

Proof

Step Hyp Ref Expression
1 monotoddzz.1 
 |-  ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> E < F ) )
2 monotoddzz.2 
 |-  ( ( ph /\ x e. ZZ ) -> E e. RR )
3 monotoddzz.3 
 |-  ( ( ph /\ y e. ZZ ) -> G = -u F )
4 monotoddzz.4 
 |-  ( x = A -> E = C )
5 monotoddzz.5 
 |-  ( x = B -> E = D )
6 monotoddzz.6 
 |-  ( x = y -> E = F )
7 monotoddzz.7 
 |-  ( x = -u y -> E = G )
8 nfv 
 |-  F/ x ( ph /\ a e. ZZ )
9 nffvmpt1 
 |-  F/_ x ( ( x e. ZZ |-> E ) ` a )
10 9 nfel1 
 |-  F/ x ( ( x e. ZZ |-> E ) ` a ) e. RR
11 8 10 nfim 
 |-  F/ x ( ( ph /\ a e. ZZ ) -> ( ( x e. ZZ |-> E ) ` a ) e. RR )
12 eleq1 
 |-  ( x = a -> ( x e. ZZ <-> a e. ZZ ) )
13 12 anbi2d 
 |-  ( x = a -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ a e. ZZ ) ) )
14 fveq2 
 |-  ( x = a -> ( ( x e. ZZ |-> E ) ` x ) = ( ( x e. ZZ |-> E ) ` a ) )
15 14 eleq1d 
 |-  ( x = a -> ( ( ( x e. ZZ |-> E ) ` x ) e. RR <-> ( ( x e. ZZ |-> E ) ` a ) e. RR ) )
16 13 15 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ x e. ZZ ) -> ( ( x e. ZZ |-> E ) ` x ) e. RR ) <-> ( ( ph /\ a e. ZZ ) -> ( ( x e. ZZ |-> E ) ` a ) e. RR ) ) )
17 simpr 
 |-  ( ( ph /\ x e. ZZ ) -> x e. ZZ )
18 eqid 
 |-  ( x e. ZZ |-> E ) = ( x e. ZZ |-> E )
19 18 fvmpt2 
 |-  ( ( x e. ZZ /\ E e. RR ) -> ( ( x e. ZZ |-> E ) ` x ) = E )
20 17 2 19 syl2anc 
 |-  ( ( ph /\ x e. ZZ ) -> ( ( x e. ZZ |-> E ) ` x ) = E )
21 20 2 eqeltrd 
 |-  ( ( ph /\ x e. ZZ ) -> ( ( x e. ZZ |-> E ) ` x ) e. RR )
22 11 16 21 chvarfv 
 |-  ( ( ph /\ a e. ZZ ) -> ( ( x e. ZZ |-> E ) ` a ) e. RR )
23 eleq1 
 |-  ( y = a -> ( y e. ZZ <-> a e. ZZ ) )
24 23 anbi2d 
 |-  ( y = a -> ( ( ph /\ y e. ZZ ) <-> ( ph /\ a e. ZZ ) ) )
25 negeq 
 |-  ( y = a -> -u y = -u a )
26 25 fveq2d 
 |-  ( y = a -> ( ( x e. ZZ |-> E ) ` -u y ) = ( ( x e. ZZ |-> E ) ` -u a ) )
27 fveq2 
 |-  ( y = a -> ( ( x e. ZZ |-> E ) ` y ) = ( ( x e. ZZ |-> E ) ` a ) )
28 27 negeqd 
 |-  ( y = a -> -u ( ( x e. ZZ |-> E ) ` y ) = -u ( ( x e. ZZ |-> E ) ` a ) )
29 26 28 eqeq12d 
 |-  ( y = a -> ( ( ( x e. ZZ |-> E ) ` -u y ) = -u ( ( x e. ZZ |-> E ) ` y ) <-> ( ( x e. ZZ |-> E ) ` -u a ) = -u ( ( x e. ZZ |-> E ) ` a ) ) )
30 24 29 imbi12d 
 |-  ( y = a -> ( ( ( ph /\ y e. ZZ ) -> ( ( x e. ZZ |-> E ) ` -u y ) = -u ( ( x e. ZZ |-> E ) ` y ) ) <-> ( ( ph /\ a e. ZZ ) -> ( ( x e. ZZ |-> E ) ` -u a ) = -u ( ( x e. ZZ |-> E ) ` a ) ) ) )
31 znegcl 
 |-  ( y e. ZZ -> -u y e. ZZ )
32 31 adantl 
 |-  ( ( ph /\ y e. ZZ ) -> -u y e. ZZ )
33 negex 
 |-  -u y e. _V
34 eleq1 
 |-  ( x = -u y -> ( x e. ZZ <-> -u y e. ZZ ) )
35 34 anbi2d 
 |-  ( x = -u y -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ -u y e. ZZ ) ) )
36 7 eleq1d 
 |-  ( x = -u y -> ( E e. RR <-> G e. RR ) )
37 35 36 imbi12d 
 |-  ( x = -u y -> ( ( ( ph /\ x e. ZZ ) -> E e. RR ) <-> ( ( ph /\ -u y e. ZZ ) -> G e. RR ) ) )
38 33 37 2 vtocl 
 |-  ( ( ph /\ -u y e. ZZ ) -> G e. RR )
39 31 38 sylan2 
 |-  ( ( ph /\ y e. ZZ ) -> G e. RR )
40 18 7 32 39 fvmptd3 
 |-  ( ( ph /\ y e. ZZ ) -> ( ( x e. ZZ |-> E ) ` -u y ) = G )
41 simpr 
 |-  ( ( ph /\ y e. ZZ ) -> y e. ZZ )
42 eleq1 
 |-  ( x = y -> ( x e. ZZ <-> y e. ZZ ) )
43 42 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ y e. ZZ ) ) )
44 6 eleq1d 
 |-  ( x = y -> ( E e. RR <-> F e. RR ) )
45 43 44 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. ZZ ) -> E e. RR ) <-> ( ( ph /\ y e. ZZ ) -> F e. RR ) ) )
46 45 2 chvarvv 
 |-  ( ( ph /\ y e. ZZ ) -> F e. RR )
47 18 6 41 46 fvmptd3 
 |-  ( ( ph /\ y e. ZZ ) -> ( ( x e. ZZ |-> E ) ` y ) = F )
48 47 negeqd 
 |-  ( ( ph /\ y e. ZZ ) -> -u ( ( x e. ZZ |-> E ) ` y ) = -u F )
49 3 40 48 3eqtr4d 
 |-  ( ( ph /\ y e. ZZ ) -> ( ( x e. ZZ |-> E ) ` -u y ) = -u ( ( x e. ZZ |-> E ) ` y ) )
50 30 49 chvarvv 
 |-  ( ( ph /\ a e. ZZ ) -> ( ( x e. ZZ |-> E ) ` -u a ) = -u ( ( x e. ZZ |-> E ) ` a ) )
51 nfv 
 |-  F/ x ( ph /\ a e. NN0 /\ b e. NN0 )
52 nfv 
 |-  F/ x a < b
53 nfcv 
 |-  F/_ x <
54 nffvmpt1 
 |-  F/_ x ( ( x e. ZZ |-> E ) ` b )
55 9 53 54 nfbr 
 |-  F/ x ( ( x e. ZZ |-> E ) ` a ) < ( ( x e. ZZ |-> E ) ` b )
56 52 55 nfim 
 |-  F/ x ( a < b -> ( ( x e. ZZ |-> E ) ` a ) < ( ( x e. ZZ |-> E ) ` b ) )
57 51 56 nfim 
 |-  F/ x ( ( ph /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( ( x e. ZZ |-> E ) ` a ) < ( ( x e. ZZ |-> E ) ` b ) ) )
58 eleq1 
 |-  ( x = a -> ( x e. NN0 <-> a e. NN0 ) )
59 58 3anbi2d 
 |-  ( x = a -> ( ( ph /\ x e. NN0 /\ b e. NN0 ) <-> ( ph /\ a e. NN0 /\ b e. NN0 ) ) )
60 breq1 
 |-  ( x = a -> ( x < b <-> a < b ) )
61 14 breq1d 
 |-  ( x = a -> ( ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` b ) <-> ( ( x e. ZZ |-> E ) ` a ) < ( ( x e. ZZ |-> E ) ` b ) ) )
62 60 61 imbi12d 
 |-  ( x = a -> ( ( x < b -> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` b ) ) <-> ( a < b -> ( ( x e. ZZ |-> E ) ` a ) < ( ( x e. ZZ |-> E ) ` b ) ) ) )
63 59 62 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ x e. NN0 /\ b e. NN0 ) -> ( x < b -> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` b ) ) ) <-> ( ( ph /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( ( x e. ZZ |-> E ) ` a ) < ( ( x e. ZZ |-> E ) ` b ) ) ) ) )
64 eleq1 
 |-  ( y = b -> ( y e. NN0 <-> b e. NN0 ) )
65 64 3anbi3d 
 |-  ( y = b -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ x e. NN0 /\ b e. NN0 ) ) )
66 breq2 
 |-  ( y = b -> ( x < y <-> x < b ) )
67 fveq2 
 |-  ( y = b -> ( ( x e. ZZ |-> E ) ` y ) = ( ( x e. ZZ |-> E ) ` b ) )
68 67 breq2d 
 |-  ( y = b -> ( ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` y ) <-> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` b ) ) )
69 66 68 imbi12d 
 |-  ( y = b -> ( ( x < y -> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` y ) ) <-> ( x < b -> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` b ) ) ) )
70 65 69 imbi12d 
 |-  ( y = b -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` y ) ) ) <-> ( ( ph /\ x e. NN0 /\ b e. NN0 ) -> ( x < b -> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` b ) ) ) ) )
71 nn0z 
 |-  ( x e. NN0 -> x e. ZZ )
72 71 20 sylan2 
 |-  ( ( ph /\ x e. NN0 ) -> ( ( x e. ZZ |-> E ) ` x ) = E )
73 72 3adant3 
 |-  ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( ( x e. ZZ |-> E ) ` x ) = E )
74 nfv 
 |-  F/ x ( ph /\ y e. NN0 )
75 nffvmpt1 
 |-  F/_ x ( ( x e. ZZ |-> E ) ` y )
76 75 nfeq1 
 |-  F/ x ( ( x e. ZZ |-> E ) ` y ) = F
77 74 76 nfim 
 |-  F/ x ( ( ph /\ y e. NN0 ) -> ( ( x e. ZZ |-> E ) ` y ) = F )
78 eleq1 
 |-  ( x = y -> ( x e. NN0 <-> y e. NN0 ) )
79 78 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. NN0 ) <-> ( ph /\ y e. NN0 ) ) )
80 fveq2 
 |-  ( x = y -> ( ( x e. ZZ |-> E ) ` x ) = ( ( x e. ZZ |-> E ) ` y ) )
81 80 6 eqeq12d 
 |-  ( x = y -> ( ( ( x e. ZZ |-> E ) ` x ) = E <-> ( ( x e. ZZ |-> E ) ` y ) = F ) )
82 79 81 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. NN0 ) -> ( ( x e. ZZ |-> E ) ` x ) = E ) <-> ( ( ph /\ y e. NN0 ) -> ( ( x e. ZZ |-> E ) ` y ) = F ) ) )
83 77 82 72 chvarfv 
 |-  ( ( ph /\ y e. NN0 ) -> ( ( x e. ZZ |-> E ) ` y ) = F )
84 83 3adant2 
 |-  ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( ( x e. ZZ |-> E ) ` y ) = F )
85 73 84 breq12d 
 |-  ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` y ) <-> E < F ) )
86 1 85 sylibrd 
 |-  ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` y ) ) )
87 70 86 chvarvv 
 |-  ( ( ph /\ x e. NN0 /\ b e. NN0 ) -> ( x < b -> ( ( x e. ZZ |-> E ) ` x ) < ( ( x e. ZZ |-> E ) ` b ) ) )
88 57 63 87 chvarfv 
 |-  ( ( ph /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( ( x e. ZZ |-> E ) ` a ) < ( ( x e. ZZ |-> E ) ` b ) ) )
89 22 50 88 monotoddzzfi 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( ( x e. ZZ |-> E ) ` A ) < ( ( x e. ZZ |-> E ) ` B ) ) )
90 simp2 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> A e. ZZ )
91 eleq1 
 |-  ( x = A -> ( x e. ZZ <-> A e. ZZ ) )
92 91 anbi2d 
 |-  ( x = A -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ A e. ZZ ) ) )
93 4 eleq1d 
 |-  ( x = A -> ( E e. RR <-> C e. RR ) )
94 92 93 imbi12d 
 |-  ( x = A -> ( ( ( ph /\ x e. ZZ ) -> E e. RR ) <-> ( ( ph /\ A e. ZZ ) -> C e. RR ) ) )
95 94 2 vtoclg 
 |-  ( A e. ZZ -> ( ( ph /\ A e. ZZ ) -> C e. RR ) )
96 95 anabsi7 
 |-  ( ( ph /\ A e. ZZ ) -> C e. RR )
97 96 3adant3 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> C e. RR )
98 18 4 90 97 fvmptd3 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( ( x e. ZZ |-> E ) ` A ) = C )
99 simp3 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> B e. ZZ )
100 eleq1 
 |-  ( x = B -> ( x e. ZZ <-> B e. ZZ ) )
101 100 anbi2d 
 |-  ( x = B -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ B e. ZZ ) ) )
102 5 eleq1d 
 |-  ( x = B -> ( E e. RR <-> D e. RR ) )
103 101 102 imbi12d 
 |-  ( x = B -> ( ( ( ph /\ x e. ZZ ) -> E e. RR ) <-> ( ( ph /\ B e. ZZ ) -> D e. RR ) ) )
104 103 2 vtoclg 
 |-  ( B e. ZZ -> ( ( ph /\ B e. ZZ ) -> D e. RR ) )
105 104 anabsi7 
 |-  ( ( ph /\ B e. ZZ ) -> D e. RR )
106 105 3adant2 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> D e. RR )
107 18 5 99 106 fvmptd3 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( ( x e. ZZ |-> E ) ` B ) = D )
108 98 107 breq12d 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( ( ( x e. ZZ |-> E ) ` A ) < ( ( x e. ZZ |-> E ) ` B ) <-> C < D ) )
109 89 108 bitrd 
 |-  ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> C < D ) )