monotuz

Description: A function defined on an upper set of integers which increases at every adjacent pair is globally strictly monotonic by induction. (Contributed by Stefan O'Rear, 24-Sep-2014)

	Ref	Expression
Hypotheses	monotuz.1	$⊢ (φ \land y \in H) \to F < G$
	monotuz.2	$⊢ (φ \land x \in H) \to C \in ℝ$
	monotuz.3	$⊢ H = ℤ_{\geq I}$
	monotuz.4	$⊢ x = y + 1 \to C = G$
	monotuz.5	$⊢ x = y \to C = F$
	monotuz.6	$⊢ x = A \to C = D$
	monotuz.7	$⊢ x = B \to C = E$
Assertion	monotuz	$⊢ (φ \land (A \in H \land B \in H)) \to (A < B \leftrightarrow D < E)$

Proof

Step	Hyp	Ref	Expression
1		monotuz.1	$⊢ (φ \land y \in H) \to F < G$
2		monotuz.2	$⊢ (φ \land x \in H) \to C \in ℝ$
3		monotuz.3	$⊢ H = ℤ_{\geq I}$
4		monotuz.4	$⊢ x = y + 1 \to C = G$
5		monotuz.5	$⊢ x = y \to C = F$
6		monotuz.6	$⊢ x = A \to C = D$
7		monotuz.7	$⊢ x = B \to C = E$
8		csbeq1	$⊢ a = b \to ⦋ a / x ⦌ C = ⦋ b / x ⦌ C$
9		csbeq1	$⊢ a = A \to ⦋ a / x ⦌ C = ⦋ A / x ⦌ C$
10		csbeq1	$⊢ a = B \to ⦋ a / x ⦌ C = ⦋ B / x ⦌ C$
11		uzssz	$⊢ ℤ_{\geq I} \subseteq ℤ$
12		zssre	$⊢ ℤ \subseteq ℝ$
13	11 12	sstri	$⊢ ℤ_{\geq I} \subseteq ℝ$
14	3 13	eqsstri	$⊢ H \subseteq ℝ$
15		nfv	$⊢ Ⅎ x (φ \land a \in H)$
16		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ C$
17	16	nfel1	$⊢ Ⅎ x ⦋ a / x ⦌ C \in ℝ$
18	15 17	nfim	$⊢ Ⅎ x ((φ \land a \in H) \to ⦋ a / x ⦌ C \in ℝ)$
19		eleq1	$⊢ x = a \to (x \in H \leftrightarrow a \in H)$
20	19	anbi2d	$⊢ x = a \to ((φ \land x \in H) \leftrightarrow (φ \land a \in H))$
21		csbeq1a	$⊢ x = a \to C = ⦋ a / x ⦌ C$
22	21	eleq1d	$⊢ x = a \to (C \in ℝ \leftrightarrow ⦋ a / x ⦌ C \in ℝ)$
23	20 22	imbi12d	$⊢ x = a \to (((φ \land x \in H) \to C \in ℝ) \leftrightarrow ((φ \land a \in H) \to ⦋ a / x ⦌ C \in ℝ))$
24	18 23 2	chvarfv	$⊢ (φ \land a \in H) \to ⦋ a / x ⦌ C \in ℝ$
25		simpl	$⊢ ((φ \land a \in H) \land a < b) \to (φ \land a \in H)$
26	25	adantlrr	$⊢ ((φ \land (a \in H \land b \in H)) \land a < b) \to (φ \land a \in H)$
27	3 11	eqsstri	$⊢ H \subseteq ℤ$
28		simplrl	$⊢ ((φ \land (a \in H \land b \in H)) \land a < b) \to a \in H$
29	27 28	sseldi	$⊢ ((φ \land (a \in H \land b \in H)) \land a < b) \to a \in ℤ$
30		simplrr	$⊢ ((φ \land (a \in H \land b \in H)) \land a < b) \to b \in H$
31	27 30	sseldi	$⊢ ((φ \land (a \in H \land b \in H)) \land a < b) \to b \in ℤ$
32		simpr	$⊢ ((φ \land (a \in H \land b \in H)) \land a < b) \to a < b$
33		csbeq1	$⊢ c = a + 1 \to ⦋ c / x ⦌ C = ⦋ (a + 1) / x ⦌ C$
34	33	breq2d	$⊢ c = a + 1 \to (⦋ a / x ⦌ C < ⦋ c / x ⦌ C \leftrightarrow ⦋ a / x ⦌ C < ⦋ (a + 1) / x ⦌ C)$
35	34	imbi2d	$⊢ c = a + 1 \to (((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ c / x ⦌ C) \leftrightarrow ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ (a + 1) / x ⦌ C))$
36		csbeq1	$⊢ c = d \to ⦋ c / x ⦌ C = ⦋ d / x ⦌ C$
37	36	breq2d	$⊢ c = d \to (⦋ a / x ⦌ C < ⦋ c / x ⦌ C \leftrightarrow ⦋ a / x ⦌ C < ⦋ d / x ⦌ C)$
38	37	imbi2d	$⊢ c = d \to (((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ c / x ⦌ C) \leftrightarrow ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ d / x ⦌ C))$
39		csbeq1	$⊢ c = d + 1 \to ⦋ c / x ⦌ C = ⦋ (d + 1) / x ⦌ C$
40	39	breq2d	$⊢ c = d + 1 \to (⦋ a / x ⦌ C < ⦋ c / x ⦌ C \leftrightarrow ⦋ a / x ⦌ C < ⦋ (d + 1) / x ⦌ C)$
41	40	imbi2d	$⊢ c = d + 1 \to (((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ c / x ⦌ C) \leftrightarrow ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ (d + 1) / x ⦌ C))$
42		csbeq1	$⊢ c = b \to ⦋ c / x ⦌ C = ⦋ b / x ⦌ C$
43	42	breq2d	$⊢ c = b \to (⦋ a / x ⦌ C < ⦋ c / x ⦌ C \leftrightarrow ⦋ a / x ⦌ C < ⦋ b / x ⦌ C)$
44	43	imbi2d	$⊢ c = b \to (((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ c / x ⦌ C) \leftrightarrow ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ b / x ⦌ C))$
45		eleq1	$⊢ y = a \to (y \in H \leftrightarrow a \in H)$
46	45	anbi2d	$⊢ y = a \to ((φ \land y \in H) \leftrightarrow (φ \land a \in H))$
47		vex	$⊢ y \in V$
48	47 5	csbie	$⊢ ⦋ y / x ⦌ C = F$
49		csbeq1	$⊢ y = a \to ⦋ y / x ⦌ C = ⦋ a / x ⦌ C$
50	48 49	eqtr3id	$⊢ y = a \to F = ⦋ a / x ⦌ C$
51		ovex	$⊢ y + 1 \in V$
52	51 4	csbie	$⊢ ⦋ (y + 1) / x ⦌ C = G$
53		oveq1	$⊢ y = a \to y + 1 = a + 1$
54	53	csbeq1d	$⊢ y = a \to ⦋ (y + 1) / x ⦌ C = ⦋ (a + 1) / x ⦌ C$
55	52 54	eqtr3id	$⊢ y = a \to G = ⦋ (a + 1) / x ⦌ C$
56	50 55	breq12d	$⊢ y = a \to (F < G \leftrightarrow ⦋ a / x ⦌ C < ⦋ (a + 1) / x ⦌ C)$
57	46 56	imbi12d	$⊢ y = a \to (((φ \land y \in H) \to F < G) \leftrightarrow ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ (a + 1) / x ⦌ C))$
58	57 1	vtoclg	$⊢ a \in ℤ \to ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ (a + 1) / x ⦌ C)$
59	24	3ad2ant2	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to ⦋ a / x ⦌ C \in ℝ$
60		simp2l	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to φ$
61		zre	$⊢ a \in ℤ \to a \in ℝ$
62	61	3ad2ant1	$⊢ (a \in ℤ \land d \in ℤ \land a < d) \to a \in ℝ$
63		zre	$⊢ d \in ℤ \to d \in ℝ$
64	63	3ad2ant2	$⊢ (a \in ℤ \land d \in ℤ \land a < d) \to d \in ℝ$
65		simp3	$⊢ (a \in ℤ \land d \in ℤ \land a < d) \to a < d$
66	62 64 65	ltled	$⊢ (a \in ℤ \land d \in ℤ \land a < d) \to a \leq d$
67	66	3ad2ant1	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to a \leq d$
68		simp11	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to a \in ℤ$
69		simp12	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to d \in ℤ$
70		eluz	$⊢ (a \in ℤ \land d \in ℤ) \to (d \in ℤ_{\geq a} \leftrightarrow a \leq d)$
71	68 69 70	syl2anc	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to (d \in ℤ_{\geq a} \leftrightarrow a \leq d)$
72	67 71	mpbird	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to d \in ℤ_{\geq a}$
73		simp2r	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to a \in H$
74	73 3	eleqtrdi	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to a \in ℤ_{\geq I}$
75		uztrn	$⊢ (d \in ℤ_{\geq a} \land a \in ℤ_{\geq I}) \to d \in ℤ_{\geq I}$
76	72 74 75	syl2anc	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to d \in ℤ_{\geq I}$
77	76 3	eleqtrrdi	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to d \in H$
78		nfv	$⊢ Ⅎ x (φ \land d \in H)$
79		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ d / x ⦌ C$
80	79	nfel1	$⊢ Ⅎ x ⦋ d / x ⦌ C \in ℝ$
81	78 80	nfim	$⊢ Ⅎ x ((φ \land d \in H) \to ⦋ d / x ⦌ C \in ℝ)$
82		eleq1	$⊢ x = d \to (x \in H \leftrightarrow d \in H)$
83	82	anbi2d	$⊢ x = d \to ((φ \land x \in H) \leftrightarrow (φ \land d \in H))$
84		csbeq1a	$⊢ x = d \to C = ⦋ d / x ⦌ C$
85	84	eleq1d	$⊢ x = d \to (C \in ℝ \leftrightarrow ⦋ d / x ⦌ C \in ℝ)$
86	83 85	imbi12d	$⊢ x = d \to (((φ \land x \in H) \to C \in ℝ) \leftrightarrow ((φ \land d \in H) \to ⦋ d / x ⦌ C \in ℝ))$
87	81 86 2	chvarfv	$⊢ (φ \land d \in H) \to ⦋ d / x ⦌ C \in ℝ$
88	60 77 87	syl2anc	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to ⦋ d / x ⦌ C \in ℝ$
89		peano2uz	$⊢ d \in ℤ_{\geq I} \to d + 1 \in ℤ_{\geq I}$
90	76 89	syl	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to d + 1 \in ℤ_{\geq I}$
91	90 3	eleqtrrdi	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to d + 1 \in H$
92		nfv	$⊢ Ⅎ x (φ \land d + 1 \in H)$
93		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ (d + 1) / x ⦌ C$
94	93	nfel1	$⊢ Ⅎ x ⦋ (d + 1) / x ⦌ C \in ℝ$
95	92 94	nfim	$⊢ Ⅎ x ((φ \land d + 1 \in H) \to ⦋ (d + 1) / x ⦌ C \in ℝ)$
96		ovex	$⊢ d + 1 \in V$
97		eleq1	$⊢ x = d + 1 \to (x \in H \leftrightarrow d + 1 \in H)$
98	97	anbi2d	$⊢ x = d + 1 \to ((φ \land x \in H) \leftrightarrow (φ \land d + 1 \in H))$
99		csbeq1a	$⊢ x = d + 1 \to C = ⦋ (d + 1) / x ⦌ C$
100	99	eleq1d	$⊢ x = d + 1 \to (C \in ℝ \leftrightarrow ⦋ (d + 1) / x ⦌ C \in ℝ)$
101	98 100	imbi12d	$⊢ x = d + 1 \to (((φ \land x \in H) \to C \in ℝ) \leftrightarrow ((φ \land d + 1 \in H) \to ⦋ (d + 1) / x ⦌ C \in ℝ))$
102	95 96 101 2	vtoclf	$⊢ (φ \land d + 1 \in H) \to ⦋ (d + 1) / x ⦌ C \in ℝ$
103	60 91 102	syl2anc	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to ⦋ (d + 1) / x ⦌ C \in ℝ$
104		simp3	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to ⦋ a / x ⦌ C < ⦋ d / x ⦌ C$
105		nfv	$⊢ Ⅎ y ((φ \land d \in H) \to ⦋ d / x ⦌ C < ⦋ (d + 1) / x ⦌ C)$
106		eleq1	$⊢ y = d \to (y \in H \leftrightarrow d \in H)$
107	106	anbi2d	$⊢ y = d \to ((φ \land y \in H) \leftrightarrow (φ \land d \in H))$
108		csbeq1	$⊢ y = d \to ⦋ y / x ⦌ C = ⦋ d / x ⦌ C$
109	48 108	eqtr3id	$⊢ y = d \to F = ⦋ d / x ⦌ C$
110		oveq1	$⊢ y = d \to y + 1 = d + 1$
111	110	csbeq1d	$⊢ y = d \to ⦋ (y + 1) / x ⦌ C = ⦋ (d + 1) / x ⦌ C$
112	52 111	eqtr3id	$⊢ y = d \to G = ⦋ (d + 1) / x ⦌ C$
113	109 112	breq12d	$⊢ y = d \to (F < G \leftrightarrow ⦋ d / x ⦌ C < ⦋ (d + 1) / x ⦌ C)$
114	107 113	imbi12d	$⊢ y = d \to (((φ \land y \in H) \to F < G) \leftrightarrow ((φ \land d \in H) \to ⦋ d / x ⦌ C < ⦋ (d + 1) / x ⦌ C))$
115	105 114 1	chvarfv	$⊢ (φ \land d \in H) \to ⦋ d / x ⦌ C < ⦋ (d + 1) / x ⦌ C$
116	60 77 115	syl2anc	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to ⦋ d / x ⦌ C < ⦋ (d + 1) / x ⦌ C$
117	59 88 103 104 116	lttrd	$⊢ ((a \in ℤ \land d \in ℤ \land a < d) \land (φ \land a \in H) \land ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to ⦋ a / x ⦌ C < ⦋ (d + 1) / x ⦌ C$
118	117	3exp	$⊢ (a \in ℤ \land d \in ℤ \land a < d) \to ((φ \land a \in H) \to (⦋ a / x ⦌ C < ⦋ d / x ⦌ C \to ⦋ a / x ⦌ C < ⦋ (d + 1) / x ⦌ C))$
119	118	a2d	$⊢ (a \in ℤ \land d \in ℤ \land a < d) \to (((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ d / x ⦌ C) \to ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ (d + 1) / x ⦌ C))$
120	35 38 41 44 58 119	uzind2	$⊢ (a \in ℤ \land b \in ℤ \land a < b) \to ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ b / x ⦌ C)$
121	29 31 32 120	syl3anc	$⊢ ((φ \land (a \in H \land b \in H)) \land a < b) \to ((φ \land a \in H) \to ⦋ a / x ⦌ C < ⦋ b / x ⦌ C)$
122	26 121	mpd	$⊢ ((φ \land (a \in H \land b \in H)) \land a < b) \to ⦋ a / x ⦌ C < ⦋ b / x ⦌ C$
123	122	ex	$⊢ (φ \land (a \in H \land b \in H)) \to (a < b \to ⦋ a / x ⦌ C < ⦋ b / x ⦌ C)$
124	8 9 10 14 24 123	ltord1	$⊢ (φ \land (A \in H \land B \in H)) \to (A < B \leftrightarrow ⦋ A / x ⦌ C < ⦋ B / x ⦌ C)$
125		nfcvd	$⊢ A \in H \to \underline{Ⅎ} x D$
126	125 6	csbiegf	$⊢ A \in H \to ⦋ A / x ⦌ C = D$
127		nfcvd	$⊢ B \in H \to \underline{Ⅎ} x E$
128	127 7	csbiegf	$⊢ B \in H \to ⦋ B / x ⦌ C = E$
129	126 128	breqan12d	$⊢ (A \in H \land B \in H) \to (⦋ A / x ⦌ C < ⦋ B / x ⦌ C \leftrightarrow D < E)$
130	129	adantl	$⊢ (φ \land (A \in H \land B \in H)) \to (⦋ A / x ⦌ C < ⦋ B / x ⦌ C \leftrightarrow D < E)$
131	124 130	bitrd	$⊢ (φ \land (A \in H \land B \in H)) \to (A < B \leftrightarrow D < E)$

Metamath Proof Explorer

Theorem monotuz

Proof