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 16538

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 6877	. . . . 5 ⊢ (𝑥 = ∅ → (♯‘𝑥) = (♯‘∅))
2		hash0 14491	. . . . 5 ⊢ (♯‘∅) = 0
3	1, 2	eqtrdi 2812	. . . 4 ⊢ (𝑥 = ∅ → (♯‘𝑥) = 0)
4	3	breq2d 5115	. . 3 ⊢ (𝑥 = ∅ → (2 ∥ (♯‘𝑥) ↔ 2 ∥ 0))
5		sumeq1 15836	. . . . 5 ⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ ∅ 𝐵)
6		sum0 15867	. . . . 5 ⊢ Σ𝑘 ∈ ∅ 𝐵 = 0
7	5, 6	eqtrdi 2812	. . . 4 ⊢ (𝑥 = ∅ → Σ𝑘 ∈ 𝑥 𝐵 = 0)
8	7	breq2d 5115	. . 3 ⊢ (𝑥 = ∅ → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ 0))
9	4, 8	bibi12d 348	. 2 ⊢ (𝑥 = ∅ → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ 0 ↔ 2 ∥ 0)))
10		fveq2 6877	. . . 4 ⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
11	10	breq2d 5115	. . 3 ⊢ (𝑥 = 𝑦 → (2 ∥ (♯‘𝑥) ↔ 2 ∥ (♯‘𝑦)))
12		sumeq1 15836	. . . 4 ⊢ (𝑥 = 𝑦 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝑦 𝐵)
13	12	breq2d 5115	. . 3 ⊢ (𝑥 = 𝑦 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵))
14	11, 13	bibi12d 348	. 2 ⊢ (𝑥 = 𝑦 → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘𝑦) ↔ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)))
15		fveq2 6877	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧})))
16	15	breq2d 5115	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ (♯‘𝑥) ↔ 2 ∥ (♯‘(𝑦 ∪ {𝑧}))))
17		sumeq1 15836	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)
18	17	breq2d 5115	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵))
19	16, 18	bibi12d 348	. 2 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵)))
20		fveq2 6877	. . . 4 ⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
21	20	breq2d 5115	. . 3 ⊢ (𝑥 = 𝐴 → (2 ∥ (♯‘𝑥) ↔ 2 ∥ (♯‘𝐴)))
22		sumeq1 15836	. . . 4 ⊢ (𝑥 = 𝐴 → Σ𝑘 ∈ 𝑥 𝐵 = Σ𝑘 ∈ 𝐴 𝐵)
23	22	breq2d 5115	. . 3 ⊢ (𝑥 = 𝐴 → (2 ∥ Σ𝑘 ∈ 𝑥 𝐵 ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵))
24	21, 23	bibi12d 348	. 2 ⊢ (𝑥 = 𝐴 → ((2 ∥ (♯‘𝑥) ↔ 2 ∥ Σ𝑘 ∈ 𝑥 𝐵) ↔ (2 ∥ (♯‘𝐴) ↔ 2 ∥ Σ𝑘 ∈ 𝐴 𝐵)))
25		biidd 265	. 2 ⊢ (𝜑 → (2 ∥ 0 ↔ 2 ∥ 0))
26		eldifi 4078	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → 𝑧 ∈ 𝐴)
27	26	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑧 ∈ 𝐴)
28	27	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ 𝐴)
29		sumeven.b	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)
30	29	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)
31	30	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ)
32		rspcsbela 4396	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ)
33	28, 31, 32	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ)
34		sumodd.o	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 2 ∥ 𝐵)
35	34	ralrimiva 3155	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ¬ 2 ∥ 𝐵)
36		nfcv 2923	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘2
37		nfcv 2923	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘 ∥
38		nfcsb1v 3871	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐵
39	36, 37, 38	nfbr 5152	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘2 ∥ ⦋𝑧 / 𝑘⦌𝐵
40	39	nfn 1890	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘 ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵
41		csbeq1a 3861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑘⦌𝐵)
42	41	breq2d 5115	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑧 → (2 ∥ 𝐵 ↔ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
43	42	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → (¬ 2 ∥ 𝐵 ↔ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵))
44	40, 43	rspc 3565	. . . . . . . . . . . . . 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 9172	. . . . . . . . . . . . . 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 3925	. . . . . . . . . . . . . . 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 15881	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ)
62	61	anim1i 627	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵))
63		opeo 16515	. . . . . . . . 9 ⊢ (((⦋𝑧 / 𝑘⦌𝐵 ∈ ℤ ∧ ¬ 2 ∥ ⦋𝑧 / 𝑘⦌𝐵) ∧ (Σ𝑘 ∈ 𝑦 𝐵 ∈ ℤ ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵)) → ¬ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))
64	49, 62, 63	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 2 ∥ Σ𝑘 ∈ 𝑦 𝐵) → ¬ 2 ∥ (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))
65	61	zcnd 12785	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ 𝑦 𝐵 ∈ ℂ)
66	33	zcnd 12785	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ)
67		addcom 11477	. . . . . . . . . . . 12 ⊢ ((Σ𝑘 ∈ 𝑦 𝐵 ∈ ℂ ∧ ⦋𝑧 / 𝑘⦌𝐵 ∈ ℂ) → (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵) = (⦋𝑧 / 𝑘⦌𝐵 + Σ𝑘 ∈ 𝑦 𝐵))
68	67	breq2d 5115	. . . . . . . . . . 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 16513	. . . . . . . . 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 14480	. . . . . . . . 9 ⊢ (𝑦 ∈ Fin → (♯‘𝑦) ∈ ℕ₀)
88	54, 87	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝑦) ∈ ℕ₀)
89	88	nn0zd 12699	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝑦) ∈ ℤ)
90		oddp1even 16494	. . . . . . 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 4079	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ¬ 𝑧 ∈ 𝑦)
97	96	adantl 487	. . . . . . . . 9 ⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → ¬ 𝑧 ∈ 𝑦)
98	97	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦)
99	54, 98	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦))
100		hashunsng 14516	. . . . . . 7 ⊢ (𝑧 ∈ (𝐴 ∖ 𝑦) → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)))
101	95, 99, 100	sylc 66	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))
102	101	breq2d 5115	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (2 ∥ (♯‘(𝑦 ∪ {𝑧})) ↔ 2 ∥ ((♯‘𝑦) + 1)))
103		vex 3455	. . . . . . . 8 ⊢ 𝑧 ∈ V
104	103	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ V)
105		df-nel 3063	. . . . . . . 8 ⊢ (𝑧 ∉ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦)
106	98, 105	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∉ 𝑦)
107		simpll 779	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝜑)
108		elun 4100	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝑦 ∪ {𝑧}) ↔ (𝑘 ∈ 𝑦 ∨ 𝑘 ∈ {𝑧}))
109	57	com12 33	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ 𝑦 → ((𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦)) → 𝑘 ∈ 𝐴))
110		elsni 4601	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ {𝑧} → 𝑘 = 𝑧)
111		eleq1w 2844	. . . . . . . . . . . . . . . 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 3155	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ)
121		fsumsplitsnun 15901	. . . . . . 7 ⊢ ((𝑦 ∈ Fin ∧ (𝑧 ∈ V ∧ 𝑧 ∉ 𝑦) ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))
122	54, 104, 106, 120, 121	syl121anc 1402	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐵 = (Σ𝑘 ∈ 𝑦 𝐵 + ⦋𝑧 / 𝑘⦌𝐵))
123	122	breq2d 5115	. . . . 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 9166	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 2145 ∉ wnel 3062 ∀wral 3077 Vcvv 3451 ⦋csb 3847 ∖ cdif 3896 ∪ cun 3897 ⊆ wss 3899 ∅c0 4279 {csn 4584 class class class wbr 5103 ‘cfv 6531 (class class class)co 7412 Fincfn 8957 ℂcc 11179 0cc0 11181 1c1 11182 + caddc 11184 2c2 12378 ℕ₀cn0 12587 ℤcz 12674 ♯chash 14454 Σcsu 15833 ∥ cdvds 16402

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-oadd 8464 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-sup 9418 df-oi 9488 df-dju 9963 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-n0 12588 df-z 12675 df-uz 12947 df-rp 13102 df-fz 13621 df-fzo 13769 df-seq 14125 df-exp 14185 df-hash 14455 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-clim 15635 df-sum 15834 df-dvds 16403

This theorem is used by: evensumodd 16539 oddsumodd 16540 vtxdgoddnumeven 30116

W3C validator