smuval2 - Metamath Proof Explorer

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

Theorem smuval2 16419

Description: The partial sum sequence stabilizes at 𝑁 after the 𝑁 + 1-th element of the sequence; this stable value is the value of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.)

**Hypotheses**
Ref	Expression
smuval.a	⊢ (𝜑 → 𝐴 ⊆ ℕ₀)
smuval.b	⊢ (𝜑 → 𝐵 ⊆ ℕ₀)
smuval.p	⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ₀, 𝑚 ∈ ℕ₀ ↦ (𝑝 sadd {𝑛 ∈ ℕ₀ ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
smuval.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
smuval2.m	⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(𝑁 + 1)))

**Assertion**
Ref	Expression
smuval2	⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))

Distinct variable groups: 𝑚,𝑛,𝑝,𝐴 𝑛,𝑁 𝜑,𝑛 𝐵,𝑚,𝑛,𝑝 Allowed substitution hints: 𝜑(𝑚,𝑝) 𝑃(𝑚,𝑛,𝑝) 𝑀(𝑚,𝑛,𝑝) 𝑁(𝑚,𝑝)

Proof of Theorem smuval2 Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		smuval2.m	. 2 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(𝑁 + 1)))
2		fveq2 6888	. . . . . 6 ⊢ (𝑥 = (𝑁 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑁 + 1)))
3	2	eleq2d 2819	. . . . 5 ⊢ (𝑥 = (𝑁 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))
4	3	bibi2d 342	. . . 4 ⊢ (𝑥 = (𝑁 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))))
5	4	imbi2d 340	. . 3 ⊢ (𝑥 = (𝑁 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))))
6		fveq2 6888	. . . . . 6 ⊢ (𝑥 = 𝑘 → (𝑃‘𝑥) = (𝑃‘𝑘))
7	6	eleq2d 2819	. . . . 5 ⊢ (𝑥 = 𝑘 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑘)))
8	7	bibi2d 342	. . . 4 ⊢ (𝑥 = 𝑘 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))))
9	8	imbi2d 340	. . 3 ⊢ (𝑥 = 𝑘 → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)))))
10		fveq2 6888	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → (𝑃‘𝑥) = (𝑃‘(𝑘 + 1)))
11	10	eleq2d 2819	. . . . 5 ⊢ (𝑥 = (𝑘 + 1) → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))
12	11	bibi2d 342	. . . 4 ⊢ (𝑥 = (𝑘 + 1) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))
13	12	imbi2d 340	. . 3 ⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))))
14		fveq2 6888	. . . . . 6 ⊢ (𝑥 = 𝑀 → (𝑃‘𝑥) = (𝑃‘𝑀))
15	14	eleq2d 2819	. . . . 5 ⊢ (𝑥 = 𝑀 → (𝑁 ∈ (𝑃‘𝑥) ↔ 𝑁 ∈ (𝑃‘𝑀)))
16	15	bibi2d 342	. . . 4 ⊢ (𝑥 = 𝑀 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥)) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))))
17	16	imbi2d 340	. . 3 ⊢ (𝑥 = 𝑀 → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑥))) ↔ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))))
18		smuval.a	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ ℕ₀)
19		smuval.b	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ ℕ₀)
20		smuval.p	. . . 4 ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ₀, 𝑚 ∈ ℕ₀ ↦ (𝑝 sadd {𝑛 ∈ ℕ₀ ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
21		smuval.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
22	18, 19, 20, 21	smuval 16418	. . 3 ⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1))))
23	18	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝐴 ⊆ ℕ₀)
24	19	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝐵 ⊆ ℕ₀)
25		peano2nn0 12508	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
26	21, 25	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ₀)
27		eluznn0 12897	. . . . . . . . . . 11 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝑘 ∈ ℕ₀)
28	26, 27	sylan 580	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝑘 ∈ ℕ₀)
29	23, 24, 20, 28	smupp1 16417	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑃‘(𝑘 + 1)) = ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}))
30	29	eleq2d 2819	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)})))
31	23, 24, 20	smupf 16415	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝑃:ℕ₀⟶𝒫 ℕ₀)
32	31, 28	ffvelcdmd 7084	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑃‘𝑘) ∈ 𝒫 ℕ₀)
33	32	elpwid 4610	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑃‘𝑘) ⊆ ℕ₀)
34		ssrab2 4076	. . . . . . . . . . . . . 14 ⊢ {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆ ℕ₀
35	34	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ⊆ ℕ₀)
36	26	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑁 + 1) ∈ ℕ₀)
37	33, 35, 36	sadeq 16409	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))))
38		inrab2 4306	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = {𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1))) ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}
39		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1))))
40	39	elin1d 4197	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑛 ∈ ℕ₀)
41	40	nn0red 12529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑛 ∈ ℝ)
42	21	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝑁 ∈ ℕ₀)
43	42	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑁 ∈ ℕ₀)
44	43	nn0red 12529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑁 ∈ ℝ)
45		1red 11211	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 1 ∈ ℝ)
46	44, 45	readdcld 11239	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → (𝑁 + 1) ∈ ℝ)
47	28	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑘 ∈ ℕ₀)
48	47	nn0red 12529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑘 ∈ ℝ)
49	39	elin2d 4198	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑛 ∈ (0..^(𝑁 + 1)))
50		elfzolt2 13637	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (0..^(𝑁 + 1)) → 𝑛 < (𝑁 + 1))
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑛 < (𝑁 + 1))
52		eluzle 12831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ (ℤ_≥‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑘)
53	52	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → (𝑁 + 1) ≤ 𝑘)
54	41, 46, 48, 51, 53	ltletrd 11370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝑛 < 𝑘)
55	41, 48	ltnled 11357	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → (𝑛 < 𝑘 ↔ ¬ 𝑘 ≤ 𝑛))
56	54, 55	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → ¬ 𝑘 ≤ 𝑛)
57	24	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → 𝐵 ⊆ ℕ₀)
58	57	sseld 3980	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → ((𝑛 − 𝑘) ∈ 𝐵 → (𝑛 − 𝑘) ∈ ℕ₀))
59		nn0ge0 12493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 − 𝑘) ∈ ℕ₀ → 0 ≤ (𝑛 − 𝑘))
60	58, 59	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → ((𝑛 − 𝑘) ∈ 𝐵 → 0 ≤ (𝑛 − 𝑘)))
61	41, 48	subge0d 11800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → (0 ≤ (𝑛 − 𝑘) ↔ 𝑘 ≤ 𝑛))
62	60, 61	sylibd 238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → ((𝑛 − 𝑘) ∈ 𝐵 → 𝑘 ≤ 𝑛))
63	62	adantld 491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → ((𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵) → 𝑘 ≤ 𝑛))
64	56, 63	mtod 197	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) ∧ 𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1)))) → ¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵))
65	64	ralrimiva 3146	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → ∀𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1))) ¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵))
66		rabeq0 4383	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1))) ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅ ↔ ∀𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1))) ¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵))
67	65, 66	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → {𝑛 ∈ (ℕ₀ ∩ (0..^(𝑁 + 1))) ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} = ∅)
68	38, 67	eqtrid 2784	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → ({𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1))) = ∅)
69	68	oveq2d 7421	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅))
70		inss1 4227	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ (𝑃‘𝑘)
71	70, 33	sstrid 3992	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ ℕ₀)
72		sadid1 16405	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ⊆ ℕ₀ → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))
73	71, 72	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ∅) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))
74	69, 73	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))
75	74	ineq1d 4210	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))))
76		inass 4218	. . . . . . . . . . . . . 14 ⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1))))
77		inidm 4217	. . . . . . . . . . . . . . 15 ⊢ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1))) = (0..^(𝑁 + 1))
78	77	ineq2i 4208	. . . . . . . . . . . . . 14 ⊢ ((𝑃‘𝑘) ∩ ((0..^(𝑁 + 1)) ∩ (0..^(𝑁 + 1)))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))
79	76, 78	eqtri 2760	. . . . . . . . . . . . 13 ⊢ (((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))
80	75, 79	eqtrdi 2788	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → ((((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) sadd ({𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)} ∩ (0..^(𝑁 + 1)))) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))
81	37, 80	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) = ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))))
82	81	eleq2d 2819	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ 𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1)))))
83		elin 3963	. . . . . . . . . 10 ⊢ (𝑁 ∈ (((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))
84		elin 3963	. . . . . . . . . 10 ⊢ (𝑁 ∈ ((𝑃‘𝑘) ∩ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1))))
85	82, 83, 84	3bitr3g 312	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → ((𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1))) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))))
86		nn0uz 12860	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
87	42, 86	eleqtrdi 2843	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝑁 ∈ (ℤ_≥‘0))
88		eluzfz2 13505	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘0) → 𝑁 ∈ (0...𝑁))
89	87, 88	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝑁 ∈ (0...𝑁))
90	42	nn0zd 12580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝑁 ∈ ℤ)
91		fzval3 13697	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℤ → (0...𝑁) = (0..^(𝑁 + 1)))
92	90, 91	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (0...𝑁) = (0..^(𝑁 + 1)))
93	89, 92	eleqtrd 2835	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1)))
94	93	biantrud 532	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))))
95	93	biantrud 532	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘𝑘) ↔ (𝑁 ∈ (𝑃‘𝑘) ∧ 𝑁 ∈ (0..^(𝑁 + 1)))))
96	85, 94, 95	3bitr4d 310	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑁 ∈ ((𝑃‘𝑘) sadd {𝑛 ∈ ℕ₀ ∣ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)}) ↔ 𝑁 ∈ (𝑃‘𝑘)))
97	30, 96	bitrd 278	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → (𝑁 ∈ (𝑃‘(𝑘 + 1)) ↔ 𝑁 ∈ (𝑃‘𝑘)))
98	97	bibi2d 342	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))) ↔ (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))))
99	98	biimprd 247	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝑁 + 1))) → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1)))))
100	99	expcom 414	. . . 4 ⊢ (𝑘 ∈ (ℤ_≥‘(𝑁 + 1)) → (𝜑 → ((𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘)) → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))))
101	100	a2d 29	. . 3 ⊢ (𝑘 ∈ (ℤ_≥‘(𝑁 + 1)) → ((𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑘))) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑘 + 1))))))
102	5, 9, 13, 17, 22, 101	uzind4i 12890	. 2 ⊢ (𝑀 ∈ (ℤ_≥‘(𝑁 + 1)) → (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))))
103	1, 102	mpcom 38	1 ⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 {crab 3432 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 ifcif 4527 𝒫 cpw 4601 class class class wbr 5147 ↦ cmpt 5230 ‘cfv 6540 (class class class)co 7405 ∈ cmpo 7407 0cc0 11106 1c1 11107 + caddc 11109 < clt 11244 ≤ cle 11245 − cmin 11440 ℕ₀cn0 12468 ℤcz 12554 ℤ_≥cuz 12818 ...cfz 13480 ..^cfzo 13623 seqcseq 13962 sadd csad 16357 smul csmu 16358

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-inf2 9632 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-xor 1510 df-tru 1544 df-fal 1554 df-had 1595 df-cad 1608 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-disj 5113 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-oadd 8466 df-er 8699 df-map 8818 df-pm 8819 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-inf 9434 df-oi 9501 df-dju 9892 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-xnn0 12541 df-z 12555 df-uz 12819 df-rp 12971 df-fz 13481 df-fzo 13624 df-fl 13753 df-mod 13831 df-seq 13963 df-exp 14024 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-clim 15428 df-sum 15629 df-dvds 16194 df-bits 16359 df-sad 16388 df-smu 16413

This theorem is referenced by: smupvallem 16420 smueqlem 16427

W3C validator