Theorem monotoddzzfi 29280

Description: A function 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.)

Hypotheses

Ref	Expression
monotoddzzfi.1	|- ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR )
monotoddzzfi.2	|- ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) )
monotoddzzfi.3	|- ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) )

Assertion

Ref	Expression
monotoddzzfi	|- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( F ` A ) < ( F ` B ) ) )

Distinct variable groups:   ph, x, y   x, A, y   x, B, y   x, F, y

Proof of Theorem monotoddzzfi

Dummy variables a b are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5689	. . 3 |- ( a = b -> ( F ` a ) = ( F ` b ) )
2		fveq2 5689	. . 3 |- ( a = A -> ( F ` a ) = ( F ` A ) )
3		fveq2 5689	. . 3 |- ( a = B -> ( F ` a ) = ( F ` B ) )
4		zssre 10651	. . 3 |- ZZ C_ RR
5		eleq1 2501	. . . . . 6 |- ( x = a -> ( x e. ZZ <-> a e. ZZ ) )
6	5	anbi2d 703	. . . . 5 |- ( x = a -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ a e. ZZ ) ) )
7		fveq2 5689	. . . . . 6 |- ( x = a -> ( F ` x ) = ( F ` a ) )
8	7	eleq1d 2507	. . . . 5 |- ( x = a -> ( ( F ` x ) e. RR <-> ( F ` a ) e. RR ) )
9	6, 8	imbi12d 320	. . . 4 |- ( x = a -> ( ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR ) <-> ( ( ph /\ a e. ZZ ) -> ( F ` a ) e. RR ) ) )
10		monotoddzzfi.1	. . . 4 |- ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR )
11	9, 10	chvarv 1958	. . 3 |- ( ( ph /\ a e. ZZ ) -> ( F ` a ) e. RR )
12		elznn 10660	. . . . . . 7 |- ( a e. ZZ <-> ( a e. RR /\ ( a e. NN \/ -u a e. NN0 ) ) )
13	12	simprbi 464	. . . . . 6 |- ( a e. ZZ -> ( a e. NN \/ -u a e. NN0 ) )
14		elznn 10660	. . . . . . 7 |- ( b e. ZZ <-> ( b e. RR /\ ( b e. NN \/ -u b e. NN0 ) ) )
15	14	simprbi 464	. . . . . 6 |- ( b e. ZZ -> ( b e. NN \/ -u b e. NN0 ) )
16	13, 15	anim12i 566	. . . . 5 |- ( ( a e. ZZ /\ b e. ZZ ) -> ( ( a e. NN \/ -u a e. NN0 ) /\ ( b e. NN \/ -u b e. NN0 ) ) )
17	16	adantl 466	. . . 4 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a e. NN \/ -u a e. NN0 ) /\ ( b e. NN \/ -u b e. NN0 ) ) )
18		simpll 753	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ b e. NN ) ) -> ph )
19		nnnn0 10584	. . . . . . . 8 |- ( a e. NN -> a e. NN0 )
20	19	ad2antrl 727	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ b e. NN ) ) -> a e. NN0 )
21		nnnn0 10584	. . . . . . . 8 |- ( b e. NN -> b e. NN0 )
22	21	ad2antll 728	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ b e. NN ) ) -> b e. NN0 )
23		vex 2973	. . . . . . . 8 |- a e. _V
24		vex 2973	. . . . . . . 8 |- b e. _V
25		simpl 457	. . . . . . . . . . 11 |- ( ( x = a /\ y = b ) -> x = a )
26	25	eleq1d 2507	. . . . . . . . . 10 |- ( ( x = a /\ y = b ) -> ( x e. NN0 <-> a e. NN0 ) )
27		simpr 461	. . . . . . . . . . 11 |- ( ( x = a /\ y = b ) -> y = b )
28	27	eleq1d 2507	. . . . . . . . . 10 |- ( ( x = a /\ y = b ) -> ( y e. NN0 <-> b e. NN0 ) )
29	26, 28	3anbi23d 1292	. . . . . . . . 9 |- ( ( x = a /\ y = b ) -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ a e. NN0 /\ b e. NN0 ) ) )
30		breq12 4295	. . . . . . . . . 10 |- ( ( x = a /\ y = b ) -> ( x < y <-> a < b ) )
31		fveq2 5689	. . . . . . . . . . 11 |- ( y = b -> ( F ` y ) = ( F ` b ) )
32	7, 31	breqan12d 4305	. . . . . . . . . 10 |- ( ( x = a /\ y = b ) -> ( ( F ` x ) < ( F ` y ) <-> ( F ` a ) < ( F ` b ) ) )
33	30, 32	imbi12d 320	. . . . . . . . 9 |- ( ( x = a /\ y = b ) -> ( ( x < y -> ( F ` x ) < ( F ` y ) ) <-> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
34	29, 33	imbi12d 320	. . . . . . . 8 |- ( ( x = a /\ y = b ) -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) ) <-> ( ( ph /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) ) )
35		monotoddzzfi.3	. . . . . . . 8 |- ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) )
36	23, 24, 34, 35	vtocl2 3023	. . . . . . 7 |- ( ( ph /\ a e. NN0 /\ b e. NN0 ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
37	18, 20, 22, 36	syl3anc 1218	. . . . . 6 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ b e. NN ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
38	37	ex 434	. . . . 5 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a e. NN /\ b e. NN ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
39	11	adantrr 716	. . . . . . . . 9 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` a ) e. RR )
40	39	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` a ) e. RR )
41		0re 9384	. . . . . . . . 9 |- 0 e. RR
42	41	a1i 11	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 e. RR )
43		eleq1 2501	. . . . . . . . . . . . 13 |- ( x = b -> ( x e. ZZ <-> b e. ZZ ) )
44	43	anbi2d 703	. . . . . . . . . . . 12 |- ( x = b -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ b e. ZZ ) ) )
45		fveq2 5689	. . . . . . . . . . . . 13 |- ( x = b -> ( F ` x ) = ( F ` b ) )
46	45	eleq1d 2507	. . . . . . . . . . . 12 |- ( x = b -> ( ( F ` x ) e. RR <-> ( F ` b ) e. RR ) )
47	44, 46	imbi12d 320	. . . . . . . . . . 11 |- ( x = b -> ( ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR ) <-> ( ( ph /\ b e. ZZ ) -> ( F ` b ) e. RR ) ) )
48	47, 10	chvarv 1958	. . . . . . . . . 10 |- ( ( ph /\ b e. ZZ ) -> ( F ` b ) e. RR )
49	48	adantrl 715	. . . . . . . . 9 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` b ) e. RR )
50	49	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` b ) e. RR )
51	41	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 e. RR )
52		znegcl 10678	. . . . . . . . . . . . . . 15 |- ( a e. ZZ -> -u a e. ZZ )
53	52	ad2antrl 727	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> -u a e. ZZ )
54		negex 9606	. . . . . . . . . . . . . . 15 |- -u a e. _V
55		eleq1 2501	. . . . . . . . . . . . . . . . 17 |- ( x = -u a -> ( x e. ZZ <-> -u a e. ZZ ) )
56	55	anbi2d 703	. . . . . . . . . . . . . . . 16 |- ( x = -u a -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ -u a e. ZZ ) ) )
57		fveq2 5689	. . . . . . . . . . . . . . . . 17 |- ( x = -u a -> ( F ` x ) = ( F ` -u a ) )
58	57	eleq1d 2507	. . . . . . . . . . . . . . . 16 |- ( x = -u a -> ( ( F ` x ) e. RR <-> ( F ` -u a ) e. RR ) )
59	56, 58	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( x = -u a -> ( ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR ) <-> ( ( ph /\ -u a e. ZZ ) -> ( F ` -u a ) e. RR ) ) )
60	54, 59, 10	vtocl 3022	. . . . . . . . . . . . . 14 |- ( ( ph /\ -u a e. ZZ ) -> ( F ` -u a ) e. RR )
61	53, 60	syldan 470	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` -u a ) e. RR )
62	61	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ( F ` -u a ) e. RR )
63		0z 10655	. . . . . . . . . . . . . . . . . 18 |- 0 e. ZZ
64		c0ex 9378	. . . . . . . . . . . . . . . . . . 19 |- 0 e. _V
65		eleq1 2501	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = 0 -> ( x e. ZZ <-> 0 e. ZZ ) )
66	65	anbi2d 703	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( ( ph /\ x e. ZZ ) <-> ( ph /\ 0 e. ZZ ) ) )
67		fveq2 5689	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = 0 -> ( F ` x ) = ( F ` 0 ) )
68	67	eleq1d 2507	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( ( F ` x ) e. RR <-> ( F ` 0 ) e. RR ) )
69	66, 68	imbi12d 320	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> ( ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR ) <-> ( ( ph /\ 0 e. ZZ ) -> ( F ` 0 ) e. RR ) ) )
70	64, 69, 10	vtocl 3022	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ 0 e. ZZ ) -> ( F ` 0 ) e. RR )
71	63, 70	mpan2 671	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( F ` 0 ) e. RR )
72	71	recnd 9410	. . . . . . . . . . . . . . . 16 |- ( ph -> ( F ` 0 ) e. CC )
73		neg0 9653	. . . . . . . . . . . . . . . . . 18 |- -u 0 = 0
74	73	fveq2i 5692	. . . . . . . . . . . . . . . . 17 |- ( F ` -u 0 ) = ( F ` 0 )
75		negeq 9600	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = 0 -> -u x = -u 0 )
76	75	fveq2d 5693	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = 0 -> ( F ` -u x ) = ( F ` -u 0 ) )
77	67	negeqd 9602	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = 0 -> -u ( F ` x ) = -u ( F ` 0 ) )
78	76, 77	eqeq12d 2455	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( ( F ` -u x ) = -u ( F ` x ) <-> ( F ` -u 0 ) = -u ( F ` 0 ) ) )
79	66, 78	imbi12d 320	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> ( ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) ) <-> ( ( ph /\ 0 e. ZZ ) -> ( F ` -u 0 ) = -u ( F ` 0 ) ) ) )
80		monotoddzzfi.2	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) )
81	64, 79, 80	vtocl 3022	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ 0 e. ZZ ) -> ( F ` -u 0 ) = -u ( F ` 0 ) )
82	63, 81	mpan2 671	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( F ` -u 0 ) = -u ( F ` 0 ) )
83	74, 82	syl5eqr 2487	. . . . . . . . . . . . . . . 16 |- ( ph -> ( F ` 0 ) = -u ( F ` 0 ) )
84	72, 83	eqnegad 10051	. . . . . . . . . . . . . . 15 |- ( ph -> ( F ` 0 ) = 0 )
85	84	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` 0 ) = 0 )
86	85	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ( F ` 0 ) = 0 )
87		nngt0 10349	. . . . . . . . . . . . . . 15 |- ( -u a e. NN -> 0 < -u a )
88	87	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 < -u a )
89		simplll 757	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ph )
90		0nn0 10592	. . . . . . . . . . . . . . . 16 |- 0 e. NN0
91	90	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 e. NN0 )
92		simplrl 759	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> -u a e. NN0 )
93		simpl 457	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = 0 /\ y = -u a ) -> x = 0 )
94	93	eleq1d 2507	. . . . . . . . . . . . . . . . . 18 |- ( ( x = 0 /\ y = -u a ) -> ( x e. NN0 <-> 0 e. NN0 ) )
95		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = 0 /\ y = -u a ) -> y = -u a )
96	95	eleq1d 2507	. . . . . . . . . . . . . . . . . 18 |- ( ( x = 0 /\ y = -u a ) -> ( y e. NN0 <-> -u a e. NN0 ) )
97	94, 96	3anbi23d 1292	. . . . . . . . . . . . . . . . 17 |- ( ( x = 0 /\ y = -u a ) -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ 0 e. NN0 /\ -u a e. NN0 ) ) )
98		breq12 4295	. . . . . . . . . . . . . . . . . 18 |- ( ( x = 0 /\ y = -u a ) -> ( x < y <-> 0 < -u a ) )
99	93	fveq2d 5693	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = 0 /\ y = -u a ) -> ( F ` x ) = ( F ` 0 ) )
100	95	fveq2d 5693	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = 0 /\ y = -u a ) -> ( F ` y ) = ( F ` -u a ) )
101	99, 100	breq12d 4303	. . . . . . . . . . . . . . . . . 18 |- ( ( x = 0 /\ y = -u a ) -> ( ( F ` x ) < ( F ` y ) <-> ( F ` 0 ) < ( F ` -u a ) ) )
102	98, 101	imbi12d 320	. . . . . . . . . . . . . . . . 17 |- ( ( x = 0 /\ y = -u a ) -> ( ( x < y -> ( F ` x ) < ( F ` y ) ) <-> ( 0 < -u a -> ( F ` 0 ) < ( F ` -u a ) ) ) )
103	97, 102	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( ( x = 0 /\ y = -u a ) -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) ) <-> ( ( ph /\ 0 e. NN0 /\ -u a e. NN0 ) -> ( 0 < -u a -> ( F ` 0 ) < ( F ` -u a ) ) ) ) )
104	64, 54, 103, 35	vtocl2 3023	. . . . . . . . . . . . . . 15 |- ( ( ph /\ 0 e. NN0 /\ -u a e. NN0 ) -> ( 0 < -u a -> ( F ` 0 ) < ( F ` -u a ) ) )
105	89, 91, 92, 104	syl3anc 1218	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ( 0 < -u a -> ( F ` 0 ) < ( F ` -u a ) ) )
106	88, 105	mpd 15	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> ( F ` 0 ) < ( F ` -u a ) )
107	86, 106	eqbrtrrd 4312	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 < ( F ` -u a ) )
108	51, 62, 107	ltled 9520	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a e. NN ) -> 0 <_ ( F ` -u a ) )
109		0le0 10409	. . . . . . . . . . . . 13 |- 0 <_ 0
110	85	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a = 0 ) -> ( F ` 0 ) = 0 )
111	109, 110	syl5breqr 4326	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a = 0 ) -> 0 <_ ( F ` 0 ) )
112		fveq2 5689	. . . . . . . . . . . . . 14 |- ( -u a = 0 -> ( F ` -u a ) = ( F ` 0 ) )
113	112	breq2d 4302	. . . . . . . . . . . . 13 |- ( -u a = 0 -> ( 0 <_ ( F ` -u a ) <-> 0 <_ ( F ` 0 ) ) )
114	113	adantl 466	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a = 0 ) -> ( 0 <_ ( F ` -u a ) <-> 0 <_ ( F ` 0 ) ) )
115	111, 114	mpbird 232	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) /\ -u a = 0 ) -> 0 <_ ( F ` -u a ) )
116		elnn0 10579	. . . . . . . . . . . . 13 |- ( -u a e. NN0 <-> ( -u a e. NN \/ -u a = 0 ) )
117	116	biimpi 194	. . . . . . . . . . . 12 |- ( -u a e. NN0 -> ( -u a e. NN \/ -u a = 0 ) )
118	117	ad2antrl 727	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( -u a e. NN \/ -u a = 0 ) )
119	108, 115, 118	mpjaodan 784	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 <_ ( F ` -u a ) )
120		negeq 9600	. . . . . . . . . . . . . . . 16 |- ( x = a -> -u x = -u a )
121	120	fveq2d 5693	. . . . . . . . . . . . . . 15 |- ( x = a -> ( F ` -u x ) = ( F ` -u a ) )
122	7	negeqd 9602	. . . . . . . . . . . . . . 15 |- ( x = a -> -u ( F ` x ) = -u ( F ` a ) )
123	121, 122	eqeq12d 2455	. . . . . . . . . . . . . 14 |- ( x = a -> ( ( F ` -u x ) = -u ( F ` x ) <-> ( F ` -u a ) = -u ( F ` a ) ) )
124	6, 123	imbi12d 320	. . . . . . . . . . . . 13 |- ( x = a -> ( ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) ) <-> ( ( ph /\ a e. ZZ ) -> ( F ` -u a ) = -u ( F ` a ) ) ) )
125	124, 80	chvarv 1958	. . . . . . . . . . . 12 |- ( ( ph /\ a e. ZZ ) -> ( F ` -u a ) = -u ( F ` a ) )
126	125	adantrr 716	. . . . . . . . . . 11 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` -u a ) = -u ( F ` a ) )
127	126	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` -u a ) = -u ( F ` a ) )
128	119, 127	breqtrd 4314	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 <_ -u ( F ` a ) )
129	40	le0neg1d 9909	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( ( F ` a ) <_ 0 <-> 0 <_ -u ( F ` a ) ) )
130	128, 129	mpbird 232	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` a ) <_ 0 )
131	85	adantr 465	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` 0 ) = 0 )
132		nngt0 10349	. . . . . . . . . . 11 |- ( b e. NN -> 0 < b )
133	132	ad2antll 728	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 < b )
134		simpll 753	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ph )
135	90	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 e. NN0 )
136	21	ad2antll 728	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> b e. NN0 )
137		simpl 457	. . . . . . . . . . . . . . 15 |- ( ( x = 0 /\ y = b ) -> x = 0 )
138	137	eleq1d 2507	. . . . . . . . . . . . . 14 |- ( ( x = 0 /\ y = b ) -> ( x e. NN0 <-> 0 e. NN0 ) )
139		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( x = 0 /\ y = b ) -> y = b )
140	139	eleq1d 2507	. . . . . . . . . . . . . 14 |- ( ( x = 0 /\ y = b ) -> ( y e. NN0 <-> b e. NN0 ) )
141	138, 140	3anbi23d 1292	. . . . . . . . . . . . 13 |- ( ( x = 0 /\ y = b ) -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ 0 e. NN0 /\ b e. NN0 ) ) )
142		breq12 4295	. . . . . . . . . . . . . 14 |- ( ( x = 0 /\ y = b ) -> ( x < y <-> 0 < b ) )
143	67, 31	breqan12d 4305	. . . . . . . . . . . . . 14 |- ( ( x = 0 /\ y = b ) -> ( ( F ` x ) < ( F ` y ) <-> ( F ` 0 ) < ( F ` b ) ) )
144	142, 143	imbi12d 320	. . . . . . . . . . . . 13 |- ( ( x = 0 /\ y = b ) -> ( ( x < y -> ( F ` x ) < ( F ` y ) ) <-> ( 0 < b -> ( F ` 0 ) < ( F ` b ) ) ) )
145	141, 144	imbi12d 320	. . . . . . . . . . . 12 |- ( ( x = 0 /\ y = b ) -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) ) <-> ( ( ph /\ 0 e. NN0 /\ b e. NN0 ) -> ( 0 < b -> ( F ` 0 ) < ( F ` b ) ) ) ) )
146	64, 24, 145, 35	vtocl2 3023	. . . . . . . . . . 11 |- ( ( ph /\ 0 e. NN0 /\ b e. NN0 ) -> ( 0 < b -> ( F ` 0 ) < ( F ` b ) ) )
147	134, 135, 136, 146	syl3anc 1218	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( 0 < b -> ( F ` 0 ) < ( F ` b ) ) )
148	133, 147	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` 0 ) < ( F ` b ) )
149	131, 148	eqbrtrrd 4312	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> 0 < ( F ` b ) )
150	40, 42, 50, 130, 149	lelttrd 9527	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( F ` a ) < ( F ` b ) )
151	150	a1d 25	. . . . . 6 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ b e. NN ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
152	151	ex 434	. . . . 5 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( -u a e. NN0 /\ b e. NN ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
153		simp3 990	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) /\ a < b ) -> a < b )
154		zre 10648	. . . . . . . . . . . 12 |- ( b e. ZZ -> b e. RR )
155	154	adantl 466	. . . . . . . . . . 11 |- ( ( a e. ZZ /\ b e. ZZ ) -> b e. RR )
156	155	ad2antlr 726	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> b e. RR )
157		1re 9383	. . . . . . . . . . 11 |- 1 e. RR
158	157	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 1 e. RR )
159		nnre 10327	. . . . . . . . . . 11 |- ( a e. NN -> a e. RR )
160	159	ad2antrl 727	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> a e. RR )
161	41	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 0 e. RR )
162		nn0ge0 10603	. . . . . . . . . . . . 13 |- ( -u b e. NN0 -> 0 <_ -u b )
163	162	ad2antll 728	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 0 <_ -u b )
164	156	le0neg1d 9909	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> ( b <_ 0 <-> 0 <_ -u b ) )
165	163, 164	mpbird 232	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> b <_ 0 )
166		0le1 9861	. . . . . . . . . . . 12 |- 0 <_ 1
167	166	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 0 <_ 1 )
168	156, 161, 158, 165, 167	letrd 9526	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> b <_ 1 )
169		nnge1 10346	. . . . . . . . . . 11 |- ( a e. NN -> 1 <_ a )
170	169	ad2antrl 727	. . . . . . . . . 10 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> 1 <_ a )
171	156, 158, 160, 168, 170	letrd 9526	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> b <_ a )
172	156, 160	lenltd 9518	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> ( b <_ a <-> -. a < b ) )
173	171, 172	mpbid 210	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) ) -> -. a < b )
174	173	3adant3 1008	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) /\ a < b ) -> -. a < b )
175	153, 174	pm2.21dd 174	. . . . . 6 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( a e. NN /\ -u b e. NN0 ) /\ a < b ) -> ( F ` a ) < ( F ` b ) )
176	175	3exp 1186	. . . . 5 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a e. NN /\ -u b e. NN0 ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
177		negex 9606	. . . . . . . . . . . 12 |- -u b e. _V
178		simpl 457	. . . . . . . . . . . . . . 15 |- ( ( x = -u b /\ y = -u a ) -> x = -u b )
179	178	eleq1d 2507	. . . . . . . . . . . . . 14 |- ( ( x = -u b /\ y = -u a ) -> ( x e. NN0 <-> -u b e. NN0 ) )
180		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( x = -u b /\ y = -u a ) -> y = -u a )
181	180	eleq1d 2507	. . . . . . . . . . . . . 14 |- ( ( x = -u b /\ y = -u a ) -> ( y e. NN0 <-> -u a e. NN0 ) )
182	179, 181	3anbi23d 1292	. . . . . . . . . . . . 13 |- ( ( x = -u b /\ y = -u a ) -> ( ( ph /\ x e. NN0 /\ y e. NN0 ) <-> ( ph /\ -u b e. NN0 /\ -u a e. NN0 ) ) )
183		breq12 4295	. . . . . . . . . . . . . 14 |- ( ( x = -u b /\ y = -u a ) -> ( x < y <-> -u b < -u a ) )
184		fveq2 5689	. . . . . . . . . . . . . . 15 |- ( x = -u b -> ( F ` x ) = ( F ` -u b ) )
185		fveq2 5689	. . . . . . . . . . . . . . 15 |- ( y = -u a -> ( F ` y ) = ( F ` -u a ) )
186	184, 185	breqan12d 4305	. . . . . . . . . . . . . 14 |- ( ( x = -u b /\ y = -u a ) -> ( ( F ` x ) < ( F ` y ) <-> ( F ` -u b ) < ( F ` -u a ) ) )
187	183, 186	imbi12d 320	. . . . . . . . . . . . 13 |- ( ( x = -u b /\ y = -u a ) -> ( ( x < y -> ( F ` x ) < ( F ` y ) ) <-> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) ) )
188	182, 187	imbi12d 320	. . . . . . . . . . . 12 |- ( ( x = -u b /\ y = -u a ) -> ( ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) ) <-> ( ( ph /\ -u b e. NN0 /\ -u a e. NN0 ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) ) ) )
189	177, 54, 188, 35	vtocl2 3023	. . . . . . . . . . 11 |- ( ( ph /\ -u b e. NN0 /\ -u a e. NN0 ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) )
190	189	3com23 1193	. . . . . . . . . 10 |- ( ( ph /\ -u a e. NN0 /\ -u b e. NN0 ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) )
191	190	3expb 1188	. . . . . . . . 9 |- ( ( ph /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) )
192	191	adantlr 714	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( -u b < -u a -> ( F ` -u b ) < ( F ` -u a ) ) )
193		negeq 9600	. . . . . . . . . . . . . . 15 |- ( x = b -> -u x = -u b )
194	193	fveq2d 5693	. . . . . . . . . . . . . 14 |- ( x = b -> ( F ` -u x ) = ( F ` -u b ) )
195	45	negeqd 9602	. . . . . . . . . . . . . 14 |- ( x = b -> -u ( F ` x ) = -u ( F ` b ) )
196	194, 195	eqeq12d 2455	. . . . . . . . . . . . 13 |- ( x = b -> ( ( F ` -u x ) = -u ( F ` x ) <-> ( F ` -u b ) = -u ( F ` b ) ) )
197	44, 196	imbi12d 320	. . . . . . . . . . . 12 |- ( x = b -> ( ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) ) <-> ( ( ph /\ b e. ZZ ) -> ( F ` -u b ) = -u ( F ` b ) ) ) )
198	197, 80	chvarv 1958	. . . . . . . . . . 11 |- ( ( ph /\ b e. ZZ ) -> ( F ` -u b ) = -u ( F ` b ) )
199	198	adantrl 715	. . . . . . . . . 10 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( F ` -u b ) = -u ( F ` b ) )
200	199	adantr 465	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( F ` -u b ) = -u ( F ` b ) )
201	126	adantr 465	. . . . . . . . 9 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( F ` -u a ) = -u ( F ` a ) )
202	200, 201	breq12d 4303	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( ( F ` -u b ) < ( F ` -u a ) <-> -u ( F ` b ) < -u ( F ` a ) ) )
203	192, 202	sylibd 214	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( -u b < -u a -> -u ( F ` b ) < -u ( F ` a ) ) )
204		zre 10648	. . . . . . . . . 10 |- ( a e. ZZ -> a e. RR )
205	204	ad2antrl 727	. . . . . . . . 9 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. RR )
206	205	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> a e. RR )
207	155	ad2antlr 726	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> b e. RR )
208	206, 207	ltnegd 9915	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( a < b <-> -u b < -u a ) )
209	39	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( F ` a ) e. RR )
210	49	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( F ` b ) e. RR )
211	209, 210	ltnegd 9915	. . . . . . 7 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( ( F ` a ) < ( F ` b ) <-> -u ( F ` b ) < -u ( F ` a ) ) )
212	203, 208, 211	3imtr4d 268	. . . . . 6 |- ( ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) /\ ( -u a e. NN0 /\ -u b e. NN0 ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
213	212	ex 434	. . . . 5 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( -u a e. NN0 /\ -u b e. NN0 ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
214	38, 152, 176, 213	ccased 938	. . . 4 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( a e. NN \/ -u a e. NN0 ) /\ ( b e. NN \/ -u b e. NN0 ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) ) )
215	17, 214	mpd 15	. . 3 |- ( ( ph /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a < b -> ( F ` a ) < ( F ` b ) ) )
216	1, 2, 3, 4, 11, 215	ltord1 9864	. 2 |- ( ( ph /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( A < B <-> ( F ` A ) < ( F ` B ) ) )
217	216	3impb 1183	1 |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( F ` A ) < ( F ` B ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   class class class wbr 4290   ` cfv 5416   RRcr 9279   0cc0 9280   1c1 9281   < clt 9416   <_ cle 9417   -ucneg 9594   NNcn 10320   NN0cn0 10577   ZZcz 10644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pow 4468  ax-pr 4529  ax-un 6370  ax-resscn 9337  ax-1cn 9338  ax-icn 9339  ax-addcl 9340  ax-addrcl 9341  ax-mulcl 9342  ax-mulrcl 9343  ax-mulcom 9344  ax-addass 9345  ax-mulass 9346  ax-distr 9347  ax-i2m1 9348  ax-1ne0 9349  ax-1rid 9350  ax-rnegex 9351  ax-rrecex 9352  ax-cnre 9353  ax-pre-lttri 9354  ax-pre-lttrn 9355  ax-pre-ltadd 9356  ax-pre-mulgt0 9357

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3185  df-csb 3287  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-pss 3342  df-nul 3636  df-if 3790  df-pw 3860  df-sn 3876  df-pr 3878  df-tp 3880  df-op 3882  df-uni 4090  df-iun 4171  df-br 4291  df-opab 4349  df-mpt 4350  df-tr 4384  df-eprel 4630  df-id 4634  df-po 4639  df-so 4640  df-fr 4677  df-we 4679  df-ord 4720  df-on 4721  df-lim 4722  df-suc 4723  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-res 4850  df-ima 4851  df-iota 5379  df-fun 5418  df-fn 5419  df-f 5420  df-f1 5421  df-fo 5422  df-f1o 5423  df-fv 5424  df-riota 6050  df-ov 6092  df-oprab 6093  df-mpt2 6094  df-om 6475  df-recs 6830  df-rdg 6864  df-er 7099  df-en 7309  df-dom 7310  df-sdom 7311  df-pnf 9418  df-mnf 9419  df-xr 9420  df-ltxr 9421  df-le 9422  df-sub 9595  df-neg 9596  df-nn 10321  df-n0 10578  df-z 10645

This theorem is referenced by:  monotoddzz  29281