sumrb

Description: Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013) (Revised by Mario Carneiro, 9-Apr-2014)

	Ref	Expression
Hypotheses	summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
	summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	sumrb.4	$⊢ φ \to M \in ℤ$
	sumrb.5	$⊢ φ \to N \in ℤ$
	sumrb.6	$⊢ φ \to A \subseteq ℤ_{\geq M}$
	sumrb.7	$⊢ φ \to A \subseteq ℤ_{\geq N}$
Assertion	sumrb	$⊢ φ \to (seq M (+ F) ⇝ C \leftrightarrow seq N (+ F) ⇝ C)$

Proof

Step	Hyp	Ref	Expression
1		summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
2		summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		sumrb.4	$⊢ φ \to M \in ℤ$
4		sumrb.5	$⊢ φ \to N \in ℤ$
5		sumrb.6	$⊢ φ \to A \subseteq ℤ_{\geq M}$
6		sumrb.7	$⊢ φ \to A \subseteq ℤ_{\geq N}$
7	4	adantr	$⊢ (φ \land N \in ℤ_{\geq M}) \to N \in ℤ$
8		seqex	$⊢ seq M (+ F) \in V$
9		climres	$⊢ (N \in ℤ \land seq M (+ F) \in V) \to (({seq M (+ F) ↾}_{ℤ_{\geq N}}) ⇝ C \leftrightarrow seq M (+ F) ⇝ C)$
10	7 8 9	sylancl	$⊢ (φ \land N \in ℤ_{\geq M}) \to (({seq M (+ F) ↾}_{ℤ_{\geq N}}) ⇝ C \leftrightarrow seq M (+ F) ⇝ C)$
11	2	adantlr	$⊢ ((φ \land N \in ℤ_{\geq M}) \land k \in A) \to B \in ℂ$
12		simpr	$⊢ (φ \land N \in ℤ_{\geq M}) \to N \in ℤ_{\geq M}$
13	1 11 12	sumrblem	$⊢ ((φ \land N \in ℤ_{\geq M}) \land A \subseteq ℤ_{\geq N}) \to {seq M (+ F) ↾}_{ℤ_{\geq N}} = seq N (+ F)$
14	6 13	mpidan	$⊢ (φ \land N \in ℤ_{\geq M}) \to {seq M (+ F) ↾}_{ℤ_{\geq N}} = seq N (+ F)$
15	14	breq1d	$⊢ (φ \land N \in ℤ_{\geq M}) \to (({seq M (+ F) ↾}_{ℤ_{\geq N}}) ⇝ C \leftrightarrow seq N (+ F) ⇝ C)$
16	10 15	bitr3d	$⊢ (φ \land N \in ℤ_{\geq M}) \to (seq M (+ F) ⇝ C \leftrightarrow seq N (+ F) ⇝ C)$
17	2	adantlr	$⊢ ((φ \land M \in ℤ_{\geq N}) \land k \in A) \to B \in ℂ$
18		simpr	$⊢ (φ \land M \in ℤ_{\geq N}) \to M \in ℤ_{\geq N}$
19	1 17 18	sumrblem	$⊢ ((φ \land M \in ℤ_{\geq N}) \land A \subseteq ℤ_{\geq M}) \to {seq N (+ F) ↾}_{ℤ_{\geq M}} = seq M (+ F)$
20	5 19	mpidan	$⊢ (φ \land M \in ℤ_{\geq N}) \to {seq N (+ F) ↾}_{ℤ_{\geq M}} = seq M (+ F)$
21	20	breq1d	$⊢ (φ \land M \in ℤ_{\geq N}) \to (({seq N (+ F) ↾}_{ℤ_{\geq M}}) ⇝ C \leftrightarrow seq M (+ F) ⇝ C)$
22	3	adantr	$⊢ (φ \land M \in ℤ_{\geq N}) \to M \in ℤ$
23		seqex	$⊢ seq N (+ F) \in V$
24		climres	$⊢ (M \in ℤ \land seq N (+ F) \in V) \to (({seq N (+ F) ↾}_{ℤ_{\geq M}}) ⇝ C \leftrightarrow seq N (+ F) ⇝ C)$
25	22 23 24	sylancl	$⊢ (φ \land M \in ℤ_{\geq N}) \to (({seq N (+ F) ↾}_{ℤ_{\geq M}}) ⇝ C \leftrightarrow seq N (+ F) ⇝ C)$
26	21 25	bitr3d	$⊢ (φ \land M \in ℤ_{\geq N}) \to (seq M (+ F) ⇝ C \leftrightarrow seq N (+ F) ⇝ C)$
27		uztric	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \lor M \in ℤ_{\geq N})$
28	3 4 27	syl2anc	$⊢ φ \to (N \in ℤ_{\geq M} \lor M \in ℤ_{\geq N})$
29	16 26 28	mpjaodan	$⊢ φ \to (seq M (+ F) ⇝ C \leftrightarrow seq N (+ F) ⇝ C)$

Metamath Proof Explorer

Theorem sumrb

Proof