sumodd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sumodd		Structured version Visualization version GIF version

Theorem sumodd 16471

Description: If every term in a sum is odd, then the sum is even iff the number of terms in the sum is even. (Contributed by AV, 14-Aug-2021.)

**Hypotheses**
Ref	Expression
sumeven.a	⊢ (𝜑 → 𝐴 ∈ Fin)
sumeven.b	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)
sumodd.o	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 2 ∥ 𝐵)

**Assertion**
Ref	Expression
sumodd	⊢ (𝜑 → (2 ∥ (♯‘𝐴) ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵))

Distinct variable groups: 𝐴,𝑘 𝜑,𝑘 Allowed substitution hint: 𝐵(𝑘)

Proof of Theorem sumodd Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6888	. . . . 5 ⊢ (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
2		hash0 14423	. . . . 5 ⊢ (♯‘∅) = 0
3	1, 2	eqtrdi 2817	. . . 4 ⊢ (𝑥 = ∅ → (♯‘𝑥) = 0)
4	3	breq2d 5126	. . 3 ⊢ (𝑥 = ∅ → (2 ∥ (♯‘𝑥) ↔ 2 ∥ 0))
5		sumeq1 15766	. . . . 5 ⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ ∅ 𝐵)
6		sum0 15798	. . . . 5 ⊢ Σ𝑘 ∈ ∅ 𝐵 = 0
7	5, 6	eqtrdi 2817	. . . 4 ⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = 0)
8	7	breq2d 5126	. . 3 ⊢ (𝑥 = ∅ → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ 0))
9	4, 8	bibi12d 348	. 2 ⊢ (𝑥 = ∅ → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ 0 ↔ 2 ∥ 0)))
10		fveq2 6888	. . . 4 ⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
11	10	breq2d 5126	. . 3 ⊢ (𝑥 = 𝑦 → (2 ∥ (♯‘𝑥) ↔ 2 ∥ (♯‘𝑦)))
12		sumeq1 15766	. . . 4 ⊢ (𝑥 = 𝑦 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝑦 𝐵)
13	12	breq2d 5126	. . 3 ⊢ (𝑥 = 𝑦 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵))
14	11, 13	bibi12d 348	. 2 ⊢ (𝑥 = 𝑦 → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)))
15		fveq2 6888	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
16	15	breq2d 5126	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ (♯‘𝑥) ↔ 2 ∥ (♯‘(𝑦 ∪ {𝑧}))))
17		sumeq1 15766	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)
18	17	breq2d 5126	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵))
19	16, 18	bibi12d 348	. 2 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)))
20		fveq2 6888	. . . 4 ⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
21	20	breq2d 5126	. . 3 ⊢ (𝑥 = 𝐴 → (2 ∥ (♯‘𝑥) ↔ 2 ∥ (♯‘𝐴)))
22		sumeq1 15766	. . . 4 ⊢ (𝑥 = 𝐴 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝐴 𝐵)
23	22	breq2d 5126	. . 3 ⊢ (𝑥 = 𝐴 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵))
24	21, 23	bibi12d 348	. 2 ⊢ (𝑥 = 𝐴 → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘𝐴) ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵)))
25		biidd 265	. 2 ⊢ (𝜑 → (2 ∥ 0 ↔ 2 ∥ 0))
26		eldifi 4088	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → 𝑧 ∈ 𝐴)
27	26	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑧 ∈ 𝐴)
28	27	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ 𝐴)
29		sumeven.b	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)
30	29	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)
31	30	ralrimiva 3160	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ)
32		rspcsbela 4406	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ)
33	28, 31, 32	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ)
34		sumodd.o	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 2 ∥ 𝐵)
35	34	ralrimiva 3160	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵)
36		nfcv 2928	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘2
37		nfcv 2928	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘 ∥
38		nfcsb1v 3880	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵
39	36, 37, 38	nfbr 5163	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘2 ∥ ⦋𝑧 / 𝑘⦌𝐵
40	39	nfn 1890	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵
41		csbeq1a 3870	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑘⦌𝐵)
42	41	breq2d 5126	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑧 → (2 ∥ 𝐵 ↔ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
43	42	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → (¬ 2 ∥ 𝐵 ↔ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
44	40, 43	rspc 3572	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵 → ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
45	26, 35, 44	syl2imc 42	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑧 ∈ (𝐴 ∖ 𝑦) → ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
46	45	a1d 26	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ⊆ 𝐴 → (𝑧 ∈ (𝐴 ∖ 𝑦) → ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)))
47	46	imp32 424	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)
48	33, 47	jca 521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
49	48	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
50		sumeven.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ Fin)
51		ssfi 9167	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Fin ∧ 𝑦 ⊆ 𝐴) → 𝑦 ∈ Fin)
52	51	expcom 419	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝐴 → (𝐴 ∈ Fin → 𝑦 ∈ Fin))
53	52	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝐴 ∈ Fin → 𝑦 ∈ Fin))
54	50, 53	mpan9 516	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin)
55		simpll 779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝜑)
56		ssel 3934	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ⊆ 𝐴 → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴))
57	56	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴))
58	57	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ 𝑦 → 𝑘 ∈ 𝐴))
59	58	imp 412	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝐴)
60	55, 59, 29	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝑦) → 𝐵 ∈ ℤ)
61	54, 60	fsumzcl 15812	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ)
62	61	anim1i 627	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵))
63		opeo 16448	. . . . . . . . 9 ⊢ (((⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵) ∧ (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) → ¬ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))
64	49, 62, 63	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → ¬ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))
65	61	zcnd 12719	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℂ)
66	33	zcnd 12719	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ)
67		addcom 11414	. . . . . . . . . . . 12 ⊢ ((Σ𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) = (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))
68	67	breq2d 5126	. . . . . . . . . . 11 ⊢ ((Σ𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)))
69	68	notbid 321	. . . . . . . . . 10 ⊢ ((Σ𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)))
70	65, 66, 69	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)))
71	70	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵)))
72	64, 71	mpbird 260	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))
73	72	ex 418	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 → ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))
74	61	anim1i 627	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵))
75	48	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
76		opoe 16446	. . . . . . . . 9 ⊢ (((Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) ∧ (⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵)) → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))
77	74, 75, 76	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ ¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))
78	77	ex 418	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵 → 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))
79	78	con1d 146	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) → 2 ∥ Σ𝑘 ∈ 𝑦 𝐵))
80	73, 79	impbid 215	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))
81		bitr3 355	. . . . 5 ⊢ ((2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) → ((2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ((♯‘𝑦) + 1)) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ ((♯‘𝑦) + 1))))
82	80, 81	syl 18	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ((♯‘𝑦) + 1)) → (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ ((♯‘𝑦) + 1))))
83		bicom 225	. . . 4 ⊢ ((¬ 2 ∥ ((♯‘𝑦) + 1) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) ↔ (2 ∥ Σ𝑘 ∈ 𝑦 𝐵 ↔ ¬ 2 ∥ ((♯‘𝑦) + 1)))
84		bicom 225	. . . 4 ⊢ ((¬ 2 ∥ ((♯‘𝑦) + 1) ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) ↔ (¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) ↔ ¬ 2 ∥ ((♯‘𝑦) + 1)))
85	82, 83, 84	3imtr4g 299	. . 3 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((¬ 2 ∥ ((♯‘𝑦) + 1) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (¬ 2 ∥ ((♯‘𝑦) + 1) ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))))
86		notnotb 318	. . . . 5 ⊢ (2 ∥ (♯‘𝑦) ↔ ¬ ¬ 2 ∥ (♯‘𝑦))
87		hashcl 14412	. . . . . . . . 9 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
88	54, 87	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝑦) ∈ ℕ₀)
89	88	nn0zd 12634	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝑦) ∈ ℤ)
90		oddp1even 16427	. . . . . . 7 ⊢ ((♯‘𝑦) ∈ ℤ → (¬ 2 ∥ (♯‘𝑦) ↔ 2 ∥ ((♯‘𝑦) + 1)))
91	89, 90	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ 2 ∥ (♯‘𝑦) ↔ 2 ∥ ((♯‘𝑦) + 1)))
92	91	notbid 321	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (¬ ¬ 2 ∥ (♯‘𝑦) ↔ ¬ 2 ∥ ((♯‘𝑦) + 1)))
93	86, 92	bitrid 286	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ (♯‘𝑦) ↔ ¬ 2 ∥ ((♯‘𝑦) + 1)))
94	93	bibi1d 346	. . 3 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (♯‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) ↔ (¬ 2 ∥ ((♯‘𝑦) + 1) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)))
95		simprr 785	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐴 ∖ 𝑦))
96		eldifn 4089	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ¬ 𝑧 ∈ 𝑦)
97	96	adantl 487	. . . . . . . . 9 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → ¬ 𝑧 ∈ 𝑦)
98	97	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦)
99	54, 98	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦))
100		hashunsng 14448	. . . . . . 7 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
101	95, 99, 100	sylc 66	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
102	101	breq2d 5126	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ ((♯‘𝑦) + 1)))
103		vex 3462	. . . . . . . 8 ⊢ 𝑧 ∈ V
104	103	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ V)
105		df-nel 3068	. . . . . . . 8 ⊢ (𝑧 ∉ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦)
106	98, 105	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∉ 𝑦)
107		simpll 779	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝜑)
108		elun 4110	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}))
109	57	com12 33	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑦 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴))
110		elsni 4611	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ {𝑧} → 𝑘 = 𝑧)
111		eleq1w 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑧 → (𝑘 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
112	27, 111	imbitrrid 249	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴))
113	110, 112	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ {𝑧} → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴))
114	109, 113	jaoi 871	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴))
115	108, 114	sylbi 220	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴))
116	115	com12 33	. . . . . . . . . . 11 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → (𝑘 ∈ (𝑦 ∪ {𝑧}) → 𝑘 ∈ 𝐴))
117	116	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑘 ∈ (𝑦 ∪ {𝑧}) → 𝑘 ∈ 𝐴))
118	117	imp 412	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐴)
119	107, 118, 29	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐵 ∈ ℤ)
120	119	ralrimiva 3160	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ)
121		fsumsplitsnun 15832	. . . . . . 7 ⊢ ((𝑦 ∈ Fin ∧ (𝑧 ∈ V ∧ 𝑧 ∉ 𝑦) ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))
122	54, 104, 106, 120, 121	syl121anc 1402	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))
123	122	breq2d 5126	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ↔ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))
124	102, 123	bibi12d 348	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) ↔ (2 ∥ ((♯‘𝑦) + 1) ↔ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))))
125		notbi 322	. . . 4 ⊢ ((2 ∥ ((♯‘𝑦) + 1) ↔ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)) ↔ (¬ 2 ∥ ((♯‘𝑦) + 1) ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵)))
126	124, 125	bitrdi 290	. . 3 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵) ↔ (¬ 2 ∥ ((♯‘𝑦) + 1) ↔ ¬ 2 ∥ (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))))
127	85, 94, 126	3imtr4d 297	. 2 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((2 ∥ (♯‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)))
128	9, 14, 19, 24, 25, 127, 50	findcard2d 9161	1 ⊢ (𝜑 → (2 ∥ (♯‘𝐴) ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2146 ∉ wnel 3067 ∀wral 3082 Vcvv 3458 ⦋csb 3856 ∖ cdif 3905 ∪ cun 3906 ⊆ wss 3908 ∅c0 4289 {csn 4594 class class class wbr 5114 ‘cfv 6543 (class class class)co 7423 Fincfn 8952 ℂcc 11116 0cc0 11118 1c1 11119 + caddc 11121 2c2 12313 ℕ₀cn0 12522 ℤcz 12609 ♯chash 14386 Σcsu 15763 ∥ cdvds 16335

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-inf2 9620 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-oadd 8466 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-oi 9482 df-dju 9906 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-n0 12523 df-z 12610 df-uz 12881 df-rp 13035 df-fz 13554 df-fzo 13702 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-sum 15764 df-dvds 16336

This theorem is used by: evensumodd 16472 oddsumodd 16473 vtxdgoddnumeven 29940

W3C validator