fzass4

Description: Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	fzass4	$⊢ (B \in (A \dots D) \land C \in (B \dots D)) \leftrightarrow (B \in (A \dots C) \land C \in (A \dots D))$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C})) \to B \in ℤ_{\geq A}$
2		simprl	$⊢ ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C})) \to C \in ℤ_{\geq B}$
3	1 2	jca	$⊢ ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C})) \to (B \in ℤ_{\geq A} \land C \in ℤ_{\geq B})$
4		uztrn	$⊢ (C \in ℤ_{\geq B} \land B \in ℤ_{\geq A}) \to C \in ℤ_{\geq A}$
5	4	ancoms	$⊢ (B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \to C \in ℤ_{\geq A}$
6	5	ad2ant2r	$⊢ ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C})) \to C \in ℤ_{\geq A}$
7		simprr	$⊢ ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C})) \to D \in ℤ_{\geq C}$
8	3 6 7	jca32	$⊢ ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C})) \to ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C}))$
9		simpll	$⊢ ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C})) \to B \in ℤ_{\geq A}$
10		uztrn	$⊢ (D \in ℤ_{\geq C} \land C \in ℤ_{\geq B}) \to D \in ℤ_{\geq B}$
11	10	ancoms	$⊢ (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C}) \to D \in ℤ_{\geq B}$
12	11	ad2ant2l	$⊢ ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C})) \to D \in ℤ_{\geq B}$
13	9 12	jca	$⊢ ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C})) \to (B \in ℤ_{\geq A} \land D \in ℤ_{\geq B})$
14		simplr	$⊢ ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C})) \to C \in ℤ_{\geq B}$
15		simprr	$⊢ ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C})) \to D \in ℤ_{\geq C}$
16	13 14 15	jca32	$⊢ ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C})) \to ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C}))$
17	8 16	impbii	$⊢ ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C})) \leftrightarrow ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C}))$
18		elfzuzb	$⊢ B \in (A \dots D) \leftrightarrow (B \in ℤ_{\geq A} \land D \in ℤ_{\geq B})$
19		elfzuzb	$⊢ C \in (B \dots D) \leftrightarrow (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C})$
20	18 19	anbi12i	$⊢ (B \in (A \dots D) \land C \in (B \dots D)) \leftrightarrow ((B \in ℤ_{\geq A} \land D \in ℤ_{\geq B}) \land (C \in ℤ_{\geq B} \land D \in ℤ_{\geq C}))$
21		elfzuzb	$⊢ B \in (A \dots C) \leftrightarrow (B \in ℤ_{\geq A} \land C \in ℤ_{\geq B})$
22		elfzuzb	$⊢ C \in (A \dots D) \leftrightarrow (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C})$
23	21 22	anbi12i	$⊢ (B \in (A \dots C) \land C \in (A \dots D)) \leftrightarrow ((B \in ℤ_{\geq A} \land C \in ℤ_{\geq B}) \land (C \in ℤ_{\geq A} \land D \in ℤ_{\geq C}))$
24	17 20 23	3bitr4i	$⊢ (B \in (A \dots D) \land C \in (B \dots D)) \leftrightarrow (B \in (A \dots C) \land C \in (A \dots D))$

Metamath Proof Explorer

Theorem fzass4

Proof