natglobalincr

Description: Local monotonicity on half-open integer range implies global monotonicity. Inference form. (Contributed by Ender Ting, 23-Nov-2024)

	Ref	Expression
Hypotheses	natglobalincr.1	$⊢ \forall k \in (0 ..^T) B (k) < B (k + 1)$
	natglobalincr.2	$⊢ T \in ℤ$
Assertion	natglobalincr	$⊢ \forall k \in (0 ..^T) \forall t \in (k + 1 \dots T) B (k) < B (t)$

Proof

Step	Hyp	Ref	Expression
1		natglobalincr.1	$⊢ \forall k \in (0 ..^T) B (k) < B (k + 1)$
2		natglobalincr.2	$⊢ T \in ℤ$
3		elfzoelz	$⊢ k \in (0 ..^T) \to k \in ℤ$
4	3	peano2zd	$⊢ k \in (0 ..^T) \to k + 1 \in ℤ$
5		elfz1	$⊢ (k + 1 \in ℤ \land T \in ℤ) \to (t \in (k + 1 \dots T) \leftrightarrow (t \in ℤ \land k + 1 \leq t \land t \leq T))$
6	4 2 5	sylancl	$⊢ k \in (0 ..^T) \to (t \in (k + 1 \dots T) \leftrightarrow (t \in ℤ \land k + 1 \leq t \land t \leq T))$
7		fveq2	$⊢ a = k + 1 \to B (a) = B (k + 1)$
8	7	breq2d	$⊢ a = k + 1 \to (B (k) < B (a) \leftrightarrow B (k) < B (k + 1))$
9		fveq2	$⊢ a = b \to B (a) = B (b)$
10	9	breq2d	$⊢ a = b \to (B (k) < B (a) \leftrightarrow B (k) < B (b))$
11		fveq2	$⊢ a = b + 1 \to B (a) = B (b + 1)$
12	11	breq2d	$⊢ a = b + 1 \to (B (k) < B (a) \leftrightarrow B (k) < B (b + 1))$
13		fveq2	$⊢ a = t \to B (a) = B (t)$
14	13	breq2d	$⊢ a = t \to (B (k) < B (a) \leftrightarrow B (k) < B (t))$
15	1	rspec	$⊢ k \in (0 ..^T) \to B (k) < B (k + 1)$
16		df-br	$⊢ B (k) < B (b) \leftrightarrow ⟨B (k), B (b)⟩ \in <$
17		ltrelxr	$⊢ < \subseteq ℝ^{} \times ℝ^{}$
18	17	sseli	$⊢ ⟨B (k), B (b)⟩ \in < \to ⟨B (k), B (b)⟩ \in (ℝ^{} \times ℝ^{})$
19	16 18	sylbi	$⊢ B (k) < B (b) \to ⟨B (k), B (b)⟩ \in (ℝ^{} \times ℝ^{})$
20		opelxp1	$⊢ ⟨B (k), B (b)⟩ \in (ℝ^{} \times ℝ^{}) \to B (k) \in ℝ^{*}$
21	19 20	syl	$⊢ B (k) < B (b) \to B (k) \in ℝ^{*}$
22	21	3ad2ant3	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to B (k) \in ℝ^{*}$
23		opelxp2	$⊢ ⟨B (k), B (b)⟩ \in (ℝ^{} \times ℝ^{}) \to B (b) \in ℝ^{*}$
24	19 23	syl	$⊢ B (k) < B (b) \to B (b) \in ℝ^{*}$
25	24	3ad2ant3	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to B (b) \in ℝ^{*}$
26		0red	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to 0 \in ℝ$
27		simp1	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to k \in (0 ..^T)$
28		zre	$⊢ k \in ℤ \to k \in ℝ$
29		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
30	27 3 28 29	4syl	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to k + 1 \in ℝ$
31		simp21	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to b \in ℤ$
32	31	zred	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to b \in ℝ$
33		elfzole1	$⊢ k \in (0 ..^T) \to 0 \leq k$
34	28	ltp1d	$⊢ k \in ℤ \to k < k + 1$
35	3 34	syl	$⊢ k \in (0 ..^T) \to k < k + 1$
36		0red	$⊢ k \in ℝ \to 0 \in ℝ$
37		id	$⊢ k \in ℝ \to k \in ℝ$
38	36 37 29	3jca	$⊢ k \in ℝ \to (0 \in ℝ \land k \in ℝ \land k + 1 \in ℝ)$
39		leltletr	$⊢ (0 \in ℝ \land k \in ℝ \land k + 1 \in ℝ) \to ((0 \leq k \land k < k + 1) \to 0 \leq k + 1)$
40	3 28 38 39	4syl	$⊢ k \in (0 ..^T) \to ((0 \leq k \land k < k + 1) \to 0 \leq k + 1)$
41	33 35 40	mp2and	$⊢ k \in (0 ..^T) \to 0 \leq k + 1$
42	41	3ad2ant1	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to 0 \leq k + 1$
43		simp22	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to k + 1 \leq b$
44	26 30 32 42 43	letrd	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to 0 \leq b$
45		simp23	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to b < T$
46		0zd	$⊢ b \in ℤ \to 0 \in ℤ$
47	2	a1i	$⊢ b \in ℤ \to T \in ℤ$
48		elfzo	$⊢ (b \in ℤ \land 0 \in ℤ \land T \in ℤ) \to (b \in (0 ..^T) \leftrightarrow (0 \leq b \land b < T))$
49	46 47 48	mpd3an23	$⊢ b \in ℤ \to (b \in (0 ..^T) \leftrightarrow (0 \leq b \land b < T))$
50		fveq2	$⊢ k = b \to B (k) = B (b)$
51		fvoveq1	$⊢ k = b \to B (k + 1) = B (b + 1)$
52	50 51	breq12d	$⊢ k = b \to (B (k) < B (k + 1) \leftrightarrow B (b) < B (b + 1))$
53	52 1	vtoclri	$⊢ b \in (0 ..^T) \to B (b) < B (b + 1)$
54	49 53	biimtrrdi	$⊢ b \in ℤ \to ((0 \leq b \land b < T) \to B (b) < B (b + 1))$
55	31 54	syl	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to ((0 \leq b \land b < T) \to B (b) < B (b + 1))$
56	44 45 55	mp2and	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to B (b) < B (b + 1)$
57		df-br	$⊢ B (b) < B (b + 1) \leftrightarrow ⟨B (b), B (b + 1)⟩ \in <$
58	17	sseli	$⊢ ⟨B (b), B (b + 1)⟩ \in < \to ⟨B (b), B (b + 1)⟩ \in (ℝ^{} \times ℝ^{})$
59	57 58	sylbi	$⊢ B (b) < B (b + 1) \to ⟨B (b), B (b + 1)⟩ \in (ℝ^{} \times ℝ^{})$
60		opelxp2	$⊢ ⟨B (b), B (b + 1)⟩ \in (ℝ^{} \times ℝ^{}) \to B (b + 1) \in ℝ^{*}$
61	56 59 60	3syl	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to B (b + 1) \in ℝ^{*}$
62		simp3	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to B (k) < B (b)$
63	22 25 61 62 56	xrlttrd	$⊢ (k \in (0 ..^T) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) < B (b)) \to B (k) < B (b + 1)$
64		elfzoel2	$⊢ k \in (0 ..^T) \to T \in ℤ$
65		elfzop1le2	$⊢ k \in (0 ..^T) \to k + 1 \leq T$
66	8 10 12 14 15 63 4 64 65	fzindd	$⊢ (k \in (0 ..^T) \land (t \in ℤ \land k + 1 \leq t \land t \leq T)) \to B (k) < B (t)$
67	6 66	sylbida	$⊢ (k \in (0 ..^T) \land t \in (k + 1 \dots T)) \to B (k) < B (t)$
68	67	rgen2	$⊢ \forall k \in (0 ..^T) \forall t \in (k + 1 \dots T) B (k) < B (t)$

Metamath Proof Explorer

Theorem natglobalincr

Proof