monotoddzzfi

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)

	Ref	Expression
Hypotheses	monotoddzzfi.1	$⊢ (φ \land x \in ℤ) \to F (x) \in ℝ$
	monotoddzzfi.2	$⊢ (φ \land x \in ℤ) \to F (- x) = - F (x)$
	monotoddzzfi.3	$⊢ (φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \to (x < y \to F (x) < F (y))$
Assertion	monotoddzzfi	$⊢ (φ \land A \in ℤ \land B \in ℤ) \to (A < B \leftrightarrow F (A) < F (B))$

Proof

Step	Hyp	Ref	Expression
1		monotoddzzfi.1	$⊢ (φ \land x \in ℤ) \to F (x) \in ℝ$
2		monotoddzzfi.2	$⊢ (φ \land x \in ℤ) \to F (- x) = - F (x)$
3		monotoddzzfi.3	$⊢ (φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \to (x < y \to F (x) < F (y))$
4		fveq2	$⊢ a = b \to F (a) = F (b)$
5		fveq2	$⊢ a = A \to F (a) = F (A)$
6		fveq2	$⊢ a = B \to F (a) = F (B)$
7		zssre	$⊢ ℤ \subseteq ℝ$
8		eleq1	$⊢ x = a \to (x \in ℤ \leftrightarrow a \in ℤ)$
9	8	anbi2d	$⊢ x = a \to ((φ \land x \in ℤ) \leftrightarrow (φ \land a \in ℤ))$
10		fveq2	$⊢ x = a \to F (x) = F (a)$
11	10	eleq1d	$⊢ x = a \to (F (x) \in ℝ \leftrightarrow F (a) \in ℝ)$
12	9 11	imbi12d	$⊢ x = a \to (((φ \land x \in ℤ) \to F (x) \in ℝ) \leftrightarrow ((φ \land a \in ℤ) \to F (a) \in ℝ))$
13	12 1	chvarvv	$⊢ (φ \land a \in ℤ) \to F (a) \in ℝ$
14		elznn	$⊢ a \in ℤ \leftrightarrow (a \in ℝ \land (a \in ℕ \lor - a \in ℕ_{0}))$
15	14	simprbi	$⊢ a \in ℤ \to (a \in ℕ \lor - a \in ℕ_{0})$
16		elznn	$⊢ b \in ℤ \leftrightarrow (b \in ℝ \land (b \in ℕ \lor - b \in ℕ_{0}))$
17	16	simprbi	$⊢ b \in ℤ \to (b \in ℕ \lor - b \in ℕ_{0})$
18	15 17	anim12i	$⊢ (a \in ℤ \land b \in ℤ) \to ((a \in ℕ \lor - a \in ℕ_{0}) \land (b \in ℕ \lor - b \in ℕ_{0}))$
19	18	adantl	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to ((a \in ℕ \lor - a \in ℕ_{0}) \land (b \in ℕ \lor - b \in ℕ_{0}))$
20		simpll	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land b \in ℕ)) \to φ$
21		nnnn0	$⊢ a \in ℕ \to a \in ℕ_{0}$
22	21	ad2antrl	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land b \in ℕ)) \to a \in ℕ_{0}$
23		nnnn0	$⊢ b \in ℕ \to b \in ℕ_{0}$
24	23	ad2antll	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land b \in ℕ)) \to b \in ℕ_{0}$
25		vex	$⊢ a \in V$
26		vex	$⊢ b \in V$
27		simpl	$⊢ (x = a \land y = b) \to x = a$
28	27	eleq1d	$⊢ (x = a \land y = b) \to (x \in ℕ_{0} \leftrightarrow a \in ℕ_{0})$
29		simpr	$⊢ (x = a \land y = b) \to y = b$
30	29	eleq1d	$⊢ (x = a \land y = b) \to (y \in ℕ_{0} \leftrightarrow b \in ℕ_{0})$
31	28 30	3anbi23d	$⊢ (x = a \land y = b) \to ((φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \leftrightarrow (φ \land a \in ℕ_{0} \land b \in ℕ_{0}))$
32		breq12	$⊢ (x = a \land y = b) \to (x < y \leftrightarrow a < b)$
33		fveq2	$⊢ y = b \to F (y) = F (b)$
34	10 33	breqan12d	$⊢ (x = a \land y = b) \to (F (x) < F (y) \leftrightarrow F (a) < F (b))$
35	32 34	imbi12d	$⊢ (x = a \land y = b) \to ((x < y \to F (x) < F (y)) \leftrightarrow (a < b \to F (a) < F (b)))$
36	31 35	imbi12d	$⊢ (x = a \land y = b) \to (((φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \to (x < y \to F (x) < F (y))) \leftrightarrow ((φ \land a \in ℕ_{0} \land b \in ℕ_{0}) \to (a < b \to F (a) < F (b))))$
37	25 26 36 3	vtocl2	$⊢ (φ \land a \in ℕ_{0} \land b \in ℕ_{0}) \to (a < b \to F (a) < F (b))$
38	20 22 24 37	syl3anc	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land b \in ℕ)) \to (a < b \to F (a) < F (b))$
39	38	ex	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to ((a \in ℕ \land b \in ℕ) \to (a < b \to F (a) < F (b)))$
40	13	adantrr	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to F (a) \in ℝ$
41	40	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to F (a) \in ℝ$
42		0red	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to 0 \in ℝ$
43		eleq1	$⊢ x = b \to (x \in ℤ \leftrightarrow b \in ℤ)$
44	43	anbi2d	$⊢ x = b \to ((φ \land x \in ℤ) \leftrightarrow (φ \land b \in ℤ))$
45		fveq2	$⊢ x = b \to F (x) = F (b)$
46	45	eleq1d	$⊢ x = b \to (F (x) \in ℝ \leftrightarrow F (b) \in ℝ)$
47	44 46	imbi12d	$⊢ x = b \to (((φ \land x \in ℤ) \to F (x) \in ℝ) \leftrightarrow ((φ \land b \in ℤ) \to F (b) \in ℝ))$
48	47 1	chvarvv	$⊢ (φ \land b \in ℤ) \to F (b) \in ℝ$
49	48	adantrl	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to F (b) \in ℝ$
50	49	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to F (b) \in ℝ$
51		0red	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to 0 \in ℝ$
52		znegcl	$⊢ a \in ℤ \to - a \in ℤ$
53	52	ad2antrl	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to - a \in ℤ$
54		negex	$⊢ - a \in V$
55		eleq1	$⊢ x = - a \to (x \in ℤ \leftrightarrow - a \in ℤ)$
56	55	anbi2d	$⊢ x = - a \to ((φ \land x \in ℤ) \leftrightarrow (φ \land - a \in ℤ))$
57		fveq2	$⊢ x = - a \to F (x) = F (- a)$
58	57	eleq1d	$⊢ x = - a \to (F (x) \in ℝ \leftrightarrow F (- a) \in ℝ)$
59	56 58	imbi12d	$⊢ x = - a \to (((φ \land x \in ℤ) \to F (x) \in ℝ) \leftrightarrow ((φ \land - a \in ℤ) \to F (- a) \in ℝ))$
60	54 59 1	vtocl	$⊢ (φ \land - a \in ℤ) \to F (- a) \in ℝ$
61	53 60	syldan	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to F (- a) \in ℝ$
62	61	ad2antrr	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to F (- a) \in ℝ$
63		0z	$⊢ 0 \in ℤ$
64		c0ex	$⊢ 0 \in V$
65		eleq1	$⊢ x = 0 \to (x \in ℤ \leftrightarrow 0 \in ℤ)$
66	65	anbi2d	$⊢ x = 0 \to ((φ \land x \in ℤ) \leftrightarrow (φ \land 0 \in ℤ))$
67		fveq2	$⊢ x = 0 \to F (x) = F (0)$
68	67	eleq1d	$⊢ x = 0 \to (F (x) \in ℝ \leftrightarrow F (0) \in ℝ)$
69	66 68	imbi12d	$⊢ x = 0 \to (((φ \land x \in ℤ) \to F (x) \in ℝ) \leftrightarrow ((φ \land 0 \in ℤ) \to F (0) \in ℝ))$
70	64 69 1	vtocl	$⊢ (φ \land 0 \in ℤ) \to F (0) \in ℝ$
71	63 70	mpan2	$⊢ φ \to F (0) \in ℝ$
72	71	recnd	$⊢ φ \to F (0) \in ℂ$
73		neg0	$⊢ - 0 = 0$
74	73	fveq2i	$⊢ F (- 0) = F (0)$
75		negeq	$⊢ x = 0 \to - x = - 0$
76	75	fveq2d	$⊢ x = 0 \to F (- x) = F (- 0)$
77	67	negeqd	$⊢ x = 0 \to - F (x) = - F (0)$
78	76 77	eqeq12d	$⊢ x = 0 \to (F (- x) = - F (x) \leftrightarrow F (- 0) = - F (0))$
79	66 78	imbi12d	$⊢ x = 0 \to (((φ \land x \in ℤ) \to F (- x) = - F (x)) \leftrightarrow ((φ \land 0 \in ℤ) \to F (- 0) = - F (0)))$
80	64 79 2	vtocl	$⊢ (φ \land 0 \in ℤ) \to F (- 0) = - F (0)$
81	63 80	mpan2	$⊢ φ \to F (- 0) = - F (0)$
82	74 81	eqtr3id	$⊢ φ \to F (0) = - F (0)$
83	72 82	eqnegad	$⊢ φ \to F (0) = 0$
84	83	adantr	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to F (0) = 0$
85	84	ad2antrr	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to F (0) = 0$
86		nngt0	$⊢ - a \in ℕ \to 0 < - a$
87	86	adantl	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to 0 < - a$
88		simplll	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to φ$
89		0nn0	$⊢ 0 \in ℕ_{0}$
90	89	a1i	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to 0 \in ℕ_{0}$
91		simplrl	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to - a \in ℕ_{0}$
92		simpl	$⊢ (x = 0 \land y = - a) \to x = 0$
93	92	eleq1d	$⊢ (x = 0 \land y = - a) \to (x \in ℕ_{0} \leftrightarrow 0 \in ℕ_{0})$
94		simpr	$⊢ (x = 0 \land y = - a) \to y = - a$
95	94	eleq1d	$⊢ (x = 0 \land y = - a) \to (y \in ℕ_{0} \leftrightarrow - a \in ℕ_{0})$
96	93 95	3anbi23d	$⊢ (x = 0 \land y = - a) \to ((φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \leftrightarrow (φ \land 0 \in ℕ_{0} \land - a \in ℕ_{0}))$
97		breq12	$⊢ (x = 0 \land y = - a) \to (x < y \leftrightarrow 0 < - a)$
98	92	fveq2d	$⊢ (x = 0 \land y = - a) \to F (x) = F (0)$
99	94	fveq2d	$⊢ (x = 0 \land y = - a) \to F (y) = F (- a)$
100	98 99	breq12d	$⊢ (x = 0 \land y = - a) \to (F (x) < F (y) \leftrightarrow F (0) < F (- a))$
101	97 100	imbi12d	$⊢ (x = 0 \land y = - a) \to ((x < y \to F (x) < F (y)) \leftrightarrow (0 < - a \to F (0) < F (- a)))$
102	96 101	imbi12d	$⊢ (x = 0 \land y = - a) \to (((φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \to (x < y \to F (x) < F (y))) \leftrightarrow ((φ \land 0 \in ℕ_{0} \land - a \in ℕ_{0}) \to (0 < - a \to F (0) < F (- a))))$
103	64 54 102 3	vtocl2	$⊢ (φ \land 0 \in ℕ_{0} \land - a \in ℕ_{0}) \to (0 < - a \to F (0) < F (- a))$
104	88 90 91 103	syl3anc	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to (0 < - a \to F (0) < F (- a))$
105	87 104	mpd	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to F (0) < F (- a)$
106	85 105	eqbrtrrd	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to 0 < F (- a)$
107	51 62 106	ltled	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a \in ℕ) \to 0 \leq F (- a)$
108		0le0	$⊢ 0 \leq 0$
109	84	ad2antrr	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a = 0) \to F (0) = 0$
110	108 109	breqtrrid	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a = 0) \to 0 \leq F (0)$
111		fveq2	$⊢ - a = 0 \to F (- a) = F (0)$
112	111	breq2d	$⊢ - a = 0 \to (0 \leq F (- a) \leftrightarrow 0 \leq F (0))$
113	112	adantl	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a = 0) \to (0 \leq F (- a) \leftrightarrow 0 \leq F (0))$
114	110 113	mpbird	$⊢ (((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \land - a = 0) \to 0 \leq F (- a)$
115		elnn0	$⊢ - a \in ℕ_{0} \leftrightarrow (- a \in ℕ \lor - a = 0)$
116	115	biimpi	$⊢ - a \in ℕ_{0} \to (- a \in ℕ \lor - a = 0)$
117	116	ad2antrl	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to (- a \in ℕ \lor - a = 0)$
118	107 114 117	mpjaodan	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to 0 \leq F (- a)$
119		negeq	$⊢ x = a \to - x = - a$
120	119	fveq2d	$⊢ x = a \to F (- x) = F (- a)$
121	10	negeqd	$⊢ x = a \to - F (x) = - F (a)$
122	120 121	eqeq12d	$⊢ x = a \to (F (- x) = - F (x) \leftrightarrow F (- a) = - F (a))$
123	9 122	imbi12d	$⊢ x = a \to (((φ \land x \in ℤ) \to F (- x) = - F (x)) \leftrightarrow ((φ \land a \in ℤ) \to F (- a) = - F (a)))$
124	123 2	chvarvv	$⊢ (φ \land a \in ℤ) \to F (- a) = - F (a)$
125	124	adantrr	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to F (- a) = - F (a)$
126	125	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to F (- a) = - F (a)$
127	118 126	breqtrd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to 0 \leq - F (a)$
128	41	le0neg1d	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to (F (a) \leq 0 \leftrightarrow 0 \leq - F (a))$
129	127 128	mpbird	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to F (a) \leq 0$
130	84	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to F (0) = 0$
131		nngt0	$⊢ b \in ℕ \to 0 < b$
132	131	ad2antll	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to 0 < b$
133		simpll	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to φ$
134	89	a1i	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to 0 \in ℕ_{0}$
135	23	ad2antll	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to b \in ℕ_{0}$
136		simpl	$⊢ (x = 0 \land y = b) \to x = 0$
137	136	eleq1d	$⊢ (x = 0 \land y = b) \to (x \in ℕ_{0} \leftrightarrow 0 \in ℕ_{0})$
138		simpr	$⊢ (x = 0 \land y = b) \to y = b$
139	138	eleq1d	$⊢ (x = 0 \land y = b) \to (y \in ℕ_{0} \leftrightarrow b \in ℕ_{0})$
140	137 139	3anbi23d	$⊢ (x = 0 \land y = b) \to ((φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \leftrightarrow (φ \land 0 \in ℕ_{0} \land b \in ℕ_{0}))$
141		breq12	$⊢ (x = 0 \land y = b) \to (x < y \leftrightarrow 0 < b)$
142	67 33	breqan12d	$⊢ (x = 0 \land y = b) \to (F (x) < F (y) \leftrightarrow F (0) < F (b))$
143	141 142	imbi12d	$⊢ (x = 0 \land y = b) \to ((x < y \to F (x) < F (y)) \leftrightarrow (0 < b \to F (0) < F (b)))$
144	140 143	imbi12d	$⊢ (x = 0 \land y = b) \to (((φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \to (x < y \to F (x) < F (y))) \leftrightarrow ((φ \land 0 \in ℕ_{0} \land b \in ℕ_{0}) \to (0 < b \to F (0) < F (b))))$
145	64 26 144 3	vtocl2	$⊢ (φ \land 0 \in ℕ_{0} \land b \in ℕ_{0}) \to (0 < b \to F (0) < F (b))$
146	133 134 135 145	syl3anc	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to (0 < b \to F (0) < F (b))$
147	132 146	mpd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to F (0) < F (b)$
148	130 147	eqbrtrrd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to 0 < F (b)$
149	41 42 50 129 148	lelttrd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to F (a) < F (b)$
150	149	a1d	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land b \in ℕ)) \to (a < b \to F (a) < F (b))$
151	150	ex	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to ((- a \in ℕ_{0} \land b \in ℕ) \to (a < b \to F (a) < F (b)))$
152		simp3	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0}) \land a < b) \to a < b$
153		zre	$⊢ b \in ℤ \to b \in ℝ$
154	153	adantl	$⊢ (a \in ℤ \land b \in ℤ) \to b \in ℝ$
155	154	ad2antlr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to b \in ℝ$
156		1red	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to 1 \in ℝ$
157		nnre	$⊢ a \in ℕ \to a \in ℝ$
158	157	ad2antrl	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to a \in ℝ$
159		0red	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to 0 \in ℝ$
160		nn0ge0	$⊢ - b \in ℕ_{0} \to 0 \leq - b$
161	160	ad2antll	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to 0 \leq - b$
162	155	le0neg1d	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to (b \leq 0 \leftrightarrow 0 \leq - b)$
163	161 162	mpbird	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to b \leq 0$
164		0le1	$⊢ 0 \leq 1$
165	164	a1i	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to 0 \leq 1$
166	155 159 156 163 165	letrd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to b \leq 1$
167		nnge1	$⊢ a \in ℕ \to 1 \leq a$
168	167	ad2antrl	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to 1 \leq a$
169	155 156 158 166 168	letrd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to b \leq a$
170	155 158	lenltd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to (b \leq a \leftrightarrow \neg a < b)$
171	169 170	mpbid	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0})) \to \neg a < b$
172	171	3adant3	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0}) \land a < b) \to \neg a < b$
173	152 172	pm2.21dd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (a \in ℕ \land - b \in ℕ_{0}) \land a < b) \to F (a) < F (b)$
174	173	3exp	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to ((a \in ℕ \land - b \in ℕ_{0}) \to (a < b \to F (a) < F (b)))$
175		negex	$⊢ - b \in V$
176		simpl	$⊢ (x = - b \land y = - a) \to x = - b$
177	176	eleq1d	$⊢ (x = - b \land y = - a) \to (x \in ℕ_{0} \leftrightarrow - b \in ℕ_{0})$
178		simpr	$⊢ (x = - b \land y = - a) \to y = - a$
179	178	eleq1d	$⊢ (x = - b \land y = - a) \to (y \in ℕ_{0} \leftrightarrow - a \in ℕ_{0})$
180	177 179	3anbi23d	$⊢ (x = - b \land y = - a) \to ((φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \leftrightarrow (φ \land - b \in ℕ_{0} \land - a \in ℕ_{0}))$
181		breq12	$⊢ (x = - b \land y = - a) \to (x < y \leftrightarrow - b < - a)$
182		fveq2	$⊢ x = - b \to F (x) = F (- b)$
183		fveq2	$⊢ y = - a \to F (y) = F (- a)$
184	182 183	breqan12d	$⊢ (x = - b \land y = - a) \to (F (x) < F (y) \leftrightarrow F (- b) < F (- a))$
185	181 184	imbi12d	$⊢ (x = - b \land y = - a) \to ((x < y \to F (x) < F (y)) \leftrightarrow (- b < - a \to F (- b) < F (- a)))$
186	180 185	imbi12d	$⊢ (x = - b \land y = - a) \to (((φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \to (x < y \to F (x) < F (y))) \leftrightarrow ((φ \land - b \in ℕ_{0} \land - a \in ℕ_{0}) \to (- b < - a \to F (- b) < F (- a))))$
187	175 54 186 3	vtocl2	$⊢ (φ \land - b \in ℕ_{0} \land - a \in ℕ_{0}) \to (- b < - a \to F (- b) < F (- a))$
188	187	3com23	$⊢ (φ \land - a \in ℕ_{0} \land - b \in ℕ_{0}) \to (- b < - a \to F (- b) < F (- a))$
189	188	3expb	$⊢ (φ \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to (- b < - a \to F (- b) < F (- a))$
190	189	adantlr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to (- b < - a \to F (- b) < F (- a))$
191		negeq	$⊢ x = b \to - x = - b$
192	191	fveq2d	$⊢ x = b \to F (- x) = F (- b)$
193	45	negeqd	$⊢ x = b \to - F (x) = - F (b)$
194	192 193	eqeq12d	$⊢ x = b \to (F (- x) = - F (x) \leftrightarrow F (- b) = - F (b))$
195	44 194	imbi12d	$⊢ x = b \to (((φ \land x \in ℤ) \to F (- x) = - F (x)) \leftrightarrow ((φ \land b \in ℤ) \to F (- b) = - F (b)))$
196	195 2	chvarvv	$⊢ (φ \land b \in ℤ) \to F (- b) = - F (b)$
197	196	adantrl	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to F (- b) = - F (b)$
198	197	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to F (- b) = - F (b)$
199	125	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to F (- a) = - F (a)$
200	198 199	breq12d	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to (F (- b) < F (- a) \leftrightarrow - F (b) < - F (a))$
201	190 200	sylibd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to (- b < - a \to - F (b) < - F (a))$
202		zre	$⊢ a \in ℤ \to a \in ℝ$
203	202	ad2antrl	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to a \in ℝ$
204	203	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to a \in ℝ$
205	154	ad2antlr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to b \in ℝ$
206	204 205	ltnegd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to (a < b \leftrightarrow - b < - a)$
207	40	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to F (a) \in ℝ$
208	49	adantr	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to F (b) \in ℝ$
209	207 208	ltnegd	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to (F (a) < F (b) \leftrightarrow - F (b) < - F (a))$
210	201 206 209	3imtr4d	$⊢ ((φ \land (a \in ℤ \land b \in ℤ)) \land (- a \in ℕ_{0} \land - b \in ℕ_{0})) \to (a < b \to F (a) < F (b))$
211	210	ex	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to ((- a \in ℕ_{0} \land - b \in ℕ_{0}) \to (a < b \to F (a) < F (b)))$
212	39 151 174 211	ccased	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to (((a \in ℕ \lor - a \in ℕ_{0}) \land (b \in ℕ \lor - b \in ℕ_{0})) \to (a < b \to F (a) < F (b)))$
213	19 212	mpd	$⊢ (φ \land (a \in ℤ \land b \in ℤ)) \to (a < b \to F (a) < F (b))$
214	4 5 6 7 13 213	ltord1	$⊢ (φ \land (A \in ℤ \land B \in ℤ)) \to (A < B \leftrightarrow F (A) < F (B))$
215	214	3impb	$⊢ (φ \land A \in ℤ \land B \in ℤ) \to (A < B \leftrightarrow F (A) < F (B))$

Metamath Proof Explorer

Theorem monotoddzzfi

Proof