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	$⊢ (φ \land x \in ℕ_{0} \land y \in ℕ_{0}) \to (x < y \to E < F)$
	monotoddzz.2	$⊢ (φ \land x \in ℤ) \to E \in ℝ$
	monotoddzz.3	$⊢ (φ \land y \in ℤ) \to G = - F$
	monotoddzz.4	$⊢ x = A \to E = C$
	monotoddzz.5	$⊢ x = B \to E = D$
	monotoddzz.6	$⊢ x = y \to E = F$
	monotoddzz.7	$⊢ x = - y \to E = G$
Assertion	monotoddzz	$⊢ (φ \land A \in ℤ \land B \in ℤ) \to (A < B \leftrightarrow C < D)$

Proof

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

Metamath Proof Explorer

Theorem monotoddzz

Proof