# Metamath Proof Explorer

## Theorem smuval2

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

Ref Expression
Hypotheses smuval.a ${⊢}{\phi }\to {A}\subseteq {ℕ}_{0}$
smuval.b ${⊢}{\phi }\to {B}\subseteq {ℕ}_{0}$
smuval.p ${⊢}{P}=seq0\left(\left({p}\in 𝒫{ℕ}_{0},{m}\in {ℕ}_{0}⟼{p}\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({m}\in {A}\wedge {n}-{m}\in {B}\right)\right\}\right),\left({n}\in {ℕ}_{0}⟼if\left({n}=0,\varnothing ,{n}-1\right)\right)\right)$
smuval.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
smuval2.m ${⊢}{\phi }\to {M}\in {ℤ}_{\ge \left({N}+1\right)}$
Assertion smuval2 ${⊢}{\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({M}\right)\right)$

### Proof

Step Hyp Ref Expression
1 smuval.a ${⊢}{\phi }\to {A}\subseteq {ℕ}_{0}$
2 smuval.b ${⊢}{\phi }\to {B}\subseteq {ℕ}_{0}$
3 smuval.p ${⊢}{P}=seq0\left(\left({p}\in 𝒫{ℕ}_{0},{m}\in {ℕ}_{0}⟼{p}\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({m}\in {A}\wedge {n}-{m}\in {B}\right)\right\}\right),\left({n}\in {ℕ}_{0}⟼if\left({n}=0,\varnothing ,{n}-1\right)\right)\right)$
4 smuval.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
5 smuval2.m ${⊢}{\phi }\to {M}\in {ℤ}_{\ge \left({N}+1\right)}$
6 fveq2 ${⊢}{x}={N}+1\to {P}\left({x}\right)={P}\left({N}+1\right)$
7 6 eleq2d ${⊢}{x}={N}+1\to \left({N}\in {P}\left({x}\right)↔{N}\in {P}\left({N}+1\right)\right)$
8 7 bibi2d ${⊢}{x}={N}+1\to \left(\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({x}\right)\right)↔\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({N}+1\right)\right)\right)$
9 8 imbi2d ${⊢}{x}={N}+1\to \left(\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({x}\right)\right)\right)↔\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({N}+1\right)\right)\right)\right)$
10 fveq2 ${⊢}{x}={k}\to {P}\left({x}\right)={P}\left({k}\right)$
11 10 eleq2d ${⊢}{x}={k}\to \left({N}\in {P}\left({x}\right)↔{N}\in {P}\left({k}\right)\right)$
12 11 bibi2d ${⊢}{x}={k}\to \left(\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({x}\right)\right)↔\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}\right)\right)\right)$
13 12 imbi2d ${⊢}{x}={k}\to \left(\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({x}\right)\right)\right)↔\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}\right)\right)\right)\right)$
14 fveq2 ${⊢}{x}={k}+1\to {P}\left({x}\right)={P}\left({k}+1\right)$
15 14 eleq2d ${⊢}{x}={k}+1\to \left({N}\in {P}\left({x}\right)↔{N}\in {P}\left({k}+1\right)\right)$
16 15 bibi2d ${⊢}{x}={k}+1\to \left(\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({x}\right)\right)↔\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}+1\right)\right)\right)$
17 16 imbi2d ${⊢}{x}={k}+1\to \left(\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({x}\right)\right)\right)↔\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}+1\right)\right)\right)\right)$
18 fveq2 ${⊢}{x}={M}\to {P}\left({x}\right)={P}\left({M}\right)$
19 18 eleq2d ${⊢}{x}={M}\to \left({N}\in {P}\left({x}\right)↔{N}\in {P}\left({M}\right)\right)$
20 19 bibi2d ${⊢}{x}={M}\to \left(\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({x}\right)\right)↔\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({M}\right)\right)\right)$
21 20 imbi2d ${⊢}{x}={M}\to \left(\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({x}\right)\right)\right)↔\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({M}\right)\right)\right)\right)$
22 1 2 3 4 smuval ${⊢}{\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({N}+1\right)\right)$
23 1 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {A}\subseteq {ℕ}_{0}$
24 2 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {B}\subseteq {ℕ}_{0}$
25 peano2nn0 ${⊢}{N}\in {ℕ}_{0}\to {N}+1\in {ℕ}_{0}$
26 4 25 syl ${⊢}{\phi }\to {N}+1\in {ℕ}_{0}$
27 eluznn0 ${⊢}\left({N}+1\in {ℕ}_{0}\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {k}\in {ℕ}_{0}$
28 26 27 sylan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {k}\in {ℕ}_{0}$
29 23 24 3 28 smupp1 ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {P}\left({k}+1\right)={P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}$
30 29 eleq2d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({N}\in {P}\left({k}+1\right)↔{N}\in \left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)\right)$
31 23 24 3 smupf ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {P}:{ℕ}_{0}⟶𝒫{ℕ}_{0}$
32 31 28 ffvelrnd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {P}\left({k}\right)\in 𝒫{ℕ}_{0}$
33 32 elpwid ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {P}\left({k}\right)\subseteq {ℕ}_{0}$
34 ssrab2 ${⊢}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\subseteq {ℕ}_{0}$
35 34 a1i ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\subseteq {ℕ}_{0}$
36 26 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}+1\in {ℕ}_{0}$
37 33 35 36 sadeq ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)\cap \left(0..^{N}+1\right)=\left(\left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\mathrm{sadd}\left(\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\cap \left(0..^{N}+1\right)\right)\right)\cap \left(0..^{N}+1\right)$
38 inrab2 ${⊢}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\cap \left(0..^{N}+1\right)=\left\{{n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}$
39 simpr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)$
40 39 elin1d ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {n}\in {ℕ}_{0}$
41 40 nn0red ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {n}\in ℝ$
42 4 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}\in {ℕ}_{0}$
43 42 adantr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {N}\in {ℕ}_{0}$
44 43 nn0red ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {N}\in ℝ$
45 1red ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to 1\in ℝ$
46 44 45 readdcld ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {N}+1\in ℝ$
47 28 adantr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {k}\in {ℕ}_{0}$
48 47 nn0red ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {k}\in ℝ$
49 39 elin2d ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {n}\in \left(0..^{N}+1\right)$
50 elfzolt2 ${⊢}{n}\in \left(0..^{N}+1\right)\to {n}<{N}+1$
51 49 50 syl ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {n}<{N}+1$
52 eluzle ${⊢}{k}\in {ℤ}_{\ge \left({N}+1\right)}\to {N}+1\le {k}$
53 52 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {N}+1\le {k}$
54 41 46 48 51 53 ltletrd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {n}<{k}$
55 41 48 ltnled ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to \left({n}<{k}↔¬{k}\le {n}\right)$
56 54 55 mpbid ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to ¬{k}\le {n}$
57 24 adantr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to {B}\subseteq {ℕ}_{0}$
58 57 sseld ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to \left({n}-{k}\in {B}\to {n}-{k}\in {ℕ}_{0}\right)$
59 nn0ge0 ${⊢}{n}-{k}\in {ℕ}_{0}\to 0\le {n}-{k}$
60 58 59 syl6 ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to \left({n}-{k}\in {B}\to 0\le {n}-{k}\right)$
61 41 48 subge0d ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to \left(0\le {n}-{k}↔{k}\le {n}\right)$
62 60 61 sylibd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to \left({n}-{k}\in {B}\to {k}\le {n}\right)$
63 62 adantld ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to \left(\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\to {k}\le {n}\right)$
64 56 63 mtod ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\wedge {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\right)\to ¬\left({k}\in {A}\wedge {n}-{k}\in {B}\right)$
65 64 ralrimiva ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \forall {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\phantom{\rule{.4em}{0ex}}¬\left({k}\in {A}\wedge {n}-{k}\in {B}\right)$
66 rabeq0 ${⊢}\left\{{n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}=\varnothing ↔\forall {n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)\phantom{\rule{.4em}{0ex}}¬\left({k}\in {A}\wedge {n}-{k}\in {B}\right)$
67 65 66 sylibr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left\{{n}\in \left({ℕ}_{0}\cap \left(0..^{N}+1\right)\right)|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}=\varnothing$
68 38 67 syl5eq ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\cap \left(0..^{N}+1\right)=\varnothing$
69 68 oveq2d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\mathrm{sadd}\left(\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\cap \left(0..^{N}+1\right)\right)=\left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\mathrm{sadd}\varnothing$
70 inss1 ${⊢}{P}\left({k}\right)\cap \left(0..^{N}+1\right)\subseteq {P}\left({k}\right)$
71 70 33 sstrid ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {P}\left({k}\right)\cap \left(0..^{N}+1\right)\subseteq {ℕ}_{0}$
72 sadid1 ${⊢}{P}\left({k}\right)\cap \left(0..^{N}+1\right)\subseteq {ℕ}_{0}\to \left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\mathrm{sadd}\varnothing ={P}\left({k}\right)\cap \left(0..^{N}+1\right)$
73 71 72 syl ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\mathrm{sadd}\varnothing ={P}\left({k}\right)\cap \left(0..^{N}+1\right)$
74 69 73 eqtrd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\mathrm{sadd}\left(\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\cap \left(0..^{N}+1\right)\right)={P}\left({k}\right)\cap \left(0..^{N}+1\right)$
75 74 ineq1d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left(\left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\mathrm{sadd}\left(\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\cap \left(0..^{N}+1\right)\right)\right)\cap \left(0..^{N}+1\right)=\left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\cap \left(0..^{N}+1\right)$
76 inass ${⊢}\left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\cap \left(0..^{N}+1\right)={P}\left({k}\right)\cap \left(\left(0..^{N}+1\right)\cap \left(0..^{N}+1\right)\right)$
77 inidm ${⊢}\left(0..^{N}+1\right)\cap \left(0..^{N}+1\right)=\left(0..^{N}+1\right)$
78 77 ineq2i ${⊢}{P}\left({k}\right)\cap \left(\left(0..^{N}+1\right)\cap \left(0..^{N}+1\right)\right)={P}\left({k}\right)\cap \left(0..^{N}+1\right)$
79 76 78 eqtri ${⊢}\left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\cap \left(0..^{N}+1\right)={P}\left({k}\right)\cap \left(0..^{N}+1\right)$
80 75 79 syl6eq ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left(\left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\mathrm{sadd}\left(\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\cap \left(0..^{N}+1\right)\right)\right)\cap \left(0..^{N}+1\right)={P}\left({k}\right)\cap \left(0..^{N}+1\right)$
81 37 80 eqtrd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)\cap \left(0..^{N}+1\right)={P}\left({k}\right)\cap \left(0..^{N}+1\right)$
82 81 eleq2d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({N}\in \left(\left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)\cap \left(0..^{N}+1\right)\right)↔{N}\in \left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)\right)$
83 elin ${⊢}{N}\in \left(\left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)\cap \left(0..^{N}+1\right)\right)↔\left({N}\in \left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)\wedge {N}\in \left(0..^{N}+1\right)\right)$
84 elin ${⊢}{N}\in \left({P}\left({k}\right)\cap \left(0..^{N}+1\right)\right)↔\left({N}\in {P}\left({k}\right)\wedge {N}\in \left(0..^{N}+1\right)\right)$
85 82 83 84 3bitr3g ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left(\left({N}\in \left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)\wedge {N}\in \left(0..^{N}+1\right)\right)↔\left({N}\in {P}\left({k}\right)\wedge {N}\in \left(0..^{N}+1\right)\right)\right)$
86 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
87 42 86 eleqtrdi ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}\in {ℤ}_{\ge 0}$
88 eluzfz2 ${⊢}{N}\in {ℤ}_{\ge 0}\to {N}\in \left(0\dots {N}\right)$
89 87 88 syl ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}\in \left(0\dots {N}\right)$
90 42 nn0zd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}\in ℤ$
91 fzval3 ${⊢}{N}\in ℤ\to \left(0\dots {N}\right)=\left(0..^{N}+1\right)$
92 90 91 syl ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left(0\dots {N}\right)=\left(0..^{N}+1\right)$
93 89 92 eleqtrd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {N}\in \left(0..^{N}+1\right)$
94 93 biantrud ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({N}\in \left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)↔\left({N}\in \left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)\wedge {N}\in \left(0..^{N}+1\right)\right)\right)$
95 93 biantrud ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({N}\in {P}\left({k}\right)↔\left({N}\in {P}\left({k}\right)\wedge {N}\in \left(0..^{N}+1\right)\right)\right)$
96 85 94 95 3bitr4d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({N}\in \left({P}\left({k}\right)\mathrm{sadd}\left\{{n}\in {ℕ}_{0}|\left({k}\in {A}\wedge {n}-{k}\in {B}\right)\right\}\right)↔{N}\in {P}\left({k}\right)\right)$
97 30 96 bitrd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left({N}\in {P}\left({k}+1\right)↔{N}\in {P}\left({k}\right)\right)$
98 97 bibi2d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left(\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}+1\right)\right)↔\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}\right)\right)\right)$
99 98 biimprd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to \left(\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}\right)\right)\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}+1\right)\right)\right)$
100 99 expcom ${⊢}{k}\in {ℤ}_{\ge \left({N}+1\right)}\to \left({\phi }\to \left(\left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}\right)\right)\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}+1\right)\right)\right)\right)$
101 100 a2d ${⊢}{k}\in {ℤ}_{\ge \left({N}+1\right)}\to \left(\left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}\right)\right)\right)\to \left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({k}+1\right)\right)\right)\right)$
102 9 13 17 21 22 101 uzind4i ${⊢}{M}\in {ℤ}_{\ge \left({N}+1\right)}\to \left({\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({M}\right)\right)\right)$
103 5 102 mpcom ${⊢}{\phi }\to \left({N}\in \left({A}\mathrm{smul}{B}\right)↔{N}\in {P}\left({M}\right)\right)$