shftuz

Description: A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013)

		Ref	Expression
	Assertion	shftuz	$⊢ (A \in ℤ \land B \in ℤ) \to \{x \in ℂ \| x - A \in ℤ_{\geq B}\} = ℤ_{\geq (B + A)}$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in ℂ \| x - A \in ℤ_{\geq B}\} = \{x \| (x \in ℂ \land x - A \in ℤ_{\geq B})\}$
2		simp2	$⊢ (A \in ℤ \land x \in ℂ \land x - A \in ℤ_{\geq B}) \to x \in ℂ$
3		zcn	$⊢ A \in ℤ \to A \in ℂ$
4	3	3ad2ant1	$⊢ (A \in ℤ \land x \in ℂ \land x - A \in ℤ_{\geq B}) \to A \in ℂ$
5	2 4	npcand	$⊢ (A \in ℤ \land x \in ℂ \land x - A \in ℤ_{\geq B}) \to x - A + A = x$
6		eluzadd	$⊢ (x - A \in ℤ_{\geq B} \land A \in ℤ) \to x - A + A \in ℤ_{\geq (B + A)}$
7	6	ancoms	$⊢ (A \in ℤ \land x - A \in ℤ_{\geq B}) \to x - A + A \in ℤ_{\geq (B + A)}$
8	7	3adant2	$⊢ (A \in ℤ \land x \in ℂ \land x - A \in ℤ_{\geq B}) \to x - A + A \in ℤ_{\geq (B + A)}$
9	5 8	eqeltrrd	$⊢ (A \in ℤ \land x \in ℂ \land x - A \in ℤ_{\geq B}) \to x \in ℤ_{\geq (B + A)}$
10	9	3expib	$⊢ A \in ℤ \to ((x \in ℂ \land x - A \in ℤ_{\geq B}) \to x \in ℤ_{\geq (B + A)})$
11	10	adantr	$⊢ (A \in ℤ \land B \in ℤ) \to ((x \in ℂ \land x - A \in ℤ_{\geq B}) \to x \in ℤ_{\geq (B + A)})$
12		eluzelcn	$⊢ x \in ℤ_{\geq (B + A)} \to x \in ℂ$
13	12	a1i	$⊢ (A \in ℤ \land B \in ℤ) \to (x \in ℤ_{\geq (B + A)} \to x \in ℂ)$
14		eluzsub	$⊢ (B \in ℤ \land A \in ℤ \land x \in ℤ_{\geq (B + A)}) \to x - A \in ℤ_{\geq B}$
15	14	3expia	$⊢ (B \in ℤ \land A \in ℤ) \to (x \in ℤ_{\geq (B + A)} \to x - A \in ℤ_{\geq B})$
16	15	ancoms	$⊢ (A \in ℤ \land B \in ℤ) \to (x \in ℤ_{\geq (B + A)} \to x - A \in ℤ_{\geq B})$
17	13 16	jcad	$⊢ (A \in ℤ \land B \in ℤ) \to (x \in ℤ_{\geq (B + A)} \to (x \in ℂ \land x - A \in ℤ_{\geq B}))$
18	11 17	impbid	$⊢ (A \in ℤ \land B \in ℤ) \to ((x \in ℂ \land x - A \in ℤ_{\geq B}) \leftrightarrow x \in ℤ_{\geq (B + A)})$
19	18	eqabcdv	$⊢ (A \in ℤ \land B \in ℤ) \to \{x \| (x \in ℂ \land x - A \in ℤ_{\geq B})\} = ℤ_{\geq (B + A)}$
20	1 19	eqtrid	$⊢ (A \in ℤ \land B \in ℤ) \to \{x \in ℂ \| x - A \in ℤ_{\geq B}\} = ℤ_{\geq (B + A)}$

Metamath Proof Explorer

Theorem shftuz

Proof